Categorical models of dependent types

Cette page :

https://ncatlab.org/nlab/show/categorical+model+of+dependent+types

Définit des notions que nous avons déjà rencontrées, comme “display maps” , “comprehension categories”, fibrations…
Elle aide ainsi à comprendre, comme les notes de Joyal ou de Shulman, les correspondances entre théorie des catégories et HoTT ou théorie des types, comme cette autre page :

https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory

Cette note de Shulman remplit le même objectif:

https://home.sandiego.edu/~shulman/hottminicourse2012/03models-handout2up.pdf

dont la Page 1 sur 21 établit les grandes lignes de cette correspondance.
Ainsi théorie des catégories ( ou des ∞-catégories) et HoTT peuvent être associées et d’ailleurs HoTT est née vers 2006 des recherches de catégoriciens comme Awodey .

Advertisements
This entry was posted in ∞-catégories, ∞-topoi, category theory, Higher category theory, Higher topos theory, homotopy type theory and tagged , , . Bookmark the permalink.