André Joyal : categorical #HoTT 3

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

Nous poursuivons l’étude de la précieuse conférence de Joyal qui est ici :

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

Il est tout à fait utile d’étudier ce texte en même temps que le Big Book de HoTT pour garder le parallèle des notions catégoriques ( sur lesquelles insiste Joyal) et des notions plus spécifiques à HoTT qui tournent autour des types et de leurs termes ou éléments ainsi pour prendre un exemple la notion de « dependent type  » dans un contexte x : A correspond (Page 17 sur 81) à un objet (E,p) d’une tribu locale C(A) , notion définie à la même page 17. Donc nous avons, en étudiant en parallèle les deux, une sorte de registre traduisant les deux langages l’un dans l’autre, une « Pierre de Rosette » en quelque sorte.

Le concept de « changement de base » (« base change ») est présenté page 12, il donne lieu (Page 21) à un foncteur entre tribus locales:

View original post 233 mots de plus

Publicités