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 $\mathrm{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}\stackrel{}{\to}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 $\mathrm{sSet}$ is defined to be a Kan fibration ${p}_{U}:\tilde{U}\to U$.
Such a universe in $\mathrm{sSet}$ may be obtained by lifting a Grothendieck universe $\mathcal{U}\in \mathrm{Set}$ to a type theoretic universe ${p}_{U}:\tilde{U}\to U$ in a presheaf topos $\hat{C}={\mathrm{Set}}^{{C}^{\mathrm{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}^{\mathrm{op}}=\alpha \circ (-)$ is given by postcomposition with $\alpha $. The idea behind this is that ${\mathcal{U}}^{(C/I{)}^{\mathrm{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 $\u27e8A,a\u27e9$ 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}:\mathrm{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}:\mathrm{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 ﬁles - 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}:\mathrm{Elts}(A)\to \Delta [n]$. This gives a lift $\Delta [n]\to \mathrm{Elts}(A)$ which composed with the projection $\mathrm{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}\stackrel{{r}_{\tilde{U}}}{\to}{\mathrm{Id}}_{\tilde{U}}\stackrel{{p}_{\tilde{U}}}{\to}\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 $\mathrm{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
$\mathrm{iscontr}(X:\mathrm{Set}):=({\Sigma}_{x}:X)({\Pi}_{y}:Y){\mathrm{Id}}_{X}(x,y)$
$\mathrm{hfiber}(X,Y:\mathrm{Set})(f:X\to Y)(y:Y):=({\Sigma}_{x}:X){\mathrm{Id}}_{Y}(f(x),y)$
$\mathrm{isweq}(X,Y:\mathrm{Set})(f:X\to Y):=({\Pi}_{y}:Y)\mathrm{iscontr}(\mathrm{hfiber}(X,Y,f,y))$
$\mathrm{Weq}(X,Y:\mathrm{Set}):=({\Sigma}_{f}:X\to Y)\mathrm{isweq}(X,Y,f)$
The eliminator $J$ for identity types induces a canonical map
The univalence axiom claims then that all maps $\mathrm{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 $\mathrm{sSet}$ a morphism to a Kan complex is a weak equivalence iff it is a homotopy equivalence.
$\mathrm{isweq}(X,Y)(f)$ is equivalent to