Joyal : categorical #HoTT 1

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

Advertisements
This entry was posted in category theory, homotopy type theory and tagged , . Bookmark the permalink.