# nLab T. Streicher - a model of type theory in simplicial sets - a brief introduction to Voevodsky' s homotopy type theory

category: type theory

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 $\left(C,W,F\right)$ (…).

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}\left(b\right)$ is in $F$.

## Identity on $X$

Let $X\in H$ be an object. Let

$X\stackrel{{r}_{X}}{\to }\mathrm{Id}\left(X\right)\stackrel{{p}_{X}}{\to }X×X$X\xrightarrow{r_X}Id(X)\xrightarrow{p_X}X\times X

be a factorization of the diagonal ${\delta }_{X}\stackrel{}{\to }X×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

$x,y:X⊢{I}_{X}\left(x,y\right)$x,y:X\vdash I_X(x,y)

Analogous, for a Kan fibration $f:A\to I$ we factor the diagonal ${\delta }_{f}:A\to A{×}_{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.

## Universes in $\mathrm{sSet}$ and lifting of Grothendieck universes into presheaf toposes

A universe in $\mathrm{sSet}$ is defined to be a Kan fibration ${p}_{U}:\stackrel{˜}{U}\to U$.

Such a universe in $\mathrm{sSet}$ may be obtained by lifting a Grothendieck universe $𝒰\in \mathrm{Set}$ to a type theoretic universe ${p}_{U}:\stackrel{˜}{U}\to U$ in a presheaf topos $\stackrel{^}{C}={\mathrm{Set}}^{{C}^{\mathrm{op}}}$ on some site $C$ by exponentiating $𝒰$ with the component-wise dependent sum and then forming the generalized universal bundle. To be more precise this is done by defining

(1)$U\left(I\right)={𝒰}^{\left(C/I{\right)}^{\mathrm{op}}}$U(I)=\mathcal{U}^{(C/I)^{op}}
(2)$U\left(\alpha \right)={𝒰}^{{\Sigma }_{\alpha }^{\mathrm{op}}}$U(\alpha)=\mathcal{U}^{\Sigma_\alpha^{op}}

where for a morphism $\alpha$ the dependent sum ${\Sigma }_{\alpha }^{\mathrm{op}}=\alpha \circ \left(-\right)$ is given by postcomposition with $\alpha$. The idea behind this is that ${𝒰}^{\left(C/I{\right)}^{\mathrm{op}}}$ is quivalent to the full subcategory of $\stackrel{^}{C}/Y\left(I\right)$ on those maps whose fibers are $𝒰$-small. The presheaf $\stackrel{˜}{U}$ is defined as

(3)$\stackrel{˜}{U}\left(I\right)=\left\{⟨A,a⟩\mid A\in U\left(I\right)\phantom{\rule{thinmathspace}{0ex}}\text{and}\phantom{\rule{thinmathspace}{0ex}}a\in A\left({\mathrm{id}}_{I}\right)\right\}$\tilde U(I)=\{\langle A,a\rangle | A\in U(I)\,\text{ and }\,a\in A(id_I)\}

and

(4)$\stackrel{˜}{U}\left(\alpha \right)\left(⟨A,a⟩\right)=⟨U\left(\alpha \right)\left(A\right),A\left(\alpha \to {\mathrm{id}}_{I}\right)\left(a\right)⟩$\tilde U(\alpha)(\langle A,a\rangle)=\langle U(\alpha)(A),A(\alpha\to id_I)(a)\rangle

for $\alpha :J\to I$ in $C$. The map ${p}_{U}:\stackrel{˜}{U}\to U$ sends $⟨A,a⟩$ to $A$. ${p}_{U}$ is generic for maps with $𝒰$-small fibers. These maps are up to isomorphism precisely those which can be obtained as pullback of ${p}_{U}$ along some morphism in $\stackrel{^}{C}$.

For $C=\Delta$ we apapt this idea in such a way that ${p}_{U}$ is generic for Kan fibrations with $𝒰$-small fibers. We redefine in this case

(5)$U\left(\left[n\right]\right)=\left\{A\in {𝒰}^{\Delta /\left[n\right]{\right)}^{\mathrm{op}}}\mid {P}_{A}\phantom{\rule{thinmathspace}{0ex}}\text{is a Kan fibration}\phantom{\rule{thinmathspace}{0ex}}\right\}$U([n])=\{A\in \mathcal{U}^{\Delta/[n])^{op}} | P_A\,\text{ is a Kan fibration }\,\}

