On a model invariance problem in #HoTT

Le site groundai.com où j’ai trouvé cette excellente introduction aux mathématiques fondamentales que nous pratiquons ici :

https://anthroposophiephilosophieetscience.wordpress.com/2018/03/05/hott-sets-types-categories/

contient tout un tas de liens intéressants, il suffit de cliquer en bas de page sur « Category theory », « Algebraic topology », etc…voici par exemple la page « category theory » avec les plus récentes références:

https://www.groundai.com/?tag=Category%20Theory

Dont celle ci qui concerne la théorie homotopique des types :

https://www.groundai.com/project/on-a-model-invariance-problem-in-homotopy-type-theory/

« On a model invariance problem in homotopy type theory« 

Page Arxiv :

https://arxiv.org/abs/1712.03409v1

L’auteur étudie la catégorie des foncteurs de Z/2Z ( l’anneau des entiers relatifs modulo 2 qui a deux éléments 0 et 1) vers Grpd, la catégorie des groupoides

Un objet de cette catégorie est un groupoide A muni d’une involution A → A et un morphisme est une foncteur équivariant

Cette catégorie possède une structure de « type theoretic fibration category » et constitue un modèle pour la théorie intentionnelle des types, l’auteur étudie la même catégorie de manière plus approfondie dans sa thèse qui est ici :

« On lifting univalence to the equivariant setting »

https://hal.archives-ouvertes.fr/tel-01294040v1/document

Nous avons déjà croisé les « fibration categories » et leur structure duale les « cofibration categories »:

https://ncatlab.org/nlab/show/fibration+category

https://anthroposophiephilosophieetscience.wordpress.com/2018/02/02/hott-fibration-categories-and-tribes/

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/05/highertopostheory-15-fibrations-densembles-simpliciaux/

https://anthroposophiephilosophieetscience.wordpress.com/2018/02/05/szumilo-co-fibration-categories-and-quasicategories/

Rappelons aussi ce lien que nous avons déjà signalé :

http://www.lorentzcenter.nl/lc/web/2011/467/presentations/Presentation%20C%20Kapulkin.pdf

« Fibration categories and Type theory »

ainsi que cet exposé de Michael Shulman:

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

https://home.sandiego.edu/~shulman/hottseminar2012/05categories.pdf

Advertisements
This entry was posted in category theory, Higher category theory, homotopy type theory, Logique, Science, mathesis, Science-internelle. Bookmark the permalink.