D'Anjou-Madore, Ludovic
(2025).
« Théories homotopiques des types » Mémoire.
Montréal (Québec, Canada), Université du Québec à Montréal, Maîtrise en mathématiques.
Fichier(s) associé(s) à ce document :
Résumé
Nous étudions diverses formes de théories des types jusqu’à parvenir à la théorie homotopique des types de Martin-Löf avec univalence (Univalent Foundations Program, 2013). Nous présentons une sémantique ensembliste et une sémantique groupoïdale de la théorie des types de Martin-Löf avant de passer en revue les constructions fondamentales de la théorie homotopique des types. En particulier, nous analysons les propriétés logiques de cette théorie – à savoir qu’elle est intuitionniste et qu’elle « prolonge » la logique des propositions. De plus, nous présentons la structure de groupoïde d’ordre supérieur des types ainsi que la caractérisation de cette structure. Pour ce faire, nous étudions des objets analogues aux fibrations de la théorie de l’homotopie et nous montrons comment ces fibrations ont des propriétés de relèvement semblables à celles des fibrations usuelles de la théorie de l’homotopie. Nous analysons les propriétés des univers univalents. Nous montrons qu’en plus du fait que tout univers univalent est classifiant, tout sous-univers d’un univers classifiant est aussi classifiant pour une certaine classe de fonctions. Nous appliquons ce résultat pour présenter une démonstration que si un univers classifiant satisfait l’axiome extensionnalité et l’extensionnalité propositionnelle, alors cet univers est univalent. Finalement, nous montrons que la théorie homotopique des types possède une structure de tribu (Joyal, 2017) et que celle-ci permet de retrouver les opérations de la théorie.
_____________________________________________________________________________
MOTS-CLÉS DE L’AUTEUR : théorie homotopique des types, catégorie, tribu, groupoïde, univalence, fibration, univers classifiant.
RECHERCHER
PARCOURIR
LIBRE ACCÈS
