#HoTT Book : introduction

Le livre complet, 500 pages écrites par les experts mondiaux de cette nouvelle discipline, qui permet de fonder les mathématiques à nouveaux frais, et est très proche de la théorie des ∞-catégories et des ∞-Topoi, peut être téléchargé gratuitement ici:

The HoTT Book

Cependant, pour une étude s’rieuse, il vaut mieux en commander aussi une version “papier”, car la lecture d’une tablette s’avère dévoreuse d’énergie..

HoTT (homotopy type theory) avec son site et son blog:

https://homotopytypetheory.org

est une nouvelle branche des mathématiques, née de la topologie algébrique et de l’algèbre homologique, qui se situe au carrefour de la théorie de l’homotopie et de la théorie des types, mêlant la logique mathématique et la Science des ordinateurs (” theoretical computer Science”). Les types sont issus des travaux de Russell pour corriger les “paradoxes” trouvés par lui même dans la fondation ensembliste de la logique. Les types ne doivent pas être considérés comme des “ensembles spéciaux” mais comme des objets bien structurés qui ont une ressemblance certaine avec les “data types” dans les langages de programmation.

Il y a un lien très fort avec la théorie des catégories :

https://anthroposophiephilosophieetscience.wordpress.com/2017/03/01/highertopostheory-11-lanalogue-du-1-topos-set-pour-la-theorie-des-∞-categories-l-∞-categorie-spaces/

multidimensionnelles (“higher category theory”) les types étant la même chose que les ∞-groupoides , ou que des espaces (” Spaces”) en théorie de l’homotopie . Les éléments d’un ensemble sont remplacés par les points d’un espace , et deux points x et y sont égaux s’il existe un chemin (“path”) liant x à y:

x ↝ y

https://ncatlab.org/nlab/show/path+space+object.
Ces types sont considérés dans HoTT de manière purement homotopique, non topologique : il n’y est pas fait mention d'”ouverts” ni de convergence d’une suite.

L’axiome d’univalence de Voevodsky s’écrit :

( A= B) ≏ (A ≏ B)

L’égalité des types est l’équivalence homotopique entre espaces.
Il existe un “type total ” appelé Univers U dont les éléments sont des types appelés “small types” , ce qui évoque les catégories : les “petites catégories” sont les catégories dont les collections de morphismes sont des ensembles (elles sont dites “petites”) .
L’axiome d’univalence identifie ainsi trois notions :

Logique: A = B
Topologique : A ↝ B (“il existe un chemin dan l’Univers U entre A et B)

Homotopique : A ≏ B

Les “Higher Inductive Types” ( HITs) créés per Shulman et d’autres sont dans HoTT le cadre pour les définitions inductives (par récurrence ) dont l’exemple paradigmatique est celui de N les entiers naturels.

https://ncatlab.org/nlab/show/higher+inductive+type

Inductive Types in HoTT

Universal properties without function extensionality

Higher inductive-recursive univalence and type-directed definitions

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