This entry is about the article T. Streicher - a model of type theory in simplicial sets - a brief introduction to Voevodsky’ s homotopy type theory.
The aim of this note is to describe in an accessible way how simplicial sets organize into a model of Martin-Löf type theory. Moreover, we explain Voevodsky’s Univalence Axiom which holds in this model and implements the idea that isomorphic types are identical
The topos $sSet=:H$ contains a natural-numbers object. $H$ is equipped with the model structure $(C,W,F)$ (…).
Families of types are defined to be Kan fibrations. The class $F$ of Kan fibrations has the following properties:
It is closed under composition, pullback along arbitrary morphisms and contains all isomorphisms.
It is closed under $\Pi$; i.e. if $a:A\to I$ and $b:B\to A$ are in $F$ then $\Pi_a(b)$ is in $F$.
Let $X\in H$ be an object. Let
be a factorization of the diagonal $\delta_X : X \xrightarrow{}X\times X$ into an acyclic cofibration $r_X\in C\cap W$ followed by a fibration $p_X\in F$. We interpret the fibration $p_X$ as
Analogous, for a Kan fibration $f:A\to I$ we factor the diagonal $\delta_f:A\to A\times_I A$ of $f$ in this way.
Now the problem ist that such a factorization is not stable under pullback. To solve this problem we introduce the notion of type theoretic universe / Martin-Löf universe.
A universe in $sSet$ is defined to be a Kan fibration $p_U:\tilde U\to U$.
Such a universe in $sSet$ may be obtained by lifting a Grothendieck universe $\mathcal{U}\in Set$ to a type theoretic universe $p_U:\tilde U\to U$ in a presheaf topos $\hat C=Set^{C^{op}}$ on some site $C$ by exponentiating $\mathcal{U}$ with the component-wise dependent sum and then forming the generalized universal bundle. To be more precise this is done by defining
where for a morphism $\alpha$ the dependent sum ${\Sigma_\alpha^{op}}=\alpha\circ (-)$ is given by postcomposition with $\alpha$. The idea behind this is that $\mathcal{U}^{(C/I)^{op}}$ is quivalent to the full subcategory of $\hat C/Y(I)$ on those maps whose fibers are $\mathcal{U}$-small. The presheaf $\tilde U$ is defined as
and
for $\alpha:J\to I$ in $C$. The map $p_U:\tilde U\to U$ sends $\langle A,a\rangle$ to $A$. $p_U$ is generic for maps with $\mathcal{U}$-small fibers. These maps are up to isomorphism precisely those which can be obtained as pullback of $p_U$ along some morphism in $\hat C$.
For $C=\Delta$ we apapt this idea in such a way that $p_U$ is generic for Kan fibrations with $\mathcal{U}$-small fibers. We redefine in this case
where $P_A:Elts(A)\to \Delta[n]$ is obtained from $A$ by the Grothendieck construction: For $A:\Delta[n]\to U$ it is the pullback $(P_A:Elts(A)\to \Delta[n]):=A^* p_U$ of $p_U$ along $A$. For morphisms $\alpha$ in $\Delta$ we define $U(\alpha)$ as above since Kan fibrations are stable under pullbacks. $\tilde U$ and $p_U$ are defined as above in (3) and (4) but with the modified $U$, formula (5).
The simplicial set $U$, formula (5) is a Kan complex
V. Voevodsky some draft papers and Coq files - www.math.ias.edu/∼vladimir/Site3/Univalent Foundations.html
For the simplicial set $U$, formula (5), the morphism $p_U:\tilde U\to U$ is universal for morphisms with $\mathcal{U}$-small fibers in that every morphisms with $\mathcal{U}$-small fibers arises as a pullback of $p_U$ along some morphism in $H$.
$p_U$ is a Kan fibration since if
is commutative, the pullback of $p_U$ along $A$ is by definition the Kan fibration $P_A:Elts(A)\to \Delta[n]$. This gives a lift $\Delta[n]\to Elts(A)$ which composed with the projection $Elts(A)\to \tilde U$ provides the searched diagonal filler $\Delta[n]\to \tilde U$.
$p_U$ is universal since a Kan fibration $a:A\to I$ with $\mathcal{U}$-small fibers is the pullback of $p_U$ along the morphism $A:I\to U$ sending $x\in I([n])$ to an $\mathcal{U}$-valued presheaf on $\Delta/[n]$ which is isomorphic to $x^* a$ by the Grothendieck construction.
The type theoretic universe $p_U:\tilde U\to U$, Theorem 2, is closed under dependent sums, products and contains the natural-numbers object $N:=\Delta(\mathbb{N})$.
We consider the factorization $\tilde U\xrightarrow{r_{\tilde U}}Id_{\tilde U}\xrightarrow{p_{\tilde U}}\tilde U\times_U \tilde U$ of the diagonal $\delta_{p_{\tilde U}}$ of $p_{\tilde U}$ into an acyclic cofibration $r_{\tilde U}\in C\cap W$ followed by a fibration $p_{\tilde U}\in F$.
For interpreting the eliminator $J$ for $Id$-types we pull back the whole situation along the projection
(…)
Now we will see that Voevodsky’s univalence axiom holds in the model described above.
Fix the following notation
$iscontr(X :Set) := (\Sigma_x :X )(\Pi_y:Y ) Id_X (x, y)$
$hfiber(X, Y :Set)(f :X \to Y )(y:Y ) := (\Sigma_x :X ) Id_Y (f (x), y)$
$isweq(X, Y :Set)(f :X \to Y ) := (\Pi_y:Y ) iscontr(hfiber(X, Y , f , y))$
$Weq(X, Y :Set) := (\Sigma_f :X \to Y ) isweq(X, Y , f )$
The eliminator $J$ for identity types induces a canonical map
The univalence axiom claims then that all maps $eqweq(X,Y)$ are themselves weak equivalences, i.e.
The univalence axiom implies the function extensionality principle: for $f,g:X\to Y$ we have
Even without the univalence axiom we have the following result corresponding to the fact that in $sSet$ a morphism to a Kan complex is a weak equivalence iff it is a homotopy equivalence.
$isweq(X,Y)(f)$ is equivalent to