#HoTT : locally cartesian closed categories (LCCC)

Le papier de Seely « Locally cartesian closed categories and Type theory »

http://www.math.mcgill.ca/rags/LCCC/LCCC.pdf

Cet article revient sur celui de Seely en prouvant une biequivalence de 2-catégories des LCCC et des MLTT (Martin Lof type theories)

Une catégorie C est dite localement cartésienne fermée si pour tout objet A de C la « slice category » C/A est cartésienne fermée.

André Joyal présente ces notions dans plusieurs de ses exposés sur le thème « categorical homotopy type theory « , voir :

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/13/andre-joyal-categorical-hott-3/

l’exposé de Joyal étant :

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

Page 32 sur 81 : une LCCC est une Π-tribu dans laquelle tout morphisme est une fibration

https://anthroposophiephilosophieetscience.wordpress.com/2018/01/09/hott-andre-joyal-π-tribus-et-h-tribus-tribus-de-martin-lof-et-de-voevodsky/

Voir aussi

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/22/hott-andre-joyal-la-notion-de-typos/

L’exposé de Joyal étant

http://www.math.uwaterloo.ca/~asl2013/Slides/Joyal.pdf

La notion de CCC est expliquée pages 11,12 avec des exemples de CCC, dont Set, Cat, Grpd

Page 20 pour les LCCC, des exemples sont donnés là aussi : Set est une LCCC, de même tout topos de Grothendieck, par contre Cat ne l’est pas, ni Grpd

Advertisements
This entry was posted in category theory, homotopy type theory, Science, mathesis. Bookmark the permalink.