Ensembles (sets) et #HoTT

Emily Riehl écrit sur Twitter que la conclusion de ce texte article de Mike Shulman « will blow your mind »:

« homotopy type theory : The Logic of space « 

Click to access 1703.03007.pdf

La théorie des « espaces synthétiques » est expliquée sommairement au début, il s’agit de ne pas considérer la notion d’espace comme une structure surimposée à une construction ensembliste ( exemple : les variétés différentielles sont des structures mathématiques, définies à l’aide d’atlas , sur des ensembles de points) mais directement comme des constructions alternatives aux ensembles, avec les points jouant le rôle des éléments pour les ensembles. Ceci est la tâche de la théorie constructionniste des types (dépendent type theory) de Martin Lof :

https://ncatlab.org/nlab/show/Martin-Löf+dependent+type+theory

Ainsi, comme déjà noté, les types se présentent comme des collections de termes , analogues aux ensembles .
Comme d’autres systèmes formels, la theoriedes types de Martin Lof peut être interprétée dans des topos ou des « higher toposes ».
Ses objets basiques sont des espaces d’homotopie (« homotopy spaces ») , c’est à dire des ∞-groupoides .
Mike Shulman oppose ensuite syntaxe et sémantique ( relation sémantique a des objets extérieurs au système ) en expliquant que la plupart des mathématiciens rencontrent des difficultés avec la théorie des types parce que celle ci privilégie la syntaxe sur la sémantique.

Il définit la théorie des types comme une construction d’objets libres ( analogue à celle des « groupes libres » par exemple ) pour la théorie, non plus d’un domaine d’objets particulier (les groupes) mais pour celle de la totalité des mathématiques. Les équations des groupes libres prennent la forme de diagrammes commutatifs valables pour tous les « group object » dans n’importe quelle catégorie (par exemple ce qu’on appelle un groupe topologique est un « objet groupe «  dans la catégorie des espaces topologiques, un groupe de Lie est un objet groupe dans la catégorie des variétés différentielles).
Le paragraphe 2.3 en vient à l’opposition des types et des ensembles.

La différence majeure concerne la relation d’appartenance notée par le signe ∊.
En théorie des ensembles (par exemple ZFC) c’est une assertion que l’on peut confirmer ou nier, prouver ou réfuter. En théorie des types , un terme (quoique le livre HOTT déconseillé d’employer ce mot) appartient à un type comme un élément appartient à un ensemble, mais cette appartenance est une partie de sa nature profonde (« part of it’s nature ») . Shulman signale même , ce que j’ignorais, que deux types distincts ne peuvent pas avoir des termes en commun : il n’y a donc pas d’intersection de types comme il y en a pour les ensembles.
La théorie des ensembles de Lawvere appelée ETCS (elementary theory of The category of sets ) prend comme objets de base , de manière catégorique, les ensembles et les fonctions :

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

c’est à dire le topos des ensembles . Voir « définition » pour les axiomes.

Il y a un second papier sur ce thème, par Spitters et Rijke:

«  Sets in HoTT »

Click to access 1305.3835.pdf

où la théorie homotopique des types est vue comme « langage interne » de l’∞-catégorie des ∞-groupoides (faibles , non stricts) qui est un modèle pour l’axiome d’univalence. Voevodsky considérait ce langage comme une nouvelle fondation des mathématiques.

https://golem.ph.utexas.edu/category/2015/07/internal_languages_of_higher_c.html

This entry was posted in ∞-catégories, ∞-topoi, homotopy type theory, Théorie des ensembles (set theory) and tagged , , , , , . Bookmark the permalink.