Thomas Streicher: A Model of Intensional Type Theory in Simplicial Sets
Thomas Streicher
Technische Universität Darmstadt
Abstract: In the mid 1990s Hofmann and Streicher have shown that groupoids give rise to a model of Martin-Löf Type Theory where Id(A, t, s) is the discrete groupoid of all morphisms from t to s in A. But the syntax of intensional type theory only gives rise to a weak ∞-dimensional groupoid structure on every type. M. Warren has shown that strict ∞-dimensional groupoids provide a model of type theory. In our account we start from the observation that Kan complexes within the topos SSet of simplicial sets provide an appealing notion of weak ∞-dimensional groupoid. Moreover, a notion of family of types is provided by the notion of Kan fibration. Since SSet is a topos and Kan fibrations are closed under Σ and Π one may interpret the corresponding type-theoretic concepts in a straightforward way. Hofmann and Streicher have shown how to lift Grothendieck universes to type-theoretic universes in presheaf toposes SetCop when C is a category within the Grothendieck universe. Based on some results by V. Voevodsky we show how this can be adpated to build a universe U of Kan complexes which are small in the sense of the Grothendieck universe. Now working in the fibre over U and factoring there the diagonal on the generic type a : U El(a) as ananodyne cofibration followed by a Kan fibration gives rise to an interpretation of a : U, x, y : El(a) Id(El(a), x, y). Performing this construction in the slice over U avoids in a simple way the usual problems with stability under substitution. Finally, we discuss Voevodsky's Equivalence Axiom which allows one to reason in a type theory identifying equality with isomorphism.
Vabljeni!
