🔢 mathematics

Univalence without function extensionality

Cet article démontre qu'une variante plus faible de l'axiome d'univalence, qualifiée d'« univalence catégorielle », n'implique pas l'extensionnalité des fonctions en analysant la construction de modèles polynomiaux de Von Glehn, qui produit des modèles de la théorie des types de Martin-Löf satisfaisant l'univalence catégorielle tout en réfutant l'extensionnalité des fonctions.

Auteurs originaux : Evan Cavallo, Jonas Höfer

Publié 2026-05-04

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Evan Cavallo, Jonas Höfer

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

La Vue d'Ensemble : La Règle du « Match Parfait »

Imaginez que vous construisez une immense bibliothèque d'objets mathématiques (appelés types). Dans cette bibliothèque, vous avez une règle spéciale appelée Univalence.

Pensez à l'Univalence comme à une règle de « Match Parfait ». Elle dit : Si deux livres dans la bibliothèque sont « équivalents » (ils contiennent les mêmes informations et peuvent être transformés l'un en l'autre), alors ils sont en réalité le même livre.

Pendant longtemps, les mathématiciens ont pensé que cette règle était un package indivisible. Ils croyaient que pour avoir la règle du « Match Parfait », il fallait aussi une deuxième règle appelée Extensionnalité des Fonctions.

L'Extensionnalité des Fonctions est comme une règle pour les recettes. Elle dit : Si deux recettes produisent exactement le même gâteau pour chaque ingrédient que vous y mettez, alors les deux recettes sont la même recette, même si les étapes pour y parvenir semblent différentes sur le papier.

La grande question que pose ce papier est : Peut-on avoir la règle du « Match Parfait » pour la bibliothèque sans avoir la règle de la « Même Recette » ?

La Découverte : Briser le Package Indivisible

Les auteurs, Evan Cavallo et Jonas Höfer, disent Oui, c'est possible.

Ils ont trouvé un moyen de construire un univers mathématique où la règle du « Match Parfait » fonctionne, mais où la règle de la « Même Recette » échoue. Cela signifie que vous pouvez avoir une bibliothèque où les livres équivalents sont identiques, mais où deux recettes différentes qui cuisent le même gâteau sont toujours considérées comme différentes.

Pour prouver cela, ils n'ont pas seulement argumenté avec des mots ; ils ont construit une « machine » spécifique (un modèle mathématique) qui génère ces univers étranges. Ils ont utilisé une construction appelée le Modèle Polynomial (inventé par Von Glehn).

La Machine : L'Usine de « Forme et Position »

Pour comprendre comment leur machine fonctionne, imaginez une usine qui fabrique des jouets.

La Forme : Chaque jouet a une forme principale (comme un cube, une sphère ou une étoile).
La Position : À l'intérieur de la forme, il y a de petits « emplacements » où vous pouvez mettre des pièces supplémentaires.

Dans cette usine, deux jouets sont considérés comme identiques seulement si :

Leurs Formes sont identiques.
Leurs Positions (les emplacements) sont identiques.

Les auteurs ont construit une usine où ils peuvent ajuster les « Positions » indépendamment des « Formes ».

L'Échec de la « Même Recette » (Extensionnalité des Fonctions) : Dans cette usine, vous pouvez avoir deux machines (fonctions) qui prennent une forme et produisent un jouet. Même si les deux machines produisent exactement le même jouet pour chaque entrée, l'usine les considère comme différentes parce que le câblage interne (les positions) des machines est légèrement différent. L'usine refuse de dire : « Oh, elles font le même travail, donc ce sont la même machine. »
Le Succès du « Match Parfait » (Univalence Catégorique) : Cependant, l'usine suit la règle du « Match Parfait » pour la bibliothèque de jouets. Si deux jouets sont équivalents (vous pouvez les échanger dans les deux sens sans rien casser), l'usine accepte qu'ils soient le même jouet.

Le Concept de « Catégorie Sauvage »

Le papier introduit un concept appelé « Catégorie Sauvage ».

Imaginez une aire de jeux chaotique où des enfants (objets) courent partout.

Dans une aire de jeux normale et bien organisée, si deux enfants peuvent échanger leurs places parfaitement, ils sont considérés comme identiques.
Dans cette Catégorie Sauvage, les règles sont un peu plus souples. Les auteurs définissent une version spécifique de la règle du « Match Parfait » appelée Univalence Catégorique. Cette règle ne se soucie que de savoir si vous pouvez échanger les choses dans les deux sens en utilisant des étapes strictes et rigides (comme emboîter des briques Lego), et non des étapes lâches et vacillantes.

Ils ont prouvé que vous pouvez avoir une aire de jeux où cette règle d'« Univalence Catégorique » est vraie, même si la règle de la « Même Recette » (Extensionnalité des Fonctions) est brisée.

Pourquoi Cela Compte-t-il ?

Pendant des années, les mathématiciens ont pensé que la règle du « Match Parfait » (Univalence) était un bloc géant et indivisible. Ils pensaient qu'on ne pouvait pas le démonter.

Ce papier est comme un mécanicien qui démonte un moteur complexe pour montrer que les « bougies d'allumage » (Extensionnalité des Fonctions) et la « pompe à carburant » (Univalence) sont en réalité des pièces séparées. Vous pouvez avoir une voiture qui fonctionne avec la pompe à carburant sans que les bougies d'allumage fonctionnent de la manière que nous attendons habituellement.

Points Clés à Retenir du Papier :

L'Univalence n'impose pas l'Extensionnalité des Fonctions. Vous pouvez avoir l'une sans l'autre.
Le « Package Indivisible » est brisé. Les auteurs ont montré qu'une version plus faible de l'Univalence (appelée Univalence Catégorique) est cohérente avec un monde où l'Extensionnalité des Fonctions est fausse.
L'Outil : Ils ont utilisé une construction mathématique spécifique (le Modèle Polynomial) pour prouver cela. Ce modèle agit comme un filtre qui conserve la règle du « Match Parfait » mais élimine la règle de la « Même Recette ».

Ce Qu'ils N'ont Pas Fait

Le papier est purement théorique. Il ne :

Applique pas cela aux logiciels informatiques ou à l'IA.
Suggère pas comment cela change la façon dont nous écrivons du code aujourd'hui.
Affirme pas qu'une version de la règle est « meilleure » que l'autre pour un usage pratique.

Il répond simplement à une question philosophique profonde en mathématiques : « Ces deux règles sont-elles inséparables ? » La réponse est Non. Elles sont distinctes, et vous pouvez construire un monde où l'une existe sans l'autre.

1. Énoncé du problème

Le papier aborde une question fondamentale en théorie des types homotopique (HoTT) concernant la relation logique entre l'Univalence (UA) et l'Extensionnalité des fonctions (FE).

Contexte : C'est un théorème standard (dû à Voevodsky) que dans tout univers univalent, l'extensionnalité des fonctions vaut. Autrement dit, si deux fonctions sont homotopes ( $f \sim g$ ), elles sont égales ( $f = g$ ).
La question : La réciproque vaut-elle ? Plus précisément, une forme plus faible d'univalence, qui affirme que l'univers forme une « catégorie sauvage univalente » (où l'égalité des types correspond à l'existence d'inverses stricts, c'est-à-dire des équivalences catégorielles), implique-t-elle l'extensionnalité des fonctions ?
Contexte : François G. Dorais a proposé un affaiblissement appelé Univalence catégorielle (CUA), où l'application de l'égalité des types vers l'équivalence catégorielle (applications avec inverses gauche et droit stricts) est une équivalence. Les auteurs examinent si la CUA implique la FE.

2. Méthodologie

Les auteurs emploient la construction de modèle polynomial de Von Glehn ( $Poly(\mathcal{C})$ ) pour construire un contre-exemple. Cette méthode est une source connue de modèles pour la théorie des types de Martin-Löf (ITT) qui réfutent l'extensionnalité des fonctions.

Modèle de base ( $\mathcal{C}$ ) : Ils partent d'un modèle $\mathcal{C}$ de l'ITT satisfaisant l'Univalence et l'Extensionnalité des fonctions (par exemple, un modèle cubique) et possédant des coproduits finis extensifs satisfaisant des règles $\eta$ strictes.
Construction du modèle polynomial : Ils construisent le modèle polynomial $Poly(\mathcal{C})$ $P o l y (C)$ . Dans ce modèle :
- Les types sont des paires $(S, P)$ représentant des « formes » et des « positions ».
- La construction est liée à l'interprétation de Dialectica de Gödel et à la catégorie des conteneurs.
- De manière cruciale, il est établi que $Poly(\mathcal{C})$ réfute toujours la FE.
Analyse des isomorphismes : Le travail technique central consiste à analyser la structure des isomorphismes (équivalences catégorielles) au sein du modèle polynomial. Les auteurs décomposent le type des isomorphismes entre deux types dans le modèle polynomial en :
1. Des isomorphismes entre leurs composantes « forme » (dans le modèle de base $\mathcal{C}$ ).
2. Des isomorphismes entre leurs composantes « position », conditionnés par l'isomorphisme de forme.

3. Définitions et concepts clés

Catégorie sauvage : Une structure capturant la nature $(\infty, 1)$ -catégorielle des types, où la composition et les identités satisfont des lois de cohérence à égalité près (pas nécessairement à homotopie près).
Équivalence catégorielle ( $A \sim= B$ ) : Une application $f: A \to B$ équipée d'inverses gauche et droit stricts ($sf = id, fs = id$). Cela diffère d'une équivalence homotopique ( $A \simeq B$ ), où les inverses n'existent qu'à homotopie près.
Univalence catégorielle (CUA) : Le principe selon lequel l'application $(A = B) \to (A \sim= B)$ est une équivalence.
Univalence catégorielle familiale (CUA $^\bullet$ ) : Une variante plus forte affirmant que pour tout type d'indice $I$ , la catégorie des familles indexées par $I$ est univalente au sens catégoriel.
Décomposition de l'Univalence : Le papier établit que l'Univalence standard (UA) est logiquement équivalente à la conjonction de l'Univalence catégorielle (CUA) et de l'Extensionnalité des fonctions (FE).
$UA \iff (CUA \land FE)$

4. Contributions et résultats clés

A. Indépendance de la CUA et de la FE

Le résultat principal est la preuve que l'Univalence catégorielle familiale n'implique pas l'Extensionnalité des fonctions.

Théorème : $ITT + CUA^\bullet_U \nvdash FE_U$ .
Stratégie de preuve :
1. Prendre un modèle de base $\mathcal{C}$ satisfaisant $UA + FE$.
2. Construire $Poly(\mathcal{C})$ .
3. Préservation de la CUA : Les auteurs prouvent (Théorème 4.17) que si le modèle de base $\mathcal{C}$ satisfait l'Univalence catégorielle familiale, alors le modèle polynomial $Poly(\mathcal{C})$ la satisfait également. Cela repose sur le fait que les isomorphismes dans le modèle polynomial sont déterminés par les isomorphismes dans le modèle de base (formes) et des conditions spécifiques sur les positions qui sont contractiles lorsque le modèle de base est univalent.
4. Réfutation de la FE : C'est une propriété connue des modèles polynomiaux (Proposition 5.3) qu'ils réfutent l'Extensionnalité des fonctions.
5. Conclusion : $Poly(\mathcal{C})$ est un modèle de $ITT + CUA^\bullet_U + \neg FE_U$ .

B. Hiérarchie des variantes de l'Univalence

Le papier explore le paysage des axiomes d'univalence affaiblis, montrant qu'ils ne sont pas tous équivalents :

CUA vs CUA $^\bullet$ : Les auteurs montrent que la CUA (pour un seul univers) n'implique pas l'Univalence catégorielle familiale (CUA $^\bullet$ ). Ils construisent un modèle tranché où la CUA vaut mais où la CUA $^\bullet$ échoue.
Univalence catégorielle catégorielle (CCUA) : Ils définissent une variante où l'application $(A=B) \to (A \sim= B)$ est une équivalence catégorielle plutôt qu'une équivalence homotopique. Ils montrent qu'elle est strictement plus forte que la CUA mais n'implique toujours pas la FE.
Univalence approximative : Ils discutent de l'« univalence approximative » de Van den Berg (existence d'un chemin pour toute équivalence) et notent que sa relation avec la FE reste une question ouverte, bien que les modèles polynomiaux réfutent une « amélioration d'équivalence approximative » connexe.

5. Signification

Découplage des axiomes : Le papier démontre que la propriété « univalente » d'un univers peut être séparée de la propriété « extensionnalité des fonctions ». Cela remet en question l'intuition selon laquelle l'univalence est un axiome monolithique qui force tous les principes d'extensionnalité.
Insight structurel : En montrant que l'Univalence se factorise en Univalence catégorielle et Extensionnalité des fonctions, les auteurs fournissent une compréhension structurelle plus claire de ce qui fait « fonctionner » l'axiome d'univalence. Cela suggère que les fonctions sont « privilégiées » dans l'énoncé standard de l'univalence spécifiquement en raison de l'interaction avec la FE.
Théorie des modèles : Ce travail valide la construction de modèle polynomial comme un outil puissant pour séparer des axiomes subtils en théorie des types, étendant son utilité au-delà de la simple réfutation de la FE vers l'analyse de la structure interne de l'univalence.
Implications fondationnelles : Pour les constructivistes et les chercheurs en fondements, cela suggère qu'on peut adopter une forme d'univalence (univalence catégorielle) qui préserve l'équivalence structurelle des types sans s'engager envers le principe plus fort, historiquement difficile à intégrer, de l'extensionnalité des fonctions.

En résumé, le papier résout la question de Dorais par la négative : l'Univalence catégorielle est strictement plus faible que l'Univalence complète et n'implique pas l'Extensionnalité des fonctions.