Categories with families

C’est le cadre pour interpréter la théorie des types dépendants (dependent type theory), notion équivalente à celle de « category with attributes « , la définition est donnée ici :

http://staff.math.su.se/palmgren/ErikP_Variants_CWF.pdf

Cet article fait le lien avec les catégories localement cartésiennes fermées:

http://perso.ens-lyon.fr/pierre.clairambault/cwfreport.pdf

C’est une idée qui a été introduite par Dybjer:

http://www.cse.chalmers.se/~peterd/papers/InternalTT.pdf

La théorie des types dépendants est la catégorie initiale dans la catégorie des « categories with families »:

http://iso.mor.phis.me/archives/2011-2012/stage-2012-goteburg/report.pdf

La notion de « category with families » est identique à celle de transformation naturelle représentable, page 3 de ce travail d’Awodey :

https://www.andrew.cmu.edu/user/awodey/preprints/natural.pdf

C’est à dire un modèle naturel de HoTT, la théorie homotopique des types, dont Steve Awodey est l’un des créateurs.

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