Polynomial Universes in Homotopy Type Theory

1. Problématique : La tension entre strictesse et cohérence

L'article s'attaque au problème fondamental de la sémantique catégorique de la théorie des types dépendants.

• Le défi de la strictesse : Dans la syntaxe de la théorie des types, la substitution est strictement associative et satisfait strictement la condition de Beck-Chevalley. Cependant, dans les modèles catégoriques classiques (basés sur la théorie des ensembles ou les topos 1-catégoriques), ces opérations ne sont définies que « à isomorphisme près » (via des produits fibrés/pullbacks). Pour modéliser correctement la syntaxe, il faut que ces identités tiennent strictement, ce qui est difficile à garantir dans des catégories générales.
• La limite des modèles naturels : Awodey et Newstead ont résolu ce problème en introduisant les modèles naturels, où les types sont classifiés par un univers $U$ (une application $u : U^\bullet \to U$). Ils ont montré que la structure de ces modèles correspond à des foncteurs polynomiaux formant des pseudo-monoïdes (ou pseudomonades) dans une catégorie de foncteurs polynomiaux.
• Le compromis actuel : Pour gérer les identités « à isomorphisme près » (les cohérences supérieures) inhérentes aux structures faibles, Awodey et Newstead ont dû construire une tricatégorie complexe de foncteurs polynomiaux. Cela sort du cadre usuel de la catégorie des foncteurs polynomiaux, rendant la théorie lourde et difficile à manipuler.

L'objectif de l'article est de résoudre cette impasse en axiomatisant entièrement la sémantique des modèles naturels au sein de la catégorie usuelle des foncteurs polynomiaux, en évitant la nécessité de passer à des structures de catégories supérieures explicites (comme les tricatégories).

2. Méthodologie : Le cadre de la Théorie des Types Homotopique (HoTT)

Les auteurs adoptent une approche synthétique en travaillant internement dans le langage de la Théorie des Types Homotopique (HoTT).

• Changement de paradigme : Au lieu de travailler dans un topos 1-catégorique (comme $\mathbf{Set}^{\mathcal{C}^{op}}$), ils travaillent dans un $\infty$-topos (représenté par $\infty\mathbf{Grpd}^{\mathcal{C}^{op}}$). Dans ce cadre, les identités et les cohérences de haut niveau sont gérées nativement par la théorie des types elle-même.
• Foncteurs Polynomiaux dans HoTT : Un foncteur polynomial $P$ est défini comme une somme de foncteurs co-représentables :
  $$P(y) = \sum_{a:A} y^{B[a]}$$
  où $A$ est un type (les positions) et $B$ est une famille de types (les directions).
• Lenses et Cartésianité : Les morphismes entre foncteurs polynomiaux sont les lenses (paires de cartes avant et arrière). Une lens est dite cartésienne si la carte arrière est une équivalence. Les foncteurs polynomiaux munis de lenses cartésiennes forment une sous-catégorie $\mathbf{Poly}_{Cart}$.
• L'axiome d'Univalence : La clé de la méthode est l'utilisation de l'axiome d'univalence de HoTT. Un foncteur polynomial $u$ est dit univalent (ou un univers polynomial) si l'ensemble des lenses cartésiennes vers $u$ est un propre proposition (c'est-à-dire qu'il y a au plus une telle lens, à égalité près).

3. Contributions Clés et Résultats

A. Définition des Univers Polynomiaux

Les auteurs définissent un univers polynomial comme un foncteur polynomial univalent dans $\mathbf{Poly}_{Cart}$.

• Théorème 4.1 (Cohérence des sommes dépendantes) : Si un univers polynomial $u$ possède des lenses cartésiennes $\eta : y \to u$ (pour le type unité) et $\mu : u \triangleright u \to u$ (pour les sommes dépendantes $\Sigma$), alors $u$ porte naturellement la structure d'un $\infty$-monade.
  • Résultat majeur : Grâce à l'univalence, tous les diagrammes de cohérence (associativité, lois d'unité) commutent automatiquement. On n'a pas besoin de spécifier manuellement les données de cohérence supérieures (les cellules d'homotopie) ; elles sont déduites de l'unicité des morphismes cartésiens vers un objet univalent.

