Relations entre #HoTT et la théorie des catégories : page du Nlab

Cette page plus générale porte sur les liens entre la théorie des types et la théorie des catégories :

https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory

Il s’agit d’un exemple de dualité entre syntaxe et sémantique :

https://ncatlab.org/nlab/show/syntax-semantics+duality

la théorie des catégories  pouvant être considérée comme sémantique pour la théorie des types, qui joue le rôle de la syntaxe d’un langage ou calcul pour la théorie des catégories, ce qui s’énonce aussi : les catégories sont des modèles de la théorie des types, et dans le cas de la théorie homotopique des types les modèles se trouvent dans les (∞,1)-topoi élémentaires :

https://ncatlab.org/homotopytypetheory/show/model+of+type+theory+in+an+%28infinity%2C1%29-topos

Comme pour la théorie des 1-topoi, on distingue en dimension infinie les (∞,1)-topoi élémentaires et les (∞,1)-topoi de Grothendieck, selon une distinction analogue à celle entre les topoi élémentaires et les topoi de Grothendieck, qui sont des topoi de faisceaux :

https://ncatlab.org/homotopytypetheory/show/Grothendieck+%28infinity%2C1%29-topos

https://ncatlab.org/nlab/show/topos

Cependant le travail des mathématiciens sur les (∞,1)-topoi élémentaires est en cours et l’on ne dispose pas encore d’une définition satisfaisante, on dispose des recherches d’André Joyal sur le sujet :

https://ncatlab.org/homotopytypetheory/show/elementary+%28infinity%2C1%29-topos

ainsi que de celles de Mike Shulman :

https://anthroposophiephilosophieetscience.wordpress.com/2019/02/16/ehtt-mike-shulman-towards-elementary-∞-toposes/

 

https://hottandphilosophy.wordpress.com/2019/02/25/mike-shulman-internal-language-for-higher-toposes/

https://cpb-us-w2.wpmucdn.com/u.osu.edu/dist/0/60807/files/2018/05/ehttalk-pallui.pdf

https://scienceinternelle.wordpress.com/2019/02/15/ehtt-vs-hott-what-is-an-elementary-higher-topos/

https://golem.ph.utexas.edu/category/2017/04/elementary_1topoi.html

l’état des connaissances sur les EHT (c’est à dire les « elementary ∞-topoi) est synthétisé sur la page Nlab :

https://ncatlab.org/nlab/show/elementary+%28infinity%2C1%29-topos

La notion philosophique  de dualité

https://ncatlab.org/nlab/show/duality

est au fondement des recherches de ce blog, à travers la dualité primordiale entre les deux plans, représentant respectivement l’être et l’un , ce qui aboutit aux thèses de Franck Jedrzejewski sur « l’être comme dual de l’Un » :

https://anthroposophiephilosophieetscience.wordpress.com/2018/02/12/resume-de-la-these-de-frank-jedrzejewski-diagrammes-et-categories-lun-comme-dual-de-letre/

La jonction de HTT (« higher topos theory ») et de la théorie homotopique des types (ou « univalent foundations » UF) se fait logiquement dans HTTUF :

https://anthroposophiephilosophieetscience.wordpress.com/2019/09/30/hott-httuf-homotopy-type-theory-highertopostheory/

c’est là à mon avis le sens de l’identification de #HoTT et de #HTT ( « Higher topos theory » de Jacob Lurie)

 

This entry was posted in category theory, Higher category theory, homotopy type theory, HTTUF, Science, mathesis, Science-internelle, Type theory. Bookmark the permalink.