#HoTT : relation des “tribes” et des “comprehension categories”

Les tribus (“tribes “) sont des espèces particulières de catégories introduites par Joyal, il en parle dans ces notes:

http://www.crm.cat/en/Activities/Documents/joyal-crm-2013.paf

et en Donne des exemples page 13 sur 75; il fait allusion page 12 sur 75 aux autres chercheurs qui utilisent cette notion, l’article de Lumsdaine et Warren qu’il évoque est ici:

https://arxiv.org/abs/1411.1736

et voici un article de Page North où est expliquée l’équivalence de la notion de tribu chez Joyal et de celle de “model of dependent type theory”:

https://www.dpmms.cam.ac.uk/~prn27/eca-paige-north.pdf

Page 15 sur 75 : un type est un objet d’une tribu, et une fibration:

E → A

peut être vue comme une famille interne d’objets de E paramétrés par A :

( E(x) x ∈ A)

famille qui est appelée “dependent type E(x) in context x: A

Notation:

x:A ⊢ E(x) : type

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