#HoTT : le cours d’André Joyal sur les tribus- notion catégorique pour la théorie des types

Advertisements

#HoTT The Book 2.1 Types are higher groupoids

Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ενοσοφια μαθεσις

The HoTT Book

Page 62

C’est la même idée que celle développée dans ces notes de Thomas Streicher:

https://www.lirmm.fr/~retore/LCS/online/streicher_bordeaux.pdf

ainsi que dans cet article séminal de Hoffman et Streicher:

Hofmann, Streicher: The groupoid interpretation of type theory

https://www.tcs.ifi.lmu.de/mitarbeiter/martin-hofmann/pdfs/agroupoidinterpretationoftypetheroy.pdf

Avec une rétrospective, vingt ans après :

https://ncatlab.org/homotopytypetheory/files/HofmannDMV.pdf

une idée qui est le point de départ des travaux de recherche sur les liens entre théorie des catégories et HoTT, comme le remarque Warren :

http://mawarren.net/papers/crmp1295.pdf

La notion de chemin inverse dont nous avons parlé dans le dernier article:

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/26/hott-the-book-chapter-2-homotopy-type-theory/

S’exprime par une fonction , pour toute paire d’éléments x,y:A

(x=y) ? (y=x)

Qui associe au chemin p , allant de x à y , son inverse p-1, allant de y à x

avec reflx-1 ≡ reflx pour tout x

reflx : x=x étant l’élément réflexivité

On peut donc considérer un type comme un ∞-groupoide, or les ∞- groupoides sont des…

View original post 285 more words