André Joyal : categorical #HoTT 2

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

L’exposé d’André Joyal est ici:

http://www1.maths.leeds.ac.uk/~pmtng/joyal-mit.pdf

Nous en avions déjà étudié la première partie ici:

https://anthroposophiephilosophieetscience.wordpress.com/2017/08/23/joyal-categorical-hott-1/

et avions vu que les tribus (tribes; attention il existe le même terme en théorie de la mesure, mais cela n’a rien à voir) sont des catégories particulières munies d’un objet terminal * et d’une structure de tribu, à savoir d’une classe de morphismes respectant certaines propriétés qui sont appelés fibrations.
Un type est un objet E d’une tribu, ce que l’on note :

⊢E : Type

Et les termes sont des éléments d’un type, c’est à dire des flèches dirigées de l’objet terminal vers le type , qui doit être considéré comme l’ensemble de ses termes :

t : * ? E

ce qui se note :

⊢ t : E

(Page 15 ; on notera le signe assertorique de jugement ⊢ )

Page 16 : une fibrations est un morphisme de la…

View original post 358 mots de plus

Publicités