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

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 les familles de types, d’objets d’une catégorie qui est une tribu .

Un Univers dans Sset est défini comme une fibration de Kan; les Univers de Grothendieck :

https://ncatlab.org/nlab/show/Grothendieck+universe

sont une construction ensembliste qui évite les paradoxes de la théorie des ensembles. Ils ont leur analogue dans tout topos:

https://ncatlab.org/nlab/show/universe+in+a+topos

La Page du Nlab est ici peu claire et l’on fera bien de revenir à l’article original de Streicher qui avec Hoffman est l’introducteur, il y a vingt ans, de la structure modélisatrice de groupoide dans HoTT (qui ne portait pas encore ce nom). L’idée dont la réalisation est assurée par le modèle de la théorie des types dans le cadre des ensembles simpliciaux remonte à ce travail de Hoffman et Streicher : à savoir l’identification de l’égalité propositionnelle des types (il y a deux types d’égalité, propositionnelle et définitionnelle, dans la théorie des types) avec les ‘isomorphismes.

http://rdp15.mimuw.edu.pl/slides-martin-hofmann.pdf

Dans le paragraphe 1 Page 1 de l’article de Streicher sont définis deux foncteurs , l’un S allant de la catégorie “géométrique” Sp des espaces topologiques et des fonctions continues vers la catégorie des ensembles simpliciaux. L’autre R, dit de “réalisation géométrique, est défini comme adjoint à gauche de S. Les objets de la catégorie image de S sont les complexes de Kan , ceux de l’image de R sont les CW-complexes.

Il y a beaucoup de choses ici qui me passent au dessus de la tête, mais je vais plutôt me concentrer avec les prochains articles sur le Livre du blog HoTT , et avancer ainsi dans la voie plus sûre d’une compréhension de cette discipline.

Advertisements
This entry was posted in ∞-catégories, ∞-topoi, category theory, Higher category theory, Higher topos theory, homotopy type theory, Philosophie, Théorie des topoi (topos theory) and tagged , , , . Bookmark the permalink.