#HoTT : théorie homotopique des types une révolution des mathématiques ?

Lorsque j’ai créé ce blog, il n’y a pas si longtemps de cela, je ne connaissais même pas ce nom : HoTT = homotopy type theory = théorie homotopique des types, encore moins en quoi consistait cette “nouvelle fondation” des mathématiques:

http://images.math.cnrs.fr/A-la-croisee-des-fondements-des-mathematiques-de-l-informatique-et-de-la.html

http://www.les-mathematiques.net/phorum/read.php?16,998167,998919

http://www.cse.chalmers.se/~coquand/gdrim.pdf

Cette nouvelle mathématique est née vers 2006 des travaux de théoriciens des catégories comme Steve Awodey qui est en plus un remarquable pédagogue auteur de “Category theory” dans la série “Oxford Logic guides”:

http://angg.twu.net/MINICATS/awodey__category_theory.pdf

Néanmoins je m’intéressais depuis longtemps à la théorie des catégories, née en 1945 des recherches de Mac Lane et Eilenbarg, en laquelle je voyais une fondation des mathématiques différente de celle de la théorie des ensembles , théorie des ensembles qui est au cœur des fameuses “mathématiques modernes” que l’on a cherché à introduire de force dans l’enseignement au Grand effroi des parents d’élèves et des … élèves, dans les années 60.

Si l’on avait plutôt choisi la théorie des catégories, qui est plus universelle , on aurait gagné du temps : un philosophe comme Alain Badiou continue et persiste dans cette erreur 50 ans plus tard, en “préférant” la théorie des ensembles, oh pardon l’oncologie mathématicienne, à la théorie des topos et des catégories censée permettre non la théorie de l’être ( vieille notion philosophique périmée, qui remonte à Aristote qui est le punching-ball favori de Brunschvicg) mais celle de “l’apparaître dans un monde”. Seulement la mathématique parle d’elle même : les ensembles sont des catégories particulières, celles sans flèches entre les éléments (objets) et tous les ensembles forment non pas un ensemble mais une catégorie, Set, qui est en même temps l’exemple paradigmatique des topos. La théorie des catégories et topos généralise donc celle des ensembles, et à toute catégorie correspond son morphismes -identité, qui est un foncteur, opération de l’Un qui n’est donc pas du tout déchu n’en déplaise à Badiou: si la catégorie est concrète, c’est à dire si ses objets sont des ensembles munis d’une structure particulière, on peut parler avec Badiou de “compte-pour-un” mais si elle est abstraite comme par exemple un groupe mathématique représenté catégoriquement, où la multiplicité est non plus celle des objets ( il n’y en a qu’un qui est l’élément neutre du groupe) mais celle des flèches ( qui sont les éléments du groupe, la loi de composition étant celle des flèches) ce n’est plus possible. Donc la théorie des catégories permet de “représenter” le principe fondamental de la Science et de la philosophie, le principe d’unité, au delà duquel il est vain de vouloir remonter. Cet Un ne doit cependant pas être considéré à l’exemple des métaphysique religieuses, islamique notamment, comme ” Un transcendant” ou ” Un séparé” mixte de l’être et de l’Un, mais comme immanence radicale de la réflexion intellectuelle possible en tout être humain, c’est à dire la réflexion proprement scientifique.

La notion des ∞-catégories est née des recherches de Grothendieck après 1980, elle mène à HoTT 25 ans plus tard. Les entités de base de HoTT sont les types, qui sont des “collections” mais non des ensembles ou des catégories. Néanmoins à tout type on peut associer un ∞-groupoide, c’est à dire une ∞-catégorie particulière, dont tous les k-morphismes sont des isomorphismes, des flèches inversibles.

Le meilleur moyen d’apprendre HoTT est la lecture patiente du Big Book, qui est téléchargeable gratuitement ici :

The HoTT Book

On entend cependant ici ou là des vois. Plus “modérées”, voire réfractaires, émanent de ceux qui “préférent” les raisonnements catégoriques à ceux des “types” : des chercheurs comme Jacob Lurie ne seraient pas très intéressés par la nouvelle discipline, par contre Emily Riehl déclare être attirée par les deux et ne voit pas de séparation entre les deux disciplines

https://arxiv.org/abs/1705.07442

http://www.math.jhu.edu/~eriehl/ct2017slides.pdf

Jugées par elle comme “aesthitically appealing”

Pour ma part il y a encore énormément de choses que je ne comprends pas dans HoTT et je comprends mieux les exposés faits par des théoriciens des catégories comme André Joyal, plus clairs à mes yeux et faisant mieux le lien avec les catégories:

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

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

http://home.sandiego.edu/~shulman/cmshighercategories2013/Joyal.pdf

Advertisements
This entry was posted in Alain Badiou, ∞-catégories, ∞-cosmoi, ∞-topoi, category theory, Grothendieck, Higher category theory, Higher topos theory, Homotopy, homotopy type theory, Léon Brunschvicg, Philosophie, Philosophie mathématique, Science, mathesis, Science-internelle and tagged , , , . Bookmark the permalink.