Homotopy type theory as a language for diagrams of $\infty$-logoses

Cet article démontre que l'homotopie type theory étendue par des modalités lex et accessibles permet de reconstruire certains diagrammes d'∞-logoses, offrant ainsi un cadre pour raisonner sur ces structures et généralisant la computabilité synthétique de Sterling aux relations logiques de dimension supérieure.

L'essentiel

🌌 Le Titre : L'Homotopie Type comme Langage pour les "Univers de Mathématiques"

Imaginez que les mathématiques ne se déroulent pas dans un seul monde, mais dans une infinité d'univers parallèles. Chaque univers a ses propres règles, ses propres objets et sa propre logique. En mathématiques avancées, on appelle ces univers des $\infty$-logoses (ou $\infty$-topos). C'est un peu comme si chaque univers était une version différente de la réalité où l'on peut faire du calcul, de la géométrie ou de la logique.

Le problème ? Ces univers ne sont pas isolés. Ils sont connectés entre eux par des "tunnels" (des fonctions) et des "ponts" (des transformations naturelles). Souvent, ces connexions forment des structures complexes, comme des diagrammes ou des réseaux.

L'auteur de cet article, Taichi Uemura, pose une question géniale :

"Comment pouvons-nous utiliser un seul langage universel pour décrire non pas un seul univers, mais tout un réseau d'univers connectés ?"

Sa réponse : La Théorie des Types Homotopique (HoTT).

---

🧱 L'Analogie du Lego et des "Modes"

Pour comprendre l'innovation, imaginons que vous avez une boîte de Lego géante (c'est la Théorie des Types). Normalement, cette boîte vous permet de construire un seul château magnifique (un seul univers mathématique). Mais si vous voulez construire un ensemble de châteaux reliés par des ponts, la boîte standard ne suffit pas : elle ne sait pas gérer les connexions entre les châteaux.

L'auteur propose une nouvelle façon d'utiliser cette boîte de Lego. Il introduit un concept appelé "Mode Sketch" (esquisse de mode).

1. Les "Modes" comme des lunettes magiques

Dans ce système, imaginez que vous avez plusieurs paires de lunettes magiques (appelées modalités).

• Quand vous mettez les lunettes A, vous voyez le monde d'une certaine façon (par exemple, vous ne voyez que les objets "lisses").
• Quand vous mettez les lunettes B, vous voyez le monde différemment (par exemple, vous ne voyez que les objets "solides").

L'idée clé est que ces lunettes ne sont pas juste des filtres passifs. Elles sont connectées. Si vous passez des lunettes A aux lunettes B, il y a une règle précise qui dit comment transformer ce que vous voyez.

2. L'Esquisse (Le "Mode Sketch")

Le "Mode Sketch" est simplement un plan ou un dessin qui dit :

• "Il y a 3 univers (lunettes A, B, C)."
• "L'univers A est connecté à B."
• "L'univers B est connecté à C."
• "Le chemin de A à C passe par B, et c'est cohérent."

Ce plan est très simple à écrire dans le langage de la théorie des types. Au lieu de construire un énorme système complexe pour décrire chaque univers séparément, on écrit juste le plan de connexion, et la théorie des types construit automatiquement les univers et leurs liens.

---

🧩 La Grande Révélation : Le "Collage" (Artin Gluing)

Comment fait-on pour relier ces univers ? L'auteur utilise une technique appelée "Collage d'Artin" (Artin gluing).

L'analogie du collage :
Imaginez que vous avez deux pièces de tissu (deux univers). L'une est en soie (lisse), l'autre en toile (rugueuse).

• Si vous voulez les coller ensemble, vous ne pouvez pas juste les coudre n'importe comment.
• Vous devez utiliser une "colle" spéciale qui respecte la texture de chaque tissu.

Dans cet article, l'auteur montre que si vous avez un plan (un Mode Sketch) qui dit comment coller vos univers, vous pouvez le faire à l'intérieur même du langage de la théorie des types.

C'est comme si vous aviez un logiciel de modélisation 3D. Au lieu de modéliser chaque pièce séparément, vous donnez au logiciel le schéma de l'assemblage, et il génère tout le modèle 3D complet, avec toutes les connexions, directement dans son espace de travail.

---

🚀 Pourquoi c'est important ? (Les Applications)

Pourquoi se donner autant de mal ? Voici deux raisons principales, expliquées simplement :

