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 contains a natural-numbers object. is equipped with the model structure (…).
Families of types are defined to be Kan fibrations. The class 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 and are in then is in .
Let be an object. Let
be a factorization of the diagonal into an acyclic cofibration followed by a fibration . We interpret the fibration as
Analogous, for a Kan fibration we factor the diagonal of 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 is defined to be a Kan fibration .
Such a universe in may be obtained by lifting a Grothendieck universe to a type theoretic universe in a presheaf topos on some site by exponentiating 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 the dependent sum is given by postcomposition with . The idea behind this is that is quivalent to the full subcategory of on those maps whose fibers are -small. The presheaf is defined as
for in . The map sends to . is generic for maps with -small fibers. These maps are up to isomorphism precisely those which can be obtained as pullback of along some morphism in .
For we apapt this idea in such a way that is generic for Kan fibrations with -small fibers. We redefine in this case
where is obtained from by the Grothendieck construction: For it is the pullback of along . For morphisms in we define as above since Kan fibrations are stable under pullbacks. and are defined as above in (3) and (4) but with the modified , formula (5).
The simplicial set , 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 , formula (5), the morphism is universal for morphisms with -small fibers in that every morphisms with -small fibers arises as a pullback of along some morphism in .
is a Kan fibration since if
is commutative, the pullback of along is by definition the Kan fibration . This gives a lift which composed with the projection provides the searched diagonal filler .
is universal since a Kan fibration with -small fibers is the pullback of along the morphism sending to an -valued presheaf on which is isomorphic to by the Grothendieck construction.
The type theoretic universe , Theorem 2, is closed under dependent sums, products and contains the natural-numbers object .
We consider the factorization of the diagonal of into an acyclic cofibration followed by a fibration .
For interpreting the eliminator for -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
The eliminator for identity types induces a canonical map
The univalence axiom claims then that all maps are themselves weak equivalences, i.e.
The univalence axiom implies the function extensionality principle: for we have
Even without the univalence axiom we have the following result corresponding to the fact that in a morphism to a Kan complex is a weak equivalence iff it is a homotopy equivalence.
is equivalent to