where ${P}_{A}:\mathrm{Elts}\left(A\right)\to \Delta \left[n\right]$ is obtained from $A$ by the Grothendieck construction: For $A:\Delta \left[n\right]\to U$ it is the pullback $\left({P}_{A}:\mathrm{Elts}\left(A\right)\to \Delta \left[n\right]\right):={A}^{*}{p}_{U}$ of ${p}_{U}$ along $A$. For morphisms $\alpha$ in $\Delta$ we define $U\left(\alpha \right)$ as above since Kan fibrations are stable under pullbacks. $\stackrel{˜}{U}$ and ${p}_{U}$ are defined as above in (3) and (4) but with the modified $U$, formula (5).

###### Theorem

The simplicial set $U$, formula (5) is a Kan complex

###### Proof

V. Voevodsky some draft papers and Coq ﬁles - www.math.ias.edu/∼vladimir/Site3/Univalent Foundations.html

###### Theorem

For the simplicial set $U$, formula (5), the morphism ${p}_{U}:\stackrel{˜}{U}\to U$ is universal for morphisms with $𝒰$-small fibers in that every morphisms with $𝒰$-small fibers arises as a pullback of ${p}_{U}$ along some morphism in $H$.

###### Proof

${p}_{U}$ is a Kan fibration since if

$\begin{array}{ccc}{\Lambda }_{k}\left[n\right]& \stackrel{a}{\to }& \stackrel{˜}{U}\\ {↓}^{{i}_{k}^{n}}& & {↓}^{{p}_{U}}\\ \Delta \left[n\right]& \stackrel{A}{\to }& U\end{array}$\array{ \Lambda_k[n]&\xrightarrow{a}&\tilde U \\ \downarrow^{i_k^n}&&\downarrow^{p_U} \\\Delta[n]&\xrightarrow{A}&U }

is commutative, the pullback of ${p}_{U}$ along $A$ is by definition the Kan fibration ${P}_{A}:\mathrm{Elts}\left(A\right)\to \Delta \left[n\right]$. This gives a lift $\Delta \left[n\right]\to \mathrm{Elts}\left(A\right)$ which composed with the projection $\mathrm{Elts}\left(A\right)\to \stackrel{˜}{U}$ provides the searched diagonal filler $\Delta \left[n\right]\to \stackrel{˜}{U}$.

${p}_{U}$ is universal since a Kan fibration $a:A\to I$ with $𝒰$-small fibers is the pullback of ${p}_{U}$ along the morphism $A:I\to U$ sending $x\in I\left(\left[n\right]\right)$ to an $𝒰$-valued presheaf on $\Delta /\left[n\right]$ which is isomorphic to ${x}^{*}a$ by the Grothendieck construction.

$\begin{array}{ccccc}{A}_{x}& \to & A& \to & \stackrel{˜}{U}\\ {↓}^{{x}^{*}a}& & {↓}^{a}& & {↓}^{{p}_{U}}\\ *& \stackrel{x}{\to }& I& \stackrel{A}{\to }& U\end{array}$\array{ A_x&\to&A&\to&\tilde U \\ \downarrow^{x^* a}&&\downarrow^a&&\downarrow^{p_U} \\ * &\xrightarrow{x}&I&\xrightarrow{A}&U }
###### Corollary

The type theoretic universe ${p}_{U}:\stackrel{˜}{U}\to U$, Theorem 2, is closed under dependent sums, products and contains the natural-numbers object $N:=\Delta \left(ℕ\right)$.

## Identity types in the lifted Grothendieck universe $U$