B. Le Foncteur $\Rightarrow$ et les Types Dépendants ($\Pi$)

Pour traiter les types fonctionnels dépendants ($\Pi$), les auteurs introduisent un nouveau foncteur $\Rightarrow$ (noté $\Uparrow$ dans le texte) agissant sur les foncteurs polynomiaux :
$$p \Rightarrow q = \sum_{(a, f): \prod_{a:A} C} y^{\prod_{b:B[a]} D[f(b)]}$$
Ce foncteur capture la structure des types $\Pi$.

• Lien avec les lois de distributivité : L'existence d'une lens cartésienne $\pi : u \Rightarrow u \to u$ (fermeture sous $\Pi$) implique l'existence d'une loi de distributivité pour la monade $u$ sur elle-même.
• Théorème 4.2 : Si $u$ est un univers polynomial fermé sous $\Sigma$ et $\Pi$, alors il existe une loi de distributivité $\aleph : u \triangleright u \to u \triangleright u$ qui satisfait les diagrammes de distributivité (DL1-DL4).
  • Mécanisme de preuve : Les auteurs généralisent la notion de distributivité aux distributeurs (morphisms entre produits tensoriels de foncteurs). Ils montrent que la loi de distributivité induite par $\pi$ correspond à un morphisme cartésien vers $u$. Par univalence, ce morphisme est unique, forçant ainsi la commutativité de tous les diagrammes de distributivité et de leurs cohérences supérieures.

C. Exemples et Applications

• Monades de partialité : Les auteurs montrent que les monades de partialité (proof-relevant partiality) sont des exemples d'univers polynomiaux.
• Complétion de Rezk et Ensembles Finis : Ils appliquent la complétion de Rezk (un concept de HoTT pour rendre les catégories univalentes) à la monade des listes ($List$).
  • La monade $List$ n'est pas univalente (les types de listes ne sont pas des groupoïdes univalents de manière naturelle).
  • Sa complétion de Rezk, notée $Rezk(List)$, correspond à l'univers des ensembles finis de Bishop.
  • Résultat surprenant : Bien que $List$ ne possède pas de loi de distributivité stricte sur elle-même (en raison de l'absence de commutativité stricte des permutations), $Rezk(List)$ en possède une. Cela fait de $Rezk(List)$ un analogue catégorique supérieur de la monade de l'anneau commutatif libre, où les identités sont respectées à homotopie près (cohérence des permutations).

4. Signification et Impact

1. Simplification Théorique : L'article démontre qu'il n'est pas nécessaire de sortir de la catégorie des foncteurs polynomiaux pour modéliser la théorie des types dépendants avec toutes ses cohérences supérieures. L'axiome d'univalence de HoTT permet de « compresser » toute la hiérarchie de données de cohérence (nécessaire dans une approche 1-catégorique stricte ou une approche de tricatégories) en une seule propriété : l'univalence.
2. Unification : Il unifie la théorie des modèles naturels (Awodey/Newstead) avec la théorie des catégories supérieures et l'algèbre des foncteurs polynomiaux.
3. Formalisabilité : Une contribution pratique majeure est la formalisation complète des résultats principaux dans l'assistant de preuve Agda. Cela valide la rigueur des constructions et offre un point de départ pour l'implémentation de vérificateurs de types basés sur ces principes.
4. Nouvelles Structures Algébriques : L'article révèle de nouvelles structures algébriques dans le monde des foncteurs polynomiaux, notamment la relation entre les lois de distributivité des monades et la fermeture sous les types $\Pi$, ouvrant la voie à l'étude d'algèbres supérieures (comme les anneaux commutatifs en théorie des types).

En résumé, ce papier propose un cadre élégant où la complexité des identités faibles en théorie des types est gérée non pas par des structures catégoriques externes complexes, mais par les propriétés intrinsèques de l'univalence au sein de la catégorie des foncteurs polynomiaux.