Tag Archives: Steve Awodey

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 ,

Awodey : natural models of #HoTT

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

Posted in Philosophie | Tagged

Help with #HoTT

C’est ici : https://math.stackexchange.com/questions/522239/where-to-get-help-with-homotopy-type-theory A noter le cours d’Awodey sur les catégories : Ainsi que cette conférence d’Awodey sur Mac Lane (fondateur avec Eilenberg de la théorie des catégories en 1945, ou 1942) et Rudolf Carnap : Steve Awodey est … Continue reading

Posted in category theory, Higher category theory, homotopy type theory, Philosophie mathématique | Tagged , ,

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

Posted in ∞-catégories, ∞-topoi, category theory, Higher category theory, Higher topos theory, homotopy type theory | Tagged , ,

#HoTT The Book : chapitre 1 , types vs sets

Le livre, écrit par les meilleurs spécialistes de cette nouvelle discipline, peut être acheté ou téléchargé gratuitement ici: The HoTT Book Il vaut mieux apprendre HoTT dans ce livre que lire, comme je le fais, des articles sur Arxiv ou … Continue reading

Posted in ∞-catégories, ∞-topoi, Grothendieck, Homotopy, homotopy type theory | Tagged , , , ,

Awodey : cubical #HoTT 1

http://www.helsinki.fi/lc2015/materials/slides_awodey.pdf Il n’est pas question ici de se lancer dans les arcanes des “cubical sets” et des recherches récentes sur la “cubical HoTT”, à la fin de cette note, mais de comparer les pages du début à celles du travail … Continue reading

Posted in homotopy type theory | Tagged , ,