scholarly journals The simplicial model of Univalent Foundations (after Voevodsky)

2021 ◽  
Vol 23 (6) ◽  
pp. 2071-2126
Author(s):  
Krzysztof Kapulkin ◽  
Peter LeFanu Lumsdaine
Keyword(s):  
Univalent Foundations

scholarly journals COMPUTER PROOFS PRACTICE AND HUMAN UNDERSTANDING: EPISTEMOLOGICAL ISSUES

2021 ◽  
pp. 5-19
Author(s):  
Lev D. Lamberov ◽  
Keyword(s):  
Type Theory ◽  
Point Of View ◽  
Foundations Of Mathematics ◽  
Traditional Concept ◽  
New Approach ◽  
Informal Mathematics ◽  
Computer Proofs ◽  
Number Of Publications ◽  
Univalent Foundations ◽  
Epistemological Point

In recent decades, some epistemological issues have become especially acute in mathematics. These issues are associated with long proofs of various important mathematical results, as well as with a large and constantly increasing number of publications in mathematics. It is assumed that (at least partially) these difficulties can be resolved by referring to computer proofs. However, computer proofs also turn out to be problematic from an epistemological point of view. With regard to both proofs in ordinary (informal) mathematics and computer proofs, the problem of their surveyability appears to be fundamental. Based on the traditional concept of proof, it must be surveyable, otherwise it will not achieve its main goal — the formation of conviction in the correctness of the mathematical result being proved. About 15 years ago, a new approach to the foundations of mathematics began to develop, combining constructivist, structuralist features and a number of advantages of the classical approach to mathematics. This approach is built on the basis of homotopy type theory and is called the univalent foundations of mathematics. Due to itspowerful notion of equality, this approach can significantly reduce the length of formalized proofs, which outlines a way to resolve the epistemological difficulties that have arisen

scholarly journals Univalent categories and the Rezk completion

2015 ◽  
Vol 25 (5) ◽  
pp. 1010-1039 ◽  
Author(s):  
BENEDIKT AHRENS ◽  
KRZYSZTOF KAPULKIN ◽  
MICHAEL SHULMAN
Keyword(s):  
Category Theory ◽  
Type Theory ◽  
Dependent Type Theory ◽  
Equivalence Of Categories ◽  
Segal Spaces ◽  
Definition Of ◽  
Categorical Semantics ◽  
Univalent Foundations ◽  
Dependent Type

We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of ‘category’ for which equality and equivalence of categories agree. Such categories satisfy a version of the univalence axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them ‘saturated’ or ‘univalent’ categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.

scholarly journals Homotopy Type Theory: A Synthetic Approach to Higher Equalities

2018 ◽  
Author(s):  
Michael Shulman
Keyword(s):  
Set Theory ◽  
Homotopy Type ◽  
Type Theory ◽  
Synthetic Approach ◽  
Homotopy Type Theory ◽  
Inductive Types ◽  
Basic Ideas ◽  
Univalent Foundations ◽  
Modern Mathematics

Homotopy type theory and univalent foundations (HoTT/UF) is a new foundation of mathematics, based not on set theory but on “infinity-groupoids”, which consist of collections of objects, ways in which two objects can be equal, ways in which those ways-to-be-equal can be equal, ad infinitum. Though apparently complicated, such structures are increasingly important in mathematics. Philosophically, they are an inevitable result of the notion that whenever we form a collection of things, we must simultaneously consider when two of those things are the same. The “synthetic” nature of HoTT/UF enables a much simpler description of infinity groupoids than is available in set theory, thereby aligning with modern mathematics while placing “equality” back in the foundations of logic. This chapter will introduce the basic ideas of HoTT/UF for a philosophical audience, including Voevodsky’s univalence axiom and higher inductive types.

scholarly journals Univalent foundations as structuralist foundations

Synthese ◽  
2016 ◽  
Vol 194 (9) ◽  
pp. 3583-3617 ◽  
Author(s):  
Dimitris Tsementzis
Keyword(s):  
Univalent Foundations

scholarly journals An experimental library of formalized Mathematics based on the univalent foundations

2015 ◽  
Vol 25 (5) ◽  
pp. 1278-1294 ◽  
Author(s):  
VLADIMIR VOEVODSKY
Keyword(s):  
Type Theory ◽  
Proof Assistant ◽  
Formalization Of Mathematics ◽  
Constructive Type Theory ◽  
Short Overview ◽  
Formalized Mathematics ◽  
The Coq Proof Assistant ◽  
Constructive Type ◽  
Coq Proof Assistant ◽  
Univalent Foundations

This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models (see Kapulkin et al. 2012).

scholarly journals The Cantor–Schröder–Bernstein Theorem for $$\infty $$-groupoids

2021 ◽  
Author(s):  
Martín Hötzel Escardó
Keyword(s):  
Homotopy Type ◽  
Classical Logic ◽  
Type Theory ◽  
The Other ◽  
Bernstein Theorem ◽  
Homotopy Types ◽  
Homotopy Type Theory ◽  
Univalent Foundations

AbstractWe show that the Cantor–Schröder–Bernstein Theorem for homotopy types, or $$\infty $$ ∞ -groupoids, holds in the following form: For any two types, if each one is embedded into the other, then they are equivalent. The argument is developed in the language of homotopy type theory, or Voevodsky’s univalent foundations (HoTT/UF), and requires classical logic. It follows that the theorem holds in any boolean $$\infty $$ ∞ -topos.

Sign in / Sign up

Export Citation Format

Share Document