🔢 mathematics

The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory

Cet article démontre que la théorie des types simpliciaux peut être formulée comme une théorie des types homotopiques avec un type intervalle postulé en prouvant que les remplisseurs uniques pour les cornes $(2,1)$ impliquent des remplisseurs uniques pour toutes les cornes intérieures via l'adjonction de Leibniz dans la catégorie sauvage des types, un résultat qui a été formalisé dans Cubical Agda.

Auteurs originaux : Tom de Jong, Nicolai Kraus, Axel Ljungström

Publié 2026-06-18

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Tom de Jong, Nicolai Kraus, Axel Ljungström

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayiez de construire une ville complexe et multicouche où les routes ne sont pas seulement des lignes plates, mais qu'elles ont une direction, des règles de circulation et même des « embouteillages » qui peuvent être résolus de manières spécifiques. Ce document porte sur la création d'un meilleur ensemble de plans pour cette ville, plus précisément pour un monde mathématique appelé Théorie des Types de l'Homotopie (HoTT).

Voici la décomposition de ce que les auteurs ont fait, en utilisant des analogies simples.

1. Le Problème : Construire une ville avec des rues à sens unique

Dans les mathématiques standard (et la HoTT standard), les routes sont comme des rues à double sens. Si vous pouvez aller de A vers B, vous pouvez toujours revenir de B vers A. C'est comme un groupe d'amis où tout le monde est également connecté.

Mais les auteurs veulent construire une ville avec des rues à sens unique (des morphismes dirigés). Dans cette ville, vous pouvez aller de A vers B, mais peut-être pas l'inverse. C'est le monde de la Théorie des Types Simpliciaux.

Cependant, il y a un piège. Dans une ville normale, si vous avez une route de A vers B et une autre de B vers C, vous pouvez facilement les combiner pour créer une route de A vers C. Mais dans cette ville mathématique de haute technologie, dire simplement « nous pouvons les combiner » ne suffit pas. Vous devez prouver que la combinaison fonctionne parfaitement, et que si vous combinez trois routes dans des ordres différents, vous arrivez au même endroit.

Dans l'« ancienne » méthode pour faire cela (le cadre de Riehl-Shulman), ces règles étaient écrites dans un « méta-langage » séparé (comme un livre de règles écrit en dehors de la ville). Les auteurs voulaient écrire les règles à l'intérieur de la ville elle-même, en utilisant un outil spécial appelé Type d'Intervalle (pensez à une règle qui mesure la direction).

2. La Grande Découverte : L'Adjonction de Leibniz

La principale réussite technique du document est de prouver une règle puissante appelée l'Adjonction de Leibniz.

L'Analogie : La Machine « Pousse-Tire »
Imaginez que vous avez deux machines :

La Machine Produit-Pushout (La Pousse) : Cette machine prend deux routes à sens unique et les combine pour créer une nouvelle structure de route plus complexe. C'est comme prendre deux briques Lego et les emboîter côte à côte pour faire une base plus large.
La Machine Hom-Pullback (La Tire) : Cette machine fait l'inverse. Elle regarde une structure de route complexe et demande : « De combien de manières puis-je insérer une petite route spécifique à l'intérieur de celle-ci ? » C'est comme demander : « De combien de manières différentes puis-je faire glisser une pièce de puzzle spécifique dans ce puzzle plus grand ? »

Les auteurs ont prouvé que ces deux machines sont parfaitement liées.

Si vous savez comment la machine « Pousse » fonctionne, vous savez automatiquement comment la machine « Tire » fonctionne.
Elles sont les deux faces d'une même pièce.

Pourquoi est-ce difficile ?
D'habitude, dans les mathématiques simples, ce lien est évident. Mais dans ce monde mathématique « sauvage » (où les routes peuvent se tordre et tourner de manières infinies), prouver ce lien revient à essayer de faire un nœud dans une corde qui change constamment de forme. Les auteurs ont dû être incroyablement prudents pour s'assurer que les « nœuds » (les preuves mathématiques) tenaient bon sans se défaire.

3. Le Raccourci : Passer des Cartes aux Familles

L'une des astuces ingénieuses utilisées par les auteurs a été de changer de perspective.

La méthode difficile : Essayer de prouver la règle en regardant des « cartes » individuelles (des routes spécifiques de A vers B). C'est comme essayer de résoudre un embouteillage en regardant chaque voiture individuellement. Cela devient très vite désordonné et confus.
La méthode facile : Ils ont réalisé que regarder des « familles » (des groupes de routes organisés par un point de départ) était beaucoup plus propre. C'est comme regarder le flux de trafic d'un quartier entier plutôt que des voitures individuelles.

