#HoTT Mike Shulman : Categorical models of homotopy type theory

Science internelle Henosophia Toposophia Mathesis universalis

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

La page 1 donne un tableau de correspondance entre les concepts catégoriques et ceux de HoTT.

Nous avons déjà croisé de nombreux types de catégories qui peuvent être vus comme des modèles ( au sens de la théorie logique des modèles ) de la théorie des types : comprehension categories « , « contextuel categories », « fibration categories « . Toutes sont expliquées dans cette page Nlab

https://www.ncatlab.org/nlab/show/categorical+model+of+dependent+types

et sont étroitement liées aux tribus de Joyal :

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/15/hott-relation-des-tribes-et-des-comprehension-categories/

https://anthroposophiephilosophieetscience.wordpress.com/2018/03/04/hott-comprehension-categories-as-models-of-type-theory/

https://anthroposophiephilosophieetscience.wordpress.com/2018/01/14/hott-andre-joyal-notes-on-tribes-and-clans-les-fibration-categories-de-brown/

Le procéssus de définition est toujours pareil, et se répète ici pour les « display map categories « , définie ici page 3 sur 21 : il s’agit d’une catégorie munie d’un objet terminal et d’une sous – classe de morphismes obéissant à une propriété particulière, et stable par pull-back :

https://fr.m.wikipedia.org/wiki/Produit_fibré

Ces morphismes particuliers , appelés ici « display maps », sont nommés « fibrations » dans…

View original post 244 more words

This entry was posted in Philosophie. Bookmark the permalink.