Nicola Gambino cours III : homotopical models of type theory

Henosophia TOPOSOPHIA μαθεσις uni√ersalis τοποσοφια MATHESIS οντοποσοφια ενοσοφια Philosophie, théorie des catégories et théorie homotopique des types

Venant à la suite de :

https://anthroposophiephilosophieetscience.wordpress.com/2018/09/04/nicola-gambino-cours-ii-homotopical-algebra/

Le texte de ce cours III est ici :

http://www1.maths.leeds.ac.uk/~pmtng/Slides/HoTT-Lecture3.pdf

Situation : on est donc avec une théorie T des types, voir cours I :

https://hottandphilosophy.wordpress.com/2018/09/02/cours-i-de-nicola-gambino-sur-hott-type-theory/

et on étudie des « modèles » de cette théorie, c’est à dire des structures mathématiques concrètes (qui seront des catégories munies d’une « model structure », Gpd et SSet notamment comme on l’a vu au cours II portant sur la discipline, « Homotopical algebra », étudiant ce genre de domaines)

http://www1.maths.leeds.ac.uk/~pmtng/Slides/HoTT-Lecture2.pdf

où cette théorie « opère « .

Pages 2 et 3 est évoquée la distinction entre théories des types extensives (extensional) et intensives (intensional)

https://ncatlab.org/nlab/show/extensional+type+theory

Dans les théories extensives les « identity types «  sont de pures propositions , ce qu’on appelle des h-propositions, de h-level (homotopy level ) 1:

https://ncatlab.org/nlab/show/mere+proposition

Cette page sur l’idée « homotopy level «  contient un tableau très important sur la correspondance entre HoTT, théorie des catégories et topos supérieurs:

View original post 637 more words

Advertisements
This entry was posted in ∞-catégories, category theory, Higher category theory, Homotopy, homotopy type theory, Science, mathesis, Science-internelle. Bookmark the permalink.