#HoTT The Book 2.1 Types are higher groupoids

The HoTT Book

Page 62

C’est la même idée que celle développée dans ces notes de Thomas Streicher:

https://www.lirmm.fr/~retore/LCS/online/streicher_bordeaux.pdf

ainsi que dans cet article séminal de Hoffman et Streicher:

Hofmann, Streicher: The groupoid interpretation of type theory

https://www.tcs.ifi.lmu.de/mitarbeiter/martin-hofmann/pdfs/agroupoidinterpretationoftypetheroy.pdf

Avec une rétrospective, vingt ans après :

https://ncatlab.org/homotopytypetheory/files/HofmannDMV.pdf

une idée qui est le point de départ des travaux de recherche sur les liens entre théorie des catégories et HoTT, comme le remarque Warren :

http://mawarren.net/papers/crmp1295.pdf

La notion de chemin inverse dont nous avons parlé dans le dernier article:

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/26/hott-the-book-chapter-2-homotopy-type-theory/

S’exprime par une fonction , pour toute paire d’éléments x,y:A

(x=y) → (y=x)

Qui associe au chemin p , allant de x à y , son inverse p-1, allant de y à x

avec reflx-1 ≡ reflx pour tout x

reflx : x=x étant l’élément réflexivité

On peut donc considérer un type comme un ∞-groupoide, or les ∞- groupoides sont des (∞, 1)- catégories, c’est à dire dans le cadre théorique de ce blog des Idées; ils forment une (∞,1)-catégorie notée ∞Grpd , qui est l’exemple paradigmatique d’un ∞-topos:

https://ncatlab.org/nlab/show/Infinity-Grpd

Sous-catégorie de (∞,1)Cat :

https://ncatlab.org/nlab/show/%28infinity%2C1%29Cat

qui est considérée ici comme plan internel de l’Idée, ou Dieu, cadre théorique pour l’hénosophie ou pensée-selon-l’Un.

Les types sont aussi interprétés comme des espaces, plutôt que des ensembles (de termes) et il existe justement une ∞-catégorie des espaces qui est un ∞-topos:

https://anthroposophiephilosophieetscience.wordpress.com/2017/03/01/highertopostheory-11-lanalogue-du-1-topos-set-pour-la-theorie-des-∞-categories-l-∞-categorie-spaces/

Il vaut la peine de lire page 62 la démonstration du lemme 2.1.1 pour se faire une idée de ce qu’on entend par démonstration constructive.

Il s’agit d’associer au lemme ou théorème que l’on veut démontrer un type : une preuve est alors un « habitant » ou élément ou terme de ce type , qui sera selon la traduction du quantificateur universel par un produit (et du quantificateur existentiel par une somme):

ΠA:UΠx,y:A(x=y) → ( y=x)

La démonstration , qui est donnée Page 63 en deux preuves, consiste à construire pour tout x,y:A et p:x=y un inverse p-1:y=x.
Par le principe d’induction il suffit de le construire pour y et x identiques, c’est à dire pour x=x, et l’on a alors:

reflx-1=reflx

Les travaux de William Lawvere associent les quantificateurs, universel et existentiel, à des foncteurs adjoints:

https://ncatlab.org/nlab/show/universal+quantifier

https://ncatlab.org/nlab/show/existential+quantifier

http://www.tac.mta.ca/tac/reprints/articles/16/tr16.pdf

Ceci se transmet à la théorie des probabilités, considérée comme logique en climat d’incertitude, par l’intermédiaire de la monade de Michèle Giry :

https://arxiv.org/pdf/1208.2938.pdf

Nous avons donc, compte tenu du fait que ces deux quantificateurs correspondent au produit et à la somme catégoriques, un rapprochement avec la théorie de l’adjonction, c’est à dire le cœur de la théorie des catégories.

Advertisements
This entry was posted in ∞-catégories, ∞-topoi, homotopy type theory. Bookmark the permalink.