Monthly Archives: October 2019

#ETCC #ETCS axiomatisation de #Cat catégorie des catégories et de #Set topos des ensembles

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

La (méta)catégorie Cat de toutes les (petites) catégories et la catégorie Set des ensembles ont ici joué le rôle de mathèmes de l’Idée d’Un et de l’Idée d’être :

https://anthroposophiephilosophieetscience.wordpress.com/2016/08/25/la-metacategorie-cat-de-toutes-les-categories-comme-modele-mathematique-du-monde-des-idees-de-platon/

https://anthroposophiephilosophieetscience.wordpress.com/2016/08/22/premiere-pierre-pour-une-nouvelle-science-internelle-mathesis-universalis-lidee-de-lun/

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

La théorie axiomatique de Cat a été entreprise par Bill Lawvere sous le nom d’ETCC (« elementary theory of the category of catégories ») ou ET2CC (« elementary theory of the 2-category of categories) :

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

L’axiomatisation de la catégorie Set des ensembles , c’est à dire de la théorie des ensembles dans l’esprit de la théorie des catégories (donc pas dans l’esprit des pionniers comme Cantor) est l’objet de ETCS (« elementary theory of the category of sets) :

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

On peut faire observer comme Alfred Tarski que la théorie des ensembles précède, non seulement historiquement mais logiquement, la théorie des catégories puisqu’une catégorie n’est rien d’autre que la donnée d’un ensemble d’objets et d’un ensemble de…

View original post 282 more words

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 155 more words