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

Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ενοσοφια μαθεσις

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…

View original post 158 more words

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s