Tag Archives: Dybjer

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: … Continue reading

Posted in category theory, Grothendieck, Higher category theory, homotopy type theory | Tagged ,