Ils ont prouvé que le monde des « Cartes » et le monde des « Familles » sont en fait la même chose (grâce à une règle appelée Univalence). En passant à la vue « Famille », le nouage complexe de nœuds est devenu beaucoup plus facile à résoudre.

4. Le Résultat : Résoudre l'Énigme de la « Composition »

Une fois que leur machine « Pousse-Tire » a fonctionné, ils l'ont appliquée à un problème spécifique : les Types de Segal.

Le Problème :
Un « Type de Segal » est une ville où l'on peut combiner des routes (composer). Mais pour que la ville soit stable, il faut s'assurer que :

La combinaison des routes fonctionne.
Les combiner dans des ordres différents donne le même résultat (associativité).
Toute la « colle » de niveau supérieur qui maintient ces règles est parfaite.

Par le passé, les mathématiciens devaient vérifier ces règles une par une, comme si l'on vérifiait chaque brique d'un mur.

L'Ancien Résultat : Ils savaient que les premières couches de briques étaient solides (pour des formes simples comme des triangles ou des carrés).
Le Nouveau Résultat : Les auteurs ont utilisé leur machine « Pousse-Tire » pour prouver que si la première couche de briques est solide, alors toutes les couches au-dessus le sont automatiquement.

Ils ont montré que si une ville possède une règle simple pour combiner deux routes (une forme de « corne »), elle possède automatiquement les règles parfaites pour combiner n'importe quel nombre de routes, quelle que soit la complexité de la forme.

5. La « Formalisation » (La Preuve Informatique)

Enfin, les auteurs n'ont pas seulement écrit cela sur papier. Ils ont construit un modèle numérique de toute leur théorie en utilisant un programme informatique appelé Cubical Agda.

Considérez cela comme la construction d'une simulation virtuelle de leur ville.
Ils ont exécuté le code, et l'ordinateur a vérifié chaque étape de leur logique pour s'assurer qu'il n'y avait pas de bugs ou de lacunes.
Cela prouve que leur machine « Pousse-Tire » et leur résultat « toutes les couches sont solides » sont mathématiquement 100 % corrects.

Résumé

En bref, les auteurs ont construit une nouvelle façon interne de gérer les « rues à sens unique » en mathématiques. Ils ont découvert une relation « Pousse-Tire » puissante entre la combinaison des routes et leur analyse. En utilisant cette relation, ils ont prouvé que si une structure mathématique fonctionne pour des formes simples, elle fonctionne automatiquement pour toutes les formes complexes, évitant ainsi aux mathématiciens de devoir vérifier chaque possibilité à la main. Ils ont vérifié tout cela à l'aide d'un ordinateur pour garantir une précision absolue.

Résumé Technique : L'Adjonction de Leibniz en Théorie des Types Homotopiques

Énoncé du Problème
La théorie des types simpliciaux (STT) étend la théorie des types homotopiques (HoTT) pour fournir un cadre synthétique pour les catégories supérieures en équipant les types de morphismes dirigés via un intervalle. Un défi central dans ce domaine est de définir les « types de Segal » — des types où les morphismes dirigés peuvent être composés. Bien que la composition soit directe, assurer que cette composition est associative et unitaire nécessite une hiérarchie infinie de cohérences supérieures. Dans la formulation standard de la STT par Riehl et Shulman, ces cohérences sont souvent traitées via des constructions méta-théoriques, ce qui rend une formalisation complète difficile. Spécifiquement, prouver qu'un type possédant des remplisseurs uniques pour les cornes $(2,1)$ (la condition de base pour les types de Segal) implique des remplisseurs uniques pour toutes les cornes intérieures $(n,k)$ (généralisant l'associativité et l'unitalité de la composition) est non trivial. Les résultats précédents, tels que ceux de Riehl et Shulman, couvraient des cas de basse dimension spécifiques ( $n=3$ ), mais une preuve générale pour tout $n$ et $k$ au sein d'un cadre HoTT unifié est restée un obstacle technique ouvert.

Méthodologie
Les auteurs adoptent une approche de théorie des types homotopiques « simple » (plain), suivant Gratzer, Weinberger et Buchholtz, plutôt que l'approche d'intervalle méta-théorique de Riehl et Shulman. Ils postulent un type intervalle $I$ qui forme un treillis distributif borné, évitant ainsi le besoin d'ordres totaux ou de modalités spécifiques.

L'innovation technique centrale est l'internalisation de l'adjonction de Leibniz au sein de la « catégorie sauvage de types ».

