#HoTT The Book chapter 2: Homotopy type theory

The HoTT Book

L’introduction à ce chapitre 2 est en quelque sorte une introduction à HoTT elle même, à ses méthodes et à ses thématiques.

L’idée fondamentale de HoTT (homotopy type theory = théorie homotopique des types) est que les types- notion logique, passés en revue au chapitre 1, peuvent être identifiés à des espaces objets de la discipline mathématique qu’est l’homotopie, ainsi qu’à des groupoides multidimensionnels (« higher groupoids »)

https://en.m.wikipedia.org/wiki/∞-groupoid

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.102.784&rep=rep1&type=pdf

https://groupoids.org.uk/pdffiles/vankampenbckground.pdf

Voici un article qui fait le lien entrera théorie des catégories et les « identity types », sans aucun doute la notion la plus importante de HoTT, la raison philosophique en a été expliquée ici:

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/24/hott-the-book-1-12-identity-types/

L’article de Van den Berg est ici:

https://arxiv.org/pdf/1604.06001.pdf

Un chemin (path) dans un espace X, entre deux points M et N , est une fonction p : [0,1] → X
avec p(0)= M et p(1)= N

Les chemins s’ additionnent (concaténation) et ont des inverses, mais le résultat de ces opérations n’est pas soumis à l’égalité stricte : ainsi aller de M à N puis de N à M selon le chemin inverse n’est pas strictement égal à l’identité (rester en M ) . Pour cette raison on introduit une notion plus grossière d’égalité qui est l’homotopie .

Une homotopie entre deux fonctions continues:

f : U → V

et g : U → V

Est une fonction continue

H : U × [0,1] → V

Telle que H ( x,0) = f(x) Et H (x,1)= g(x)

Une homotopie entre deux chemins p et q de M à N dans un espace X est une fonction continue

H : [0,1] × [0,1] → X

avec H(s,0) = p(s) et H(s,1) = q(s) pour tout s appartenant à [0,1]
et l’on exige aussi que H(0, t) = M et H(1, t)= N pour tout t appartenant à [0,1] c’est à dire que pour tout t appartenant à [0,1] :

H(-, t) est un chemin de M à N

Une homotopie entre deux chemins est donc un chemin entre chemins , un chemin 2-dimensionnel. On peut définir des homotopie entre homotopie, d’où des chemins 3- dimensionnels , et l’on poursuit ainsi pour arriver à des chemins k- dimensionnels qui sont les k-morphismes d’un ∞-groupoide

L’homotopie est une relation d’équivalence. Les classes d’homotopie des boucles à un point x forment un groupe, le groupe fondamental de l’espace X au point x :

https://ncatlab.org/nlab/show/fundamental+group

On a aussi le groupoide fondamental dont les objets sont les ponts de X et les flèches sont les chemins, identifiés à une homotopie près:

https://ncatlab.org/nlab/show/fundamental+groupoid

Et l’on arrive ainsi à l’ ∞-groupoide fondamental d’un espace :

https://ncatlab.org/nlab/show/fundamental+infinity-groupoid

Les Topoi peuvent être considérés comme des espaces généralisés , donc des groupoides comme le montre cet article d’André Joyal :

https://ac.els-cdn.com/000187089090013D/1-s2.0-000187089090013D-main.pdf?_tid=85c95570-ba5b-11e7-96ac-00000aab0f02&acdnat=1509028970_c6e1e430a99f87381ae9c182a1b483c3

On peut aussi définir le groupoide fondamental d’une catégorie et étudier l’homotopie dans Cat, catégorie des catégories:

https://hal.inria.fr/inria-00347424/document

Cet article du blog concerne les mêmes thèmes généraux de HoTT:

Homotopy Theory in Homotopy Type Theory: Introduction

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