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\"of type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.
Keywords
Cite
@article{arxiv.1211.2851,
title = {The Simplicial Model of Univalent Foundations (after Voevodsky)},
author = {Chris Kapulkin and Peter LeFanu Lumsdaine},
journal= {arXiv preprint arXiv:1211.2851},
year = {2026}
}
Comments
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