Catégories Sauvages : Les auteurs travaillent avec des « catégories sauvages », qui sont des traductions naïves de la théorie des catégories dans la HoTT. Celles-ci manquent de données de cohérence supérieure (les lois d'associativité et d'identité sont soit définitionnelles, soit non suivies), ce qui les distingue des $(\infty, 1)$ -catégories, mais elles sont suffisantes pour les besoins des auteurs.
L'Adjonction : Ils établissent que le produit-pushout (noté $\hat{\times}$ $\hat{\times}$ ) est adjoint au hom-pullback (noté $\pitchfork$ $⋔$ ) dans la catégorie sauvage des applications.
- Pour les applications $f: A \to B$ et $g: X \to Y$ , le produit-pushout $f \hat{\times} g$ est l'application induite par le pushout de $f \times Y$ et $A \times g$ .
- Le hom-pullback $f \pitchfork g$ est l'application induite entre les types fonctions.
- L'adjonction stipule : $\text{Map}(f \hat{\times} g, h) \simeq \text{Map}(f, g \pitchfork h)$ .
Applications vs Familles : Une preuve directe de cette adjonction dans la catégorie sauvage des applications est intraçable en raison de la complexité du suivi des données de cohérence (7-uplets d'applications et d'identifications). Pour surmonter cela, les auteurs utilisent l'axiome d'univalence pour établir une équivalence entre la catégorie sauvage des applications et la catégorie sauvage des familles (types dépendants). Ils prouvent que le produit-pushout et le hom-pullback correspondent à la jonction fibreuse (fiberwise join) et à une construction spécifique de produit dépendant dans la catégorie des familles, où l'adjonction est plus facile à vérifier.

Contributions Clés et Résultats

L'Adjonction de Leibniz (Théorème 3.16) : Le papier prouve que le produit-pushout et le hom-pullback forment une paire adjointe dans la catégorie sauvage des types. Il s'agit d'un résultat technique significatif car, bien que bien connu pour les 1-catégories, prouver cela pour des structures supérieures (même dans le cadre « sauvage ») nécessite une gestion prudente de l'équivalence entre applications et familles pour éviter un enregistrement de cohérence insoluble.
Généralisation des Propriétés des Types de Segal (Théorème 4.9) : En utilisant l'adjonction de Leibniz, les auteurs prouvent que si un type possède des remplisseurs uniques pour les cornes $(2,1)$ $(2, 1)$ (c'est-à-dire qu'il est un type de Segal), il possède automatiquement des remplisseurs uniques pour toutes les cornes intérieures $(n,k)$ $(n, k)$ ( $0 < k < n$ $0 < k < n$ ).
- Cela généralise le résultat de Riehl et Shulman (qui couvrait $n=3$ ) et fournit une version du résultat de Lurie pour la théorie des types simpliciaux.
- La preuve repose sur la démonstration que les inclusions de cornes intérieures $\lambda^n_k$ sont « anodinnes intérieures » (orthogonales à gauche à tous les types de Segal). Ceci est accompli en démontrant que $\lambda^n_k$ est un rétract de le produit-pushout $\lambda^n_k \hat{\times} \lambda^2_1$ , puis en appliquant les propriétés de clôture de l'orthogonalité dérivées de l'adjonction de Leibniz.
Formalisation : Tous les résultats sont formalisés en Cubical Agda. Le code est disponible et sert de vérification des arguments combinatoires complexes impliquant des indices et des pushouts.

Signification et Revendications
Le papier affirme que sa contribution principale est l'internalisation réussie de l'adjonction de Leibniz au sein de la HoTT, ce qui constitue un outil puissant pour dériver les cohérences supérieures dans la théorie des types simpliciaux.

Cadre Synthétique : En travaillant avec un type intervalle interne, les auteurs démontrent que toutes les cohérences supérieures pour les types de Segal peuvent être énoncées et dérivées synthétiquement dans la HoTT, sans recourir à une quantification méta-théorique.
Faisabilité de la Formalisation : Les auteurs soulignent que leur approche permet une formalisation complète dans Agda. Ils notent que si l'approche méta-théorique de Rie–Shulman pourrait rendre l'énoncé du théorème plus facile (en raison du raisonnement basé sur les ensembles au niveau méta), la preuve du cas général dans leur cadre interne est non triviale et a nécessité le développement de l'adjonction de Leibniz pour gérer « l'immense majorité du défi » concernant le suivi de la cohérence.
Utilité Technique : L'équivalence entre la catégorie sauvage des applications et des familles est présentée comme un outil méthodologique crucial qui simplifie les preuves impliquant le produit-pushout et le hom-pullback, rendant la dérivation des propriétés d'orthogonalité réalisable.

En résumé, le papier fournit un fondement rigoureux et formalisé pour la théorie des types simpliciaux, prouvant que la condition de base de Segal implique la pleine cohérence catégorique supérieure grâce à l'application de l'adjonction de Leibniz dans un cadre catégorique sauvage.