T Streicher : a model of type theory in simplicial sets – a brief introduction to Voevodsky’s #HoTT

Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ενοσοφια μαθεσις

https://ncatlab.org/nlab/show/T.+Streicher+-+a+model+of+type+theory+in+simplicial+sets+-+a+brief+introduction+to+Voevodsky%27+s+homotopy+type+theory

L’article de T Streicher se lit en cliquant sur la référence au début.

Comme on l’a vu dans l’article 15 récent du Hashtag #HigherToposTheory, les ensembles simpliciaux , qui sont des foncteurs ayant pour cible Set, s’organisent en une catégorie Sset qui est comme Set un topos, et il est possible de doter cette catégorie, de deux façons ( classique et Joyal) d’une structure de « model category »

https://ncatlab.org/nlab/show/model+structure+on+simplicial+sets

Une structure de « model category » signifie que l’on dispose de trois classes de morphismes, les cofibrations (C) les weak equivalences ( WE) et les fibrations (F) qui peuvent différer selon la structure choisie.

Sset est un topos, donc possède un « natural number object « (NNO) jouant le même rôle que le monoide N des entiers naturels pour le topos Set:

https://ncatlab.org/nlab/show/natural+numbers+object

Les fibrations (F) sont les fibrations de Kan, on a vu dans la conférence de Joyal « Categorical HoTT » que ce sont…

View original post 266 mots de plus

Publicités