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=: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 Π; i.e. if a:AI and b:BA are in F then Π a(b) is in F.

Identity on X

Let XH 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 into an acyclic cofibration r XCW followed by a fibration p XF. We interpret the fibration p X as

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

Analogous, for a Kan fibration f:AI we factor the diagonal δ f:AA× IA 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 sSet and lifting of Grothendieck universes into presheaf toposes

A universe in sSet is defined to be a Kan fibration p U:U˜U.

Such a universe in sSet may be obtained by lifting a Grothendieck universe 𝒰Set to a type theoretic universe p U:U˜U in a presheaf topos C^=Set C 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(I)=𝒰 (C/I) opU(I)=\mathcal{U}^{(C/I)^{op}}
(2)U(α)=𝒰 Σ α opU(\alpha)=\mathcal{U}^{\Sigma_\alpha^{op}}

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

(3)U˜(I)={A,aAU(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 in C. The map p U:U˜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 C^.

For C=Δ 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([n])={A𝒰 Δ/[n]) opP 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] is obtained from A by the Grothendieck construction: For A:Δ[n]U it is the pullback (P A:Elts(A)Δ[n]):=A *p U of p U along A. For morphisms α in Δ we define U(α) as above since Kan fibrations are stable under pullbacks. 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 files - www.math.ias.edu/∼vladimir/Site3/Univalent Foundations.html

Theorem

For the simplicial set U, formula (5), the morphism p U:U˜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

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

p U is universal since a Kan fibration a:AI with 𝒰-small fibers is the pullback of p U along the morphism A:IU sending xI([n]) to an 𝒰-valued presheaf on Δ/[n] which is isomorphic to x *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˜U, Theorem 2, is closed under dependent sums, products and contains the natural-numbers object N:=Δ().

Identity types in the lifted Grothendieck universe U

We consider the factorization U˜r U˜Id U˜p U˜U˜× UU˜ of the diagonal δ p U˜ of p U˜ into an acyclic cofibration r U˜CW followed by a fibration p U˜F.

Interpretation of the eliminator for identity types

For interpreting the eliminator J for Id-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)

hfiber(X,Y:Set)(f:XY)(y:Y):=(Σ x:X)Id Y(f(x),y)

isweq(X,Y:Set)(f:XY):=(Π y:Y)iscontr(hfiber(X,Y,f,y))

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

The eliminator J 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) 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:XY 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 sSet a morphism to a Kan complex is a weak equivalence iff it is a homotopy equivalence.

Remark

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)