Daily Archives: February 20, 2018

#HoTT categorical models of dependent type theory

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.63.8051&rep=rep1&type=pdf http://www.cs.nott.ac.uk/~psxpc2/report-2013.pdf Différents modèles catégoriques de la théorie des types sont donnés : «  categories with families » ( = « categories with attributes »), comprehension categories, contextual categories Advertisements

Posted in category theory, Higher category theory, homotopy type theory, Science, mathesis, Science-internelle

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 ,