#HoTT et théorie des catégories

http://benedikt-ahrens.de/talks/Marseille.pdf

Les types, entités qui sont à la base de HoTT et y remplacent les ensembles (ensembles qui sont considérés comme des types particuliers) peuvent être considérés comme des ∞-groupoides.

L’axiome des “univalent foundations ” asserte en gros que pour les types, isomorphisme coïncide avec égalité. L’axiome est noté en abrégé U F et accompagné toujours l’Homotopy type theory qu’on note donc quelquefois en abrégé HoTT UF

HoTT interprète les types comme des espaces (Page 9 sur 67) les éléments d’un type a:A sont interprétés comme des points dans un espace (Page 10 sur 67).
Une attention spéciale doit être portée aux “Identity types” qui sont dans HoTT le représentant du principe d’unité qui dans les catégories est le morphisme identité et que Badiou interprète pour les ensembles comme “compte pour un”

Pour deux éléments de type A a,b:A il existe un type d’identité ( ” Identity type”) qui est interprété comme l’espace des chemins (path space) menant de a à b: a ↝ b
( c’est une flèche comme pour un morphisme dans une catégorie mais avec une branche courbe de la flèche)
a et b sont dits homotopiques si il existe un chemin : a ↝ b
Ici la
Les “higher identity types ” sont des chemins (des homotopies ) entre les chemins , et ainsi de suite jusqu’à l’infini, et ne peuvent être compris que dans le cadre des ∞-catégories

Un autre lien, d’André Joyal , ayant le même sujet, est :

http://www.crm.cat/en/Activities/Documents/joyal-crm-2013.pdf

Il est nettement plus orienté vers un rôle conceptuel et explique (Page 7) le rôle de pont unificateur joué par la théorie des catégories entre “type theory” et “homotopy theory”, c’est à dire en substance HoTT (d’où est absente la théorie des catégories ); et surtout il donne les liens précis des travaux les plus importants (Pages 3 , 4, 6, 8 sur 75) .

Le principe “indistinguishability = equality” correspond au principe des indiscernables de Leibniz en métaphysique :

https://www.ac-grenoble.fr/PhiloSophie/logphil/reperes/identit2.htm

Il requiert l’axiome d’univalence et (Page 4 sur 67) celui d’extensionnalité s’agissant des fonctions ( functional extensionality )

Les propositions sont des types dans HoTT : un type est une proposition (Page 14 sur 67) si tous ses habitants (éléments ) sont homotopiques .

“Être une proposition” est une proposition, on peut le prouver dans le cadre de la théorie. Une proposition est soit vide, soit un singleton (type réduit à un élément )

https://ncatlab.org/nlab/show/propositions+as+types

https://groups.google.com/forum/m/#!msg/homotopytypetheory/o-cVRGFF-Ig/2-QOl9ucbFoJ

Page 17 sur 67 : un type A est un ensemble si Id A (x,y ) est une proposition pour tout couple x,y.
Les ensembles sont les espaces discrets , ceux dont les points, s’ils sont égaux, le sont d’une façon unique .

Voir aussi:

https://golem.ph.utexas.edu/category/2013/03/category_theory_in_homotopy_ty.html

Advertisements
This entry was posted in ∞-cosmoi, ∞-topoi, homotopy type theory and tagged , , , . Bookmark the permalink.