Structures supérieures en théorie des types homotopiques
Higher structures in homotopy type theory
par Antoine ALLIOUX sous la direction de Pierre-Louis CURIEN
Thèse de doctorat en Informatique
ED 386 Sciences Mathematiques de Paris Centre

Soutenue le lundi 17 juillet 2023 à Université Paris Cité

Sujets
  • Homotopie
  • Logique monadique du second-ordre
  • Théorie des types

Les thèses de doctorat soutenues à Université Paris Cité sont déposées au format électronique

Consultation de la thèse sur d’autres sites :

https://theses.hal.science/tel-04506555 (Version intégrale de la thèse (pdf))
Theses.fr (Version intégrale de la thèse (pdf))

Description en anglais
Description en français
Mots clés
Théorie des types homotopiques, Théorie des types, Algèbre supérieure, Théorie des catégories supérieures, Monades polynomiales, Opétopes
Resumé
La définition de structures algébriques sur des types arbitraires en théorie des types homotopiques (HoTT) s'est révélée hors de portée jusqu'à présent. Cela est dû au fait que les types sont, en général, des espaces plutôt que de simples ensembles, et que les égalités d'éléments d'un type se comportent comme des homotopies. Les lois équationnelles des structures algébriques doivent donc être énoncées de manière cohérente. Cependant, en mathématiques ensemblistes, la présentation de ces données de cohérence se fait à l'aide de structures algébriques sur des ensembles, telles que les opérades ou les préfaisceaux, qui ne sont donc pas soumises à des conditions de cohérence supplémentaires. Reproduire cette approche en HoTT conduit à une situation de dépendance circulaire puisque ces structures doivent être définies de manière cohérente dès le départ. Dans cette thèse, nous brisons cette circularité en étendant la théorie des types d'un univers de monades polynomiales cartésiennes qui, de manière cruciale, satisfont leurs lois définitionnellement. Cette extension permet de présenter les types et leurs structures supérieures sous forme de types opétopiques qui sont des collections infinies de cellules dont la géométrie est décrite par les opétopes. Les opétopes sont des formes géométriques introduites par Baez et Dolan afin de donner une définition des n-catégories. Nous ouvrons cette thèse en donnant une définition des opétopes dans une théorie des types similaire à celle du livre HoTT au chapitre 3. Nous définissons les opétopes comme séquences d'arbres bien fondés satisfaisant certaines propriétés qui sont capturées par leur typage. L'approche opétopique est particulièrement adaptée au contexte de la théorie des types car ces arbres sont aisément définissables comme types inductifs. Plus précisément, notre construction est basée sur une séquence de monades polynomiales cartésiennes, une notion qui devient centrale dans les chapitres suivants. Nous concluons ce chapitre par une définition inductive des faces d'un opétope. Ce chapitre est l'occasion pour le lecteur de se familiariser avec les opétopes en théorie des types qui sont des ensembles et qui échappent donc aux considérations de cohérence avant d'aborder les types opétopiques dont la complexité peut obscurcir la simplicité conceptuelle des opétopes. Nous étendons ensuite la théorie des types d'un univers de monades polynomiales cartésiennes clos sous certains constructeurs de monades au chapitre 4 qui nous servira à définir les types opétopiques au chapitre 5. Contrairement à notre définition des opétopes qui n'implique que des ensembles, les types opétopiques sont à valeurs dans des types arbitraires. Par conséquent, nous ne pouvons plus énoncer les lois équationnelles du chapitre 3 de façon cohérente. Nous définissons donc notre univers de monades polynomiales afin que ces lois soient satisfaites par définition. Les constructeurs sous lesquels notre univers est clos nous permettent alors de définir, en particulier, la construction tranche de Baez et Dolan sur laquelle repose notre définition des types opétopiques. Nous définissons finalement un certain nombre d'extensions afin d'établir des résultats plus avancés au chapitre 5. Enfin, nous tirons parti de notre univers de monades polynomiales pour définir les types opétopiques au chapitre 5. Cela nous permet de définir des structures algébriques supérieures cohérentes, parmi lesquelles les infini-groupoïdes et les (infini, 1)-catégories. De manière cruciale, leur structure supérieure est univalente en ce sens qu'elle coïncide avec celle induite par leurs types identités. Nous établissons ensuite quelques résultats attendus afin de motiver nos définitions. En particulier, nous comparons notre définition de type opétopique fibrant avec la définition d'algèbre cohérente de Baez et Dolan, et nous montrons qu'elles sont équivalentes sous certaines hypothèses.