#HoTT : L’événement spirituel de la théorie homotopique des types

S’il est vrai, comme le disait Léon Brunschvicg il y a environ 90 ans , que « Le fait décisif de l’histoire, ce serait donc, à nos yeux, le déplacement dans l’axe de la vie religieuse au XVIIe siècle, lorsque la physique mathématique, susceptible d’une vérification sans cesse plus scrupuleuse et plus heureuse, a remplacé une physique métaphysique qui était un tissu de dissertations abstraites et chimériques autour des croyances primitives« 

quelques citations éparses de Brunschvicg particulièrement éclairantes, voire illuminatrices

alors ne peut on pas dire que « l’apparition au 20eme siècle de la théorie des catégories (en 1945, un an après la mort de Brunschvicg et la victoire de l’Occident sur la Bête, qui n’est pas morte cependant et s’est réveillée le 11septembre 2001 et en 2014 en Syrie et en 2015 en France) et l’apparition au 21eme siècle de la théorie homotopique des types sont un déplacement de l’Histoire elle même « ?

Certes cela semble outré mais j’en suis profondément convaincu : je ne me contente pas de donner ici des liens vers les travaux portant sur ce champ d’explorations, je les lis et les médite avec soin…

la théorie homotopique des types (HoTT) naît aux confluents de la logique, de la « computer science », de l’homotopie et de la théorie des types, mais elle n’est pas pour autant une sous- région de ces domaines : elle constitue par elle même un champ autonome. De même elle n’est pas un résidu , un « sous-objet » de la théorie des catégories, bien qu’elle soit née des travaux de chercheurs en ce domaine. C’est tout simplement une nouvelle fondation pour la totalité de la mathématique , qui vient compléter le rôle de la théorie des catégories en ce sens, pas la supplanter .. par contre il est une chose claire à mes yeux, comte tenu des observations qui sont livrées dans tous ces travaux : ce qui est supplanté, à la fois par HoTT et la TC , c’est la fondation ensembliste de la logique et de la mathématique. Comme je considère ici , en accord (seulement sur ce point) avec Badiou, la théorie des ensembles , disons la mathématique ensembliste, comme ce que la philosophie appelle depuis Aristote « ontologie », c’est la prédominance de l’ontologie qui se trouve mise à bas par l’évenement de 1945 et celui intervenu 60 ans plus tard, l’émergence de HoTT vers 2005 , sous condition de la théorie des catégories et de la naissance d’Internet à la fin du 20 eme siècle. Si bien qu’il s’agit à mes yeux d’un événement unique, de caractère double si l’on veut..

Certes les travaux d’André Joyal, approfondissant le lien entre HoTT et la TC, sont précieux entre tous, mais l’on peut aussi citer ceux de Shulman, Kapulkin, Szumilo, que Joyal est d’ailleurs le premier à citer et dont il souligne l’importance:

L’article très important de Kapulkin et Szumilo dont parle André Joyal

« Two years ago, I wrote a post for the n-Cafe, in which I sketched how to make precise the claim that intensional type theory (and ultimately HoTT) is the internal language of higher category theory. I wrote it in response to a heated discussion on Michael Harris’ blog Mathematics Without Apologies about what (if anything) HoTT is good for, with the goal of making certain arguments mathematically precise, rather than taking a side in the discussion« 

https://golem.ph.utexas.edu/category/2015/07/internal_languages_of_higher_c.html

https://golem.ph.utexas.edu/category/2017/11/internal_languages_of_higher_c_1.html