Le modèle simplicial de #HoTT

Henosophia TOPOSOPHIA μαθεσις uni√ersalis τοποσοφια MATHESIS οντοποσοφια ενοσοφια Philosophie, théorie des catégories et théorie homotopique des types

Des papiers de Kapulkin, Lumsdaine et Voevodsky



et :


« We describe how to interpret constructive type theory in the topos of simplicial sets where types appear as Kan complexes and families of types as Kan fibrations. Since Kan complexes may be understood as weak higher-dimensional groupoids this model generalizes and extends the (ordinary) groupoid model which was introduced by M. Hofmann and the author about 20 years ago. Finally, we discuss Voevodsky’s Univalence Axiom which has been shown to hold in this model. This axiom roughly states that isomorphic types are equal. The type theoretic notion of isomorphism provided by this model coincides with homotopy equivalence of Kan complexes. For this reason it has become common to refer to it as Homotopy Type Theory.

View original post

This entry was posted in Philosophie. Bookmark the permalink.