#HoTT : The Book; homotopies et équivalences

The HoTT Book

Paragraphe 2.4 page 76

Au fond c’est le sujet central de la théorie homotopique des types, celui des rapports entre identité (égalité) et indiscernabilité:

https://anthroposophiephilosophieetscience.wordpress.com/2017/12/18/andrei-rodin-identity-equality-and-equivalence-in-mathematics/

https://anthroposophiephilosophieetscience.wordpress.com/2017/12/20/identite-des-indiscernables/

https://www.sussex.ac.uk/webteam/gateway/file.php?name=talk.pdf&site=552

https://anthroposophiephilosophieetscience.wordpress.com/2017/12/20/hott-equality-indistinguishabity/

https://uberty.org/wp-content/uploads/2017/06/synhott-shulman.pdf

What’s Special About Identity Types

C’est par là que les types peuvent être vus comme des ∞-groupoides, c’est à dire comme des objets de ∞Grpd, qui est une (∞,1)-catégorie, c’est à dire ici une Idée, un objet de (∞,1)Cat et l’exemple paradigmatique d’un ∞-topos, l’analogue du 1-topos Set, Idée de l’être , sous-catégorie de Cat qui est Idée de l’Idée

https://anthroposophiephilosophieetscience.wordpress.com/2016/08/25/la-metacategorie-cat-de-toutes-les-categories-comme-modele-mathematique-du-monde-des-idees-de-platon/

https://anthroposophiephilosophieetscience.wordpress.com/2016/08/22/premiere-pierre-pour-une-nouvelle-science-internelle-mathesis-universalis-lidee-de-lun/

http://alpha.math.uga.edu/~davide/The_Category_of_Categories_as_a_Model_for_the_Platonic_World_of_Forms.pdf

Mais revenons au Livre « Homotopy type theory » paragraphe 2.4 page 76

Le type x =A y , appelé Type identité (identity type) peut être vu comme chemin (path) ou équivalence entre deux éléments (deux points d’un espace ) x et y du type A.

L’axiome d’univalence nous assure que nous avons le droit d’identifier ces trois notions : égalité, équivalence, chemin

https://anthroposophiephilosophieetscience.wordpress.com/2017/12/05/axiome-dunivalence-hott-univalent-categories/

D’ailleurs la théorie homotopique des types est souvent appelée HoTT/UF ( UF pour « univalent foundations »)

https://ncatlab.org/nlab/show/Homotopy+Type+Theory+–+Univalent+Foundations+of+Mathematics

Nous passons dans la suite aux Types identité entre fonctions, et entre types considérés comme éléments de l’Univers

https://anthroposophiephilosophieetscience.wordpress.com/2017/12/18/universe-in-hott/

L’homotopie est définie en 2.4.1 page 76 :ce sont des fonctions dépendantes, de type:

(f ∽ g):≡ Πx:A(f(x)=g(x)

Il s’agit du type des équivalences fonctorielles ou , topologiquement parlant, des chemins continus (continuous paths). Il peut être vu comme type des isomorphismes naturels que sont les homotopies. Les fonctions f et g peuvent être considérées comme identiques si ce type a un habitant.

Une homotopie n’est pas une identité (f=g)

C’est seulement sous condition de l’axiome d’univalence, introduit en 2.9, que l’on aura l’équivalence entre homotopie et égalité .

En théorie des types les fonctions sont des foncteurs et les homotopies des transformations naturelles (des isomorphismes)

Une homotopie est une relation d’équivalence sur le type concerné : c’est une relation d’équivalence sur l’univers U dans le cas d’homotopie entre types (lemme 2.4.12 page 79)

Advertisements
This entry was posted in Homotopy, homotopy type theory. Bookmark the permalink.