The Simplicial Model of Univalent Foundations (after Voevodsky)

TL;DR

This paper constructs a model of univalent type theory within simplicial sets, demonstrating the Univalence Axiom and linking the consistency of Martin-Löf type theory to ZFC with inaccessible cardinals.

Contribution

It introduces a categorical technique for modeling dependent type theory and constructs a simplicial set model satisfying the Univalence Axiom.

Findings

The model satisfies the Univalence Axiom.

The construction provides a coherence technique for categorical models.

It establishes a consistency link between type theory and set theory.

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.