Joyal : categorical #HoTT 1

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

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

La définition importante (Page 13-14 sur 81) est celle de tribu (« tribe « ) , c’est à dire une catégorie C munie d’une structur de tribu F (une sous-catégorie F de C) et d’un objet terminal.

Les morphismes de F sont appelés fibrations.

Les types sont les objets E d’une tribu C, noté

⊢E : type

Un terme de type E est un morphisme :

* ? E

où * est l’objet terminal

(Dans la théorie des catégories les flèches de l’objet terminal vers un objet quelconque A sont appelés éléments de A si A est un ensemble, ils se confondent avec les éléments de A au sens ensembliste)

Des exemples de tribus ( avec un choix adéquat des fibrations ) sont donnés Page 15:
notamment la catégorie Grpd des ( petits) groupoides, la catégorie Kan des complexes de Kan

View original post

Publicités