1. La "Logique Relationnelle" (Synthetic Tait Computability)

En informatique, on veut souvent prouver que deux programmes se comportent de la même façon (par exemple, qu'un programme optimisé fait exactement la même chose que le programme original). C'est ce qu'on appelle une relation logique.

Traditionnellement, prouver cela pour des systèmes complexes (comme ceux qui gèrent des dimensions supérieures, comme en physique théorique ou en informatique quantique) est un cauchemar.
Grâce à cette nouvelle méthode, on peut traiter ces relations logiques comme des objets mathématiques ordinaires dans la théorie des types. C'est comme si on transformait une preuve complexe en un simple calcul de Lego. Cela ouvre la porte à la vérification automatique de programmes très complexes.

2. Une version "3D" de la logique

La théorie des types classique est comme une ligne droite (1D). Les mathématiques modernes (comme la théorie de l'homotopie) sont comme des sphères, des tore, des structures en 3D, 4D, etc.
Cet article fournit un langage pour parler de ces structures multidimensionnelles sans avoir à sortir du langage de base. C'est comme si on apprenait à parler de la 4ème dimension en utilisant uniquement des mots du quotidien, sans avoir besoin de créer un nouveau dictionnaire.

---

🎯 En Résumé

Taichi Uemura nous dit :

"Vous n'avez pas besoin de créer un nouveau langage compliqué pour décrire des réseaux d'univers mathématiques. Vous pouvez utiliser le langage existant de la Théorie des Types Homotopique, en y ajoutant quelques règles simples (les 'Modes'). Ce langage va alors générer automatiquement tout le réseau d'univers et leurs connexions."

C'est une avancée majeure car cela permet aux mathématiciens et aux informaticiens de raisonner sur des structures complexes et interconnectées avec la même simplicité que s'ils ne regardaient qu'un seul objet. C'est passer de la construction d'une maison à la construction d'une ville entière, en utilisant les mêmes briques et les mêmes règles.

Résumé technique

Voici un résumé technique détaillé de l'article « Homotopy Type Theory as a Language for Diagrams of ∞-Logoses » de Taichi Uemura, rédigé en français.

1. Problématique

L'article s'attaque à la difficulté de raisonner sur les diagrammes d'∞-logoses (ou ∞-topos) à l'intérieur même de la Théorie des Types Homotopique (HoTT).

• Contexte : Un ∞-logos est un cadre général pour l'homotopie, analogue à la façon dont un logos classique (topos) l'est pour les mathématiques ensemblistes. La HoTT est un langage interne puissant pour les ∞-logoses, permettant de prouver des théorèmes qui sont ensuite interprétables dans n'importe quel ∞-logos.
• Le problème : La HoTT standard (plain HoTT) est insuffisante pour modéliser directement des diagrammes d'∞-logoses reliés par des foncteurs et des transformations naturelles.
  • L'internalisation naïve de ces structures échoue souvent : certaines adjonctions internes mènent à des contradictions, et les comonades idempotentes internes sont triviales.
  • Bien que des cas particuliers aient été résolus (notamment par Shulman via l'« Artin gluing »), il manquait un cadre général permettant de reconstruire systématiquement des diagrammes complexes d'∞-logoses à l'intérieur de la HoTT.

2. Méthodologie

L'auteur propose une approche basée sur l'ajout de modalités (subuniverses réflexifs) à la HoTT, spécifiquement des modalités lex, accessibles (LAM).

• Reconstruction interne : L'idée centrale est que certaines structures de diagrammes d'∞-logoses peuvent être reconstruites à l'intérieur d'un ∞-logos unique (le « logos collé ») en utilisant des LAM.
• Les Mode Sketches (Croquis de modes) : L'auteur introduit une nouvelle notion, le mode sketch, qui est un poset fini décidable muni d'un ensemble de triangles « minces » (thin). Ce croquis définit la forme du diagramme à internaliser.
• Axiomes en HoTT : Pour chaque mode sketch $M$, l'auteur postule un ensemble d'axiomes en HoTT :
  1. Des relations d'orthogonalité entre les LAM associées aux éléments du poset (Axiome A).
  2. L'inversibilité de certaines transformations naturelles pour les triangles minces (Axiome B).
  3. Une condition de « fracture » globale assurant que l'univers entier est reconstruit à partir des sous-universes modaux (Axiome C).
• Équivalence avec les propositions : L'auteur montre que ces axiomes basés sur les LAM sont équivalents à une formulation basée sur un treillis de propositions, reliant ainsi la théorie aux relations logiques synthétiques.

3. Contributions Clés

1. Théorème de Fracture et Collage Généralisé (Proposition 2.17) :

   • L'article améliore le théorème de fracture et collage de Rijke, Shulman et Spitters. Il démontre que le « join » (somme) canonique de deux LAM lex, accessibles est lui-même accessible. Cela permet de construire des univers plus grands à partir de sous-universes plus petits tout en préservant les propriétés techniques nécessaires.

2. Introduction des Mode Sketches (Définition 3.5) :

   • Définition formelle de structures de diagrammes internalisables via des LAM.
   • Démonstration que les types dans l'univers global d'un modèle de mode sketch se « fracturent » en une structure de relations logiques généralisées (types dépendant les uns des autres selon l'ordre du poset).

3. Lien avec la Calculabilité Synthétique de Tait (Théorème 4.4) :

   • L'auteur établit une équivalence entre les axiomes des mode sketches (basés sur les LAM) et la postulation d'un treillis de propositions.
   • Cela généralise la « Synthetic Tait Computability » de Sterling, offrant une méthode synthétique pour travailler avec des relations logiques de dimension supérieure (logical relations) directement en HoTT, sans avoir besoin de modèles externes complexes.

4. Théorie des Limites Oplax (Sections 5 et 6) :

   • L'auteur développe la théorie des limites oplax (oplax limits) pour les ∞-logoses.
   • Il prouve que la limite oplax d'un diagramme d'∞-logoses et de foncteurs lex, accessibles est elle-même un ∞-logos (Théorème 5.43).
   • Il établit une correspondance entre les transformations naturelles oplax et les foncteurs entre les catégories d'éléments (Corollaire 5.55).

4. Résultats Principaux

Le résultat central est le Théorème 6.4, qui établit une équivalence fondamentale :

• Pour tout mode sketch $M$, la catégorie $(\infty, 1)$ des modèles de $M$ dans les ∞-logoses (c'est-à-dire les ∞-logoses équipés d'une fonction satisfaisant les axiomes A, B, C) est équivalente à la catégorie $(\infty, 1)$ des diagrammes d'∞-logoses indexés par $M$ (via des foncteurs lex, accessibles).
• Construction :
  • De gauche à droite : Un modèle de $M$ est isomorphe à la limite oplax du diagramme correspondant.
  • De droite à gauche : À partir d'un diagramme d'∞-logoses, on peut construire un ∞-logos (la limite oplax) qui porte une structure interne de mode sketch satisfaisant les axiomes.

Ce théorème confirme que la HoTT étendue avec des LAM appropriées est un langage suffisant pour raisonner non seulement sur un seul ∞-logos, mais sur des diagrammes entiers d'∞-logoses.

5. Signification et Impact

• Unification de la théorie des types et de la théorie des catégories supérieures : L'article fournit un pont robuste entre la syntaxe de la HoTT et la sémantique complexe des diagrammes d'∞-topos.
• Relations Logiques de Dimension Supérieure : En généralisant la calculabilité synthétique de Tait, l'article ouvre la voie à l'étude des relations logiques dans des contextes de dimension supérieure. Cela est crucial pour la normalisation de théories des types de haute dimension (comme celles introduites par Nguyen et Uemura).
• Simplicité et Formalisation : Contrairement à d'autres approches (comme la HoTT cohésive étendue avec de nouveaux contextes), cette méthode reste dans le cadre de la HoTT standard (avec des opérateurs modaux internes). Cela rend les résultats plus faciles à formaliser dans des assistants de preuve existants (comme Agda ou Coq) et plus accessibles pour une utilisation informelle.
• Généralisation de l'Artin Gluing : L'article généralise la construction classique de l'Artin gluing (qui relie deux topos) à des diagrammes arbitraires de forme complexe, utilisant les limites oplax comme outil unificateur.

En résumé, Taichi Uemura démontre que la HoTT, enrichie par une axiomatique modale bien définie, possède la puissance expressive nécessaire pour internaliser et manipuler des structures diagrammatiques complexes d'∞-logoses, transformant ainsi la HoTT en un langage universel pour la théorie des ∞-topos diagrammatiques.