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 sSet=:HsSet=:H contains a natural-numbers object. HH is equipped with the model structure (C,W,F)(C,W,F) (…).

Families of types are defined to be Kan fibrations. The class FF 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:AIa:A\to I and b:BAb:B\to A are in FF then Π a(b)\Pi_a(b) is in FF.

Identity on XX

Let XHX\in H be an object. Let

Xr XId(X)p XX×XX\xrightarrow{r_X}Id(X)\xrightarrow{p_X}X\times X

be a factorization of the diagonal δ XX×X\delta_X\xrightarrow{}X\times X into an acyclic cofibration r XCWr_X\in C\cap W followed by a fibration p XFp_X\in F. We interpret the fibration p Xp_X as

x,y:XI X(x,y)x,y:X\vdash I_X(x,y)

Analogous, for a Kan fibration f:AIf:A\to I we factor the diagonal δ f:AA× IA\delta_f:A\to A\times_I A of ff 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 sSetsSet and lifting of Grothendieck universes into presheaf toposes

A universe in sSetsSet is defined to be a Kan fibration p U:U˜Up_U:\tilde U\to U.

Such a universe in sSetsSet may be obtained by lifting a Grothendieck universe 𝒰Set\mathcal{U}\in Set to a type theoretic universe p U:U˜Up_U:\tilde U\to U in a presheaf topos C^=Set C op\hat C=Set^{C^{op}} on some site CC 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

(1)U(I)=𝒰 (C/I) op U(I)=\mathcal{U}^{(C/I)^{op}}
(2)U(α)=𝒰 Σ α op U(\alpha)=\mathcal{U}^{\Sigma_\alpha^{op}}

where for a morphism α\alpha the dependent sum Σ α op=α(){\Sigma_\alpha^{op}}=\alpha\circ (-) is given by postcomposition with α\alpha. The idea behind this is that 𝒰 (C/I) op\mathcal{U}^{(C/I)^{op}} is quivalent to the full subcategory of C^/Y(I)\hat C/Y(I) on those maps whose fibers are 𝒰\mathcal{U}-small. The presheaf U˜\tilde U is defined as

(3)U˜(I)={A,a|AU(I) and aA(id I)}\tilde U(I)=\{\langle A,a\rangle | A\in U(I)\,\text{ and }\,a\in A(id_I)\}

and

(4)U˜(α)(A,a)=U(α)(A),A(αid I)(a)\tilde U(\alpha)(\langle A,a\rangle)=\langle U(\alpha)(A),A(\alpha\to id_I)(a)\rangle

for α:JI\alpha:J\to I in CC. The map p U:U˜Up_U:\tilde U\to U sends A,a\langle A,a\rangle to AA. p Up_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 Up_U along some morphism in C^\hat C.

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

(5)U([n])={A𝒰 Δ/[n]) op|P A is a Kan fibration }U([n])=\{A\in \mathcal{U}^{\Delta/[n])^{op}} | P_A\,\text{ is a Kan fibration }\,\}

where P A:Elts(A)Δ[n]P_A:Elts(A)\to \Delta[n] is obtained from AA by the Grothendieck construction: For A:Δ[n]UA:\Delta[n]\to U it is the pullback (P A:Elts(A)Δ[n]):=A *p U(P_A:Elts(A)\to \Delta[n]):=A^* p_U of p Up_U along AA. For morphisms α\alpha in Δ\Delta we define U(α)U(\alpha) as above since Kan fibrations are stable under pullbacks. U˜\tilde U and p Up_U are defined as above in (3) and (4) but with the modified UU, formula (5).

Theorem

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

Proof

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

Theorem

For the simplicial set UU, formula (5), the morphism p U:U˜Up_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 Up_U along some morphism in HH.

Proof

p Up_U is a Kan fibration since if

Λ k[n] a U˜ i k n p U Δ[n] A U\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 Up_U along AA is by definition the Kan fibration P A:Elts(A)Δ[n]P_A:Elts(A)\to \Delta[n]. This gives a lift Δ[n]Elts(A)\Delta[n]\to Elts(A) which composed with the projection Elts(A)U˜Elts(A)\to \tilde U provides the searched diagonal filler Δ[n]U˜\Delta[n]\to \tilde U.

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

A x A U˜ x *a a p U * x I A U\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:U˜Up_U:\tilde U\to U, Theorem 2, is closed under dependent sums, products and contains the natural-numbers object N:=Δ()N:=\Delta(\mathbb{N}).

Identity types in the lifted Grothendieck universe UU

We consider the factorization U˜r U˜Id U˜p U˜U˜× UU˜\tilde U\xrightarrow{r_{\tilde U}}Id_{\tilde U}\xrightarrow{p_{\tilde U}}\tilde U\times_U \tilde U of the diagonal δ p U˜\delta_{p_{\tilde U}} of p U˜p_{\tilde U} into an acyclic cofibration r U˜CWr_{\tilde U}\in C\cap W followed by a fibration p U˜Fp_{\tilde U}\in F.

Interpretation of the eliminator for identity types

For interpreting the eliminator JJ for IdId-types we pull back the whole situation along the projection

Γ:=(C:Id U˜UU *U,d:Π U(r U˜ *C))\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

iscontr(X:Set):=(Σ x:X)(Π y:Y)Id X(x,y)iscontr(X :Set) := (\Sigma_x :X )(\Pi_y:Y ) Id_X (x, y)

hfiber(X,Y:Set)(f:XY)(y:Y):=(Σ x:X)Id Y(f(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:XY):=(Π y:Y)iscontr(hfiber(X,Y,f,y))isweq(X, Y :Set)(f :X \to Y ) := (\Pi_y:Y ) iscontr(hfiber(X, Y , f , y))

Weq(X,Y:Set):=(Σ f:XY)isweq(X,Y,f)Weq(X, Y :Set) := (\Sigma_f :X \to Y ) isweq(X, Y , f )

The eliminator JJ for identity types induces a canonical map

eqweq(X,Y:Set)isweq(eqweq(X,Y))eqweq(X,Y:Set)isweq(eqweq(X,Y))

The univalence axiom claims then that all maps eqweq(X,Y)eqweq(X,Y) are themselves weak equivalences, i.e.

Definition
UnivAx:(ΠX,Y:Set)isweq(eqweq(X,Y))UnivAx:(\Pi X, Y:Set)isweq(eqweq(X,Y))
Remark

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

(Πx:X)Id Y(fx,gx))Id XY(f,g)(\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 sSetsSet a morphism to a Kan complex is a weak equivalence iff it is a homotopy equivalence.

Remark

isweq(X,Y)(f)isweq(X,Y)(f) is equivalent to

isiso(X,Y)(f):=(Σg:YX)((Πx:X)Id X(g(fx),x))×((Πy:Y)Id Y(f(gy),y))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)