#HoTT display maps

Sur Nlab:

https://ncatlab.org/nlab/show/display+map

André Joyal en parle dans ces notes, page 27 sur 81

https://ncatlab.org/homotopytypetheory/files/Joyal.pdf

C’est une projection de l’espace total:

pr : ∑x:AE(x) → A

voir Page 26 pour la règle de ∑-formation

Un terme t:∑x:AE(x) est une paire (a,u) où a:A et

u: E(a)

La projection envoie t sur a

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