The simplicial model of Univalent Foundations (after Voevodsky)

By Chris Kapulkin, Peter LeFanu Lumsdaine. Journal of the European Mathematical Society (Print), 2012

244 citations recorded by the source corpus.

In this largely expository paper, we construct and investigate a model of the Univalent Foundations of Mathematics in the category of simplicial sets. To this end, we first give a new technique for constructing 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 this model. As a corollary, we conclude that Univalent Foundations are at least as consistent as ZFC with two inaccessible cardinals. The main results of the paper are due to Vladimir Voevodsky.

Subfields: Geometry and Topology, Mathematical Physics

View Paper: https://www.semanticscholar.org/paper/00586a15d00d5eab44799558df479d5d7428fe79

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Geometry and Topology

In Mathematical Physics

Citations in the corpus

A type theory for synthetic ∞-categories (2017, unknown): “These rules and axioms are motivated by homotopy-theoretic models such as Voevodsky’s simplicial set model [12].”
Higher Categories and Homotopical Algebra (2019, methodology): “Indeed, inspired by Voevodsky’s construction of a semantic interpretation of Homotopy Type Theory with a univalent universe within the homotopy theory of Kan complexes [KL16], we consider the universal left fibration.”
The Frobenius condition, right properness, and uniform fibrations (2015, background): “ of simplicial sets, this amounts to the preservation of Kan ﬁbrations by pushforward along Kan ﬁbrations, a fact that plays an important role in Voevodsky’s simplicial model of univalent foundations [27]. Our development begins by introducing a general notion of ﬁbration, which subsumes that of a K”
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom (2015, unknown): “Indeed, the proof of Theorem 3.4.1 in [17] contains a similar diagram where Example 8.”