De #HigherToposTheory à #HomotopyTypeTheory

J’ai commencé à étudier sur ce blog, dans le Hashtag #HigherToposTheory l’extraordinaire livre de Jacob Lurie ” Higher Topos theory” que l’on peut lire gratuitement sur plusieurs sites, comme Arxiv, ou bien ici:

http://www.math.harvard.edu/~lurie/papers/highertopoi.pdf

Le dernier article publié dans le Hashtag est le numéro 12:

https://anthroposophiephilosophieetscience.wordpress.com/2017/04/19/highertopostheory-un-nouveau-guide-de-lecture/

Ordepuis une dizaine d’années une nouvelle discipline a émergé, qui possède de fortes connexions avec la théorie multidimensionnelle des catégories et des topoi (“higher category theory”, “higher topos theory”) . Cette nouvelle discipline s’appelle :

Homotopy type theory

(En abrégé :

HoTT

)
et il existe sur Google un groupe de discussions : HoTT Cafe

avec ce fil de discussion consacré aux relations de HoTT avec les travaux de Jacob Lurie et la “Higher topos theory”:

https://groups.google.com/forum/m/#!msg/hott-cafe/oBRMrk17G0I/5QBNVcE4AgAJ

Parmi les intervenants, on peut noter Urs Schreiber, qui participe de façon régulière comme rédacteur, au Nlab et au blog n-category café, ainsi que Mike Schulman qui est aussi un théoricien des “higher categories and topoi”, mais plus impliqué dans la recherche sur HoTT.

Les deux vont un peu dans le même sens : HoTT présente un fort potentiel d’attractivité pour les théoriciens de l’homotopie et des catégories et topoi, mais dans l’avenir et il faut être patient… pour le moment les chercheurs ou théoriciens des autres domaines ne sont pas très intéressés par HoTT (” they are dismissive of it”) et Mike Schulman qui lui est un spécialiste à la fois de HoTT et de HTT (“higher topos theory”) le regrette profondément (“too bad”). Urs Schreiber cite d’ailleurs explicitement cette page rédigée par Mike Schulman (et révisée par Bas Spitters, qui intervient aussi sur le groupe Google) :

https://ncatlab.org/homotopytypetheory/show/model+of+type+theory+in+an+(infinity,1)-topos

page qui associe , mais de manière conjecturelle (“it is expected that….”) les (∞,1)-topoi élémentaires de Lurie à HoTT :

https://ncatlab.org/homotopytypetheory/show/elementary+%28infinity%2C1%29-topos

en affirmant qu’ils permettent d’interpréter (“admettent un modèle de”) HoTT , mais cela n’est certain, et encore avec des restrictions, que pour les (∞,1)-topoi de Grothendieck:

https://ncatlab.org/homotopytypetheory/show/Grothendieck+%28infinity%2C1%29-topos

Quant à Jacob Lurie lui même, il ne semble d’après Schulman qui le connaît bien pas encore très intéressé par HoTT et j’avais déjà cité cet article de blog sur sa réaction en forme de “No comment”:

https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/

au programme de Voevodsky “Univalent foundations” qui est étroitement lié à HoTT.

Il existe un blog “Homotopy type theory” et un livre, dont le lien pour achat ou lecture gratuite est donné sur le blog, Mike Schulman y écrit régulièrement et voici l’un de ses articles les plus intéressants qui fait le lien avec les travaux de William Lawvere sur les “topoi cohésifs” :

Axiomatic cohesion in HoTT

qui sont selon moi le cadre rigoureux où l’on peut traiter les problèmes philosophiques (platoniciens) de l’un et du multiple, voir cet ancien article :

https://meditationesdeprimaphilosophia.wordpress.com/2016/01/01/cohesive-∞-topoi/

La théorie des types est d’ordre logique, elle remonte à l’émergence du paradoxe de Bertrand Russell, et constitue l’une des solutions pour traiter ce paradoxe, comme expliqué à la fin de cette page:

https://fr.m.wikipedia.org/wiki/Paradoxe_de_Russell

https://fr.m.wikipedia.org/wiki/Théorie_des_types

Les types sont des catégories hiérarchisées d’ensembles, un ensemble ne peut être élément que d’un ensemble de type supérieur.

Dans les liens de ce blog, il y a une rubrique “HoTT” j’y ai mis les liens de trois ouvrages de Hans Joachim Baues, un précurseur dans le domaine…cette rubrique est d’ailleurs un peu un “fourre-tout”, j’y classe tout ce qui se rapporte à l’homotopie, il y a d’ailleurs ici un nom à retenir, celui de Tim Porter , notamment la version révisée en 2010 de son article de 2001, consacré aux interactions de la théorie de l’homotopie et de la théorie des catégories , qui trouvent leur cadre dans ce qui est appelé “Abstract homotopy theory”, il y a d’ailleurs un livre de 1996 par Porter et Kamps, on en trouve la version en lecture partielle sur Google, mais pas le texte complet, mais les notions expliquées se retrouvent dans “Algebraic homotopy” de Baues:

Abstract homotopy theory and simple homotopy theory” par Porter et Kamps:

https://books.google.fr/books?id=7JYKxInRMdAC&printsec=frontcover&hl=fr#v=onepage&q&f=false

Grothendieck a trouvé les fondements de la théorie des catégories et topoi de dimensions supérieures, dont il est un peu le fondateur dans les années 80, dans des problèmes liés à l’homotopie, (une Grande théorie nouvelle s’origine toujours dans des problèmes, et non dans des théories, pour faire progresser la Science internelle il faut comprendre dans quels types de problèmes elle trouve sa source) homotopie, c’est à dire notion topologique de la déformation continue de courbes dans des espaces, et un topos peut être considéré comme une généralisation de la notion d’espace.

Je suis donc persuadé que la “homotopy type theory” qui se situe au carrefour de la géométrie, de l’algèbre et de la logique, comme le dit Steve Awodey ( qui écrit régulièrement sur le blog HoTT) au début de cet article:

https://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf

(sans oublier la programmation et la “computer Science”) est un domaine fructueux d’investigations pour la Science internelle.

Awodey rappelle aussi que HoTT trouve son origine dans la théorie constructive des types de PER Martin-Löf:

https://fr.m.wikipedia.org/wiki/Per_Martin-Löf

Dont elle donne une interprétation dans le cadre de la théorie de l’homotopie, donc au final:

HOTT= “version homotopique de la théorie des types de Martin-Löf”

Advertisements
This entry was posted in ∞-catégories, ∞-cosmoi, ∞-topoi, Bertrand Russell, category theory, Higher category theory, Higher topos theory, homotopy type theory, Philosophie, Philosophie mathématique, Science, mathesis, Science-internelle, Théorie des topoi (topos theory), Wronski-Messianisme-séhélianisme-Science-internelle and tagged , , , , , , , , , , , , , , . Bookmark the permalink.