We consider the factorization $\stackrel{˜}{U}\stackrel{{r}_{\stackrel{˜}{U}}}{\to }{\mathrm{Id}}_{\stackrel{˜}{U}}\stackrel{{p}_{\stackrel{˜}{U}}}{\to }\stackrel{˜}{U}{×}_{U}\stackrel{˜}{U}$ of the diagonal ${\delta }_{{p}_{\stackrel{˜}{U}}}$ of ${p}_{\stackrel{˜}{U}}$ into an acyclic cofibration ${r}_{\stackrel{˜}{U}}\in C\cap W$ followed by a fibration ${p}_{\stackrel{˜}{U}}\in F$.

### Interpretation of the eliminator for identity types

For interpreting the eliminator $J$ for $\mathrm{Id}$-types we pull back the whole situation along the projection

$\Gamma :=\left(C:{\mathrm{Id}}_{\stackrel{˜}{U}}\stackrel{U}{\to }{U}^{*}U,d:{\Pi }_{U}\left({r}_{\stackrel{˜}{U}}^{*}C\right)\right)$\Gamma:=(C:Id_{\tilde U}\xrightarrow{U}U^* U, d:\Pi_U(r^*_{\tilde U} C))

(…)

## Voevodsky’ s univalence axiom

Now we will see that Voevodsky’s univalence axiom holds in the model described above.

Fix the following notation

$\mathrm{iscontr}\left(X:\mathrm{Set}\right):=\left({\Sigma }_{x}:X\right)\left({\Pi }_{y}:Y\right){\mathrm{Id}}_{X}\left(x,y\right)$

$\mathrm{hfiber}\left(X,Y:\mathrm{Set}\right)\left(f:X\to Y\right)\left(y:Y\right):=\left({\Sigma }_{x}:X\right){\mathrm{Id}}_{Y}\left(f\left(x\right),y\right)$

$\mathrm{isweq}\left(X,Y:\mathrm{Set}\right)\left(f:X\to Y\right):=\left({\Pi }_{y}:Y\right)\mathrm{iscontr}\left(\mathrm{hfiber}\left(X,Y,f,y\right)\right)$

$\mathrm{Weq}\left(X,Y:\mathrm{Set}\right):=\left({\Sigma }_{f}:X\to Y\right)\mathrm{isweq}\left(X,Y,f\right)$

The eliminator $J$ for identity types induces a canonical map

$\mathrm{eqweq}\left(X,Y:\mathrm{Set}\right)\mathrm{isweq}\left(\mathrm{eqweq}\left(X,Y\right)\right)$eqweq(X,Y:Set)isweq(eqweq(X,Y))

The univalence axiom claims then that all maps $\mathrm{eqweq}\left(X,Y\right)$ are themselves weak equivalences, i.e.

###### Definition
$\mathrm{UnivAx}:\left(\Pi X,Y:\mathrm{Set}\right)\mathrm{isweq}\left(\mathrm{eqweq}\left(X,Y\right)\right)$UnivAx:(\Pi X, Y:Set)isweq(eqweq(X,Y))
###### Remark

The univalence axiom implies the function extensionality principle: for $f,g:X\to Y$ we have

$\left(\Pi x:X\right){\mathrm{Id}}_{Y}\left(\mathrm{fx},\mathrm{gx}\right)\right)\to {\mathrm{Id}}_{X\to Y}\left(f,g\right)$(\Pi x:X)Id_Y(fx,gx))\to Id_{X\to Y}(f,g)

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.

###### Remark

$\mathrm{isweq}\left(X,Y\right)\left(f\right)$ is equivalent to

$\mathrm{isiso}\left(X,Y\right)\left(f\right):=\left(\Sigma g:Y\to X\right)\left(\left(\Pi x:X\right){\mathrm{Id}}_{X}\left(g\left(\mathrm{fx}\right),x\right)\right)×\left(\left(\Pi y:Y\right){\mathrm{Id}}_{Y}\left(f\left(\mathrm{gy}\right),y\right)\right)$isiso(X,Y)(f):=(\Sigma g :Y\to X)((\Pi x:X)Id_X(g(fx),x))\times ((\Pi y:Y)Id_Y(f(gy),y))
Created on April 4, 2012 19:07:52 by Stephan Alexander Spahn (188.62.33.89)