#HoTT Homotopy theory in type theory : pour une compréhension claire de la théorie homotopique des types

J’ai déjà signalé ce lien hier :

http://dlicata.web.wesleyan.edu/pubs/bll13homotopy/bll13homotopy.pdf

Je voudrais faire remarquer brièvement combien il favorise l’intelligence de ce qu’est vraiment HoTT, à savoir l’introduction de l’homotopie dans la logique de la théorie des types, créée par Bertrand Russell pour éviter les paradoxes qu’il avait lui même soulevés de la théorie des ensembles.

C’est un fichier pdf, mais peu technique , à base de slogans et de « mots d’ordre »résumés, dans des notes (« slides ») correspondant à des exposés oraux.

On y retrouve les idées directrices bien souvent vues ici, mais cela ne peut pas faire de mal d’y insister :

La théorie de l’homotopie, branche de la topologie, est l’étude des déformations continues de courbes dans des espaces topologiques, ces courbes sont appelées « chemins » (path) , un chemin est une fonction continue :

f : [0,1] → X où X est l’espace topologique des points, 0 et 1 sont envoyés sur l’origine et l’autre extrémité du chemin, on étudie donc les déformations entre deux chemins p et q, qui ont les mêmes extrémités , et correspondent à des fonctions différentes. Une déformation peut être vue comme un chemin 2-dimensionnel entre les deux chemins p et q , catégoriquement comme un 2-morphisme entre deux 1-morphismes , et ainsi s’introduit, si l’on continue ce processus indéfiniment, la théorie des ∞-catégories et des ∞-groupoides ( c’est à dire des ∞-catégories où tous les k-morphismes sont des isomorphismes, c’est à dire sont inversibles).

La théorie des types est, comme dit plus haut, une alternative à la théorie des ensembles, une union de la théorie des ensembles et de la logique, où les objets primordiaux : N ( N entiers naturels, Z entiers relatifs, type booléen à deux valeurs, type des listes c’est à dire d’ensembles de nombres ) sont mis en relation par des fonctions.
La thèse célèbre « propositions as types » s’ensuit : les propositions (par exemple mathématiques, à propos de nombres) sont vues comme des types, et les éléments (ou termes) de ces types comme des preuves de ces propositions . Les types sont donc analogues à des ensembles ( dont les éléments sont les termes, c’est à dire des preuves de la proposition que sont les types)
La page 15-16 présente le triangle de base , dont les sommets sont : théorie de l’homotopie (topologie) théorie des types (logique) (théorie des ensembles) et théorie des catégories .

S’ensuit la célèbre thèse de Hofmann- Streicher : les types sont des ∞-groupoides (Page 16 à 20) dont les morphismes , tous inversibles, ne sont autres que des preuves (homotopie) , preuves de preuves (2-preuves) , etc… à l’infini.

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/28/hott-the-book-2-1-types-are-higher-groupoids/

Page 21 : la théorie des catégories y gagne de nouveaux principes, la théorie de l’homotopie de nouvelles preuves de théorèmes.

Page 23 à 26 est abordée la distinction entre synthétique ( de haut en bas) et analytique (de bas en haut, du plus simple au plus complexe) très importante dans la philosophie de Brunschvicg qui ne cesse de dénigrer le synthétique qu’il rattache au logique, alors que l’analytique , qui commence effectivement avec la géométrie analytique d’un Descartes est rattaché à la mathématique.

Page 28 à 37 : les types sont interprétés plutôt comme des espaces, géométriquement et visuellement donc , et non comme des ensembles , trop abstraits, les éléments des types sont des points dans ces espaces, et les chemins entre deux points M et N sont interprétés comme des preuves, des démonstrations de l’égalité de M et N

Il y a des opérations entre ces chemins, comme il y en a entre les morphismes dans une catégorie. A tout point M est associé un chemin en boucle, analogue au morphisme identité en théorie des catégories

Id: M= M appelé en théorie homotopique des types «réflexivité »
A tout chemin de M à N correspond son inverse (le chemin en sens inverse de N à M) , deux chemins a et b peuvent être composés en un chemin ab (on parcourt d’abord a puis b) le chemin identité 1 joue le rôle d’élément neutre c’est à dire que pour toutchemin u on a :
u1=1u=u

Et n’importe quel chemin suivi de son inverse (le chemin en sens inverse) redonne le chemin identité, ou refl:

uu -1= u-1u=1

On reconnaît une opération de groupe et effectivement les morphismes dans une catégorie se composent comme dans un groupe.

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