#HoTT The Book : trois points de vue relationnel, homotopique et catégorique

The HoTT Book

Le tableau en haut de page 65 comporte trois colonnes et trois lignes.

Les trois colonnes, respectivement nommées « equality », « homotopy » et « higher groupoid » correspondent à trois points de vue, trois façons de voir ce dont nous avons traité jusqu’à présent . Nous appelons la première colonne « (point de vue) relationnel » parce que les trois lignes qui lui correspondent : réflexivité, symétrie et transitivité , sont trois propriétés de relation : une relation binaire qui possède ces propriétés est appelée « relation d’équivalence » et c’est le cas de l’égalité :
Réflexivité : a=a

Symétrie : si a =b alors b=a

Transitivité : si a =b et b=c alors a =c

Le deuxième point de vue dans la colonne centrale , est celui de l’homotopie et des chemins dans l’espace . La réflexivité devient le chemin constant d’un point A au même point A, la symétrie est l’inversion d’un chemin entre A et B (même chemin mais parcouru en sens inverse de B à A) et enfin la transitivité devient la concaténation des chemins : le chemin de B à C s’ajoute au chemin de A à B pour donner un chemin de A à C . Du point de vue catégorique (troisième colonne) la réflexivité devient le morphisme identité, la symétrie devient l’opération ( le morphisme) inverse, nous sommes dans un groupoide et donc tous les morphismes sont des isomorphismes donc sont inversibles, et la transitivité devient la composition de morphismesdans une catégorie ou une ∞-catégorie (dans ce cas précis un ∞-groupoide, puisque les types sont des ∞-groupoides)
Remarque 2.5 de la page 68 a propos des chemins d’ordre supérieur (higher paths)

On définit l’espace en boucle pour un point a:A(loop space) Ω(A,a) , A étant un type dont a est un terme (vu comme un point d’un espace ) , on note aussi ΩA quand l’identité de a est claire, c’est le type identité a =A a

On associe aussi les espaces en boucle d’ordre supérieur, par exemple d’ordre 2: espace en boucle de l’espace en boucle Ω2(A,a)

Page 68 est indiqué le théorème 2.1.6 (Eckman- Hilton) qui affirme que la loi de composition sur Ω2(A) est commutative.

Page 70 définition 2.1.7

Un type pointé (pointed type)est la donnée de (A,a) où A est un type et aun point de A.

Les espaces en boucle sur un type pointé sont définis récursivement comme pour les autres types.

2.2 page 71

Les fonctions entre types se comportent comme des foncteurs sur les chemins (paths). Cela revient à dire topologiquement parlant ( deuxième point de vue) que toute fonction est continue; en théorie classique des types, cela équivaut au fait que ces fonctions préservent l’égalité.

Soit une fonction f: A → B

Pour tout couple d’éléments de A x,y:A il y correspond une application :

apf : ( x=Ay) → (f(x) =Bf(y))

Et pour tout x:A l’identité est conservée :

apf (reflx)≡ reflf(x)

Advertisements
This entry was posted in category theory, Higher category theory, Higher topos theory, homotopy type theory. Bookmark the permalink.

Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s