The Simplicial Model of Univalent Foundations (after Voevodsky)

Abstract

We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan fibration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model. As a corollary, we conclude that Martin-Löf type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.

50 pages. V5: final journal version, to appear in Journal of the European Mathematical Society; no change in theorem numbering. Homotopy-theoretic portions appear also in the note "Univalence in Simplicial Sets", arXiv:1203.2553

References in corpus (6)

• A formal proof of the four color theorem
• The identity type weak factorisation system
• An introduction to univalent foundations for mathematicians
• Homotopy Theoretic Models of Type Theory
• A C-system defined by a universe category
• Martin-Lof identity types in the C-systems defined by a universe category

Cited by in corpus (29)

• The Frobenius Condition, Right Properness, and Uniform Fibrations
• Modalities in homotopy type theory
• All $(\infty ,1)$-toposes have strict univalent universes
• Towards a constructive simplicial model of Univalent Foundations
• Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages
• Topological Quantum Gates in Homotopy Type Theory
• On Small Types in Univalent Foundations
• From Reversible Programs to Univalent Universes and Back
• Bicategorical type theory: semantics and syntax
• Bicategories in Univalent Foundations
• The Hurewicz theorem in Homotopy Type Theory
• Constructing Higher Inductive Types as Groupoid Quotients
• Transpension: The Right Adjoint to the Pi-type
• Modal Fracture of Higher Groups
• Homotopical inverse diagrams in categories with attributes
• On the $\infty$-topos semantics of homotopy type theory
• Canonicity and homotopy canonicity for cubical type theory
• A parametricity-based formalization of semi-simplicial and semi-cubical sets
• The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
• Limits and colimits of synthetic $\infty$-categories
• Non-accessible localizations
• The effective model structure and $\infty$-groupoid objects
• First-order homotopical logic
• The derivator of setoids
• Formalizing two-level type theory with cofibrant exo-nat
• Relative elegance and cartesian cubes with one connection
• Unifying cubical and multimodal type theory
• Polynomials in homotopy type theory as a Kleisli category
• Toward the effective 2-topos