The simplicial model of univalent foundations (after Voevodsky) (Q2031691)

The Univalent Foundations program is a new proposed approach to foundations of mathematics, originally suggested in [\url{https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf}], building on the systems of dependent type theory developed by \textit{P. Martin-Löf} [Intuitionistic type theory. Notes by Giovanni Sambin of a Series of Lectures given in Padua, June 1980. Napoli: Bibliopolis (1984; Zbl 0571.03030)] and others. In dependent type theory, equality can carry information. One can not ask whether elements of a type are equal on the nose in the classical sense. The Univalent Axiom introduced by Voevodsky strengthens this characteristics. The Univalent Axiom claims that equality between types, as elements of a universe, is the same as equivalence between them, as types, formalizing the practice of treating equivalent structures as completely interchangeable. It soiidifies the idea of types as some kind of spaces in the homotopy-theoretic sense. The principal objective in this paper is to justify the idea of types as spaces, constructing a model of type theory in the Quillen model category of simplicial sets in which the Univalent Axiom obtains. The fibrations called Kan fibrations serve as an interpretation of type dependency, Kan complexes standing for closed types. A synopsis of the paper goes as follows. \begin{itemize} \item \S 1 is concerned with general techniques for constructing models of type theory. \S 1.1 sets out the specific type theory that this paper considers, while \S 1.2 reviews some fundamental facts concerning its intended semantics in contextual categories after [\textit{T. Streicher}, Semantics of type theory. Correctness, completeness and independence results. With a foreword by Martin Wirsing. Basel: Birkhäuser Verlag (1991; Zbl 0790.68068)]. \S 1.3 makes use of universes to construct contextual categories representing the structural core of type theory, while \S 1.4 exploits categorical constructions on the universe to model the logical constructions of type theory, which presents a new solution to the coherence problem for modeling type theory [\textit{M. Hofmann}, Lect. Notes Comput. Sci. 933, 427--441 (1995; Zbl 1044.03544)]. \item \S 2 aims at constructing a model in the category of simplicial sets. \S 2.1 and \S 2.2 are dedicated to the construction and investigation of a weakly universal Kan fibration (a universe of Kan complexes), which is exploited to apply the techniques in \S 1, giving a model of the full type theory in simplicial sets. \item \S 3 is concerned wtih the univalence axiom. \S 3.1 formulates univalence in type theory, while it is formulated in terms of homotopy theory in \S 3.2. It is shown in \S 3.3 that these definitions correspond under the simplicial model. \S 3.4 demonstrates that the universal Kan fibration is univalent, the univalence axiom holding in the simplicial model. \S 3.5 discusses an alternative formulation of univalence, shedding further light on the universal property of the universe. \item The paper contains two appendices, setting out in full the type theory under consideration. Appendix A is devoted to a conventional syntactic presentation, while Appendix B deals with its translation into algebraic structure on contextual categories. \end{itemize}