Définir les (∞,1)-catégories dans le cadre de #HoTT

Le lien est à

http://www.cs.nott.ac.uk/~psxpc2/reedy-slides.pdf

Page 6:

La donnée d’une (∞,1)- catégorie équivaut à :

La donnée d’un type des objets

La donnée d’un type des 1-morphismes pour tout couple d’objets

Une loi de composition des morphismes

Un morphisme identité Id

Une « tour infinie » de cohérences

Page 7 : on définit une (∞,1)-catégorie TYPE des types.

Tout type a une structure d’ (∞,0)- catégorie , donc une collection de types doit avoir une structure de (∞,1)-catégorie

https://mathoverflow.net/questions/145770/how-do-you-define-infinity-1-categories-in-homotopy-type-theory

https://ncatlab.org/nlab/show/internal+category+in+homotopy+type+theory

Advertisements
This entry was posted in ∞-catégories, ∞-topoi, Homotopy, homotopy type theory. Bookmark the permalink.