💻 computer science

Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory

Cet article construit des modèles d'ensembles matériels non bien fondés dans la Théorie des Types Homotopiques qui satisfont les axiomes d'anti-fondation de Scott et d'Aczel via les M-types et les coalgèbres terminales, étend ces axiomes aux niveaux de types supérieurs au sein de la Théorie des Ensembles Matériels Univalents, et fournit une caractérisation des types d'identité des M-types, l'ensemble des résultats étant formalisé dans Agda.

Auteurs originaux : Hakon Robbestad Gylterud, Elisabeth Stenholm, Niccolò Veltri

Publié 2026-07-01

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Hakon Robbestad Gylterud, Elisabeth Stenholm, Niccolò Veltri

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

L'idée générale : Construire un univers d'ensembles « tourbillonnants »

Imaginez que vous construisez un univers d'objets (des ensembles). Selon la méthode traditionnelle de la mathématique (appelée théorie des ensembles « bien fondée »), chaque objet est construit à partir d'objets plus petits, qui sont eux-mêmes construits à partir d'objets encore plus petits, et ainsi de suite jusqu'au néant. C'est comme une pyramide : vous ne pouvez pas avoir un bloc flottant dans les airs ; il doit reposer sur quelque chose en dessous de lui.

Mais et si vous vouliez construire un univers où les choses peuvent reposer sur elles-mêmes ? Et si vous aviez une boîte qui se contient elle-même ? Ou une chaîne de boîtes où la Boîte A est à l'intérieur de la Boîte B, qui est à l'intérieur de la Boîte C, qui est à l'intérieur de la Boîte A ? Dans les mathématiques traditionnelles, cela est interdit car cela crée une boucle infinie. Dans cet article, les auteurs explorent comment construire un univers mathématique qui autorise ces boucles, en utilisant un cadre moderne appelé Théorie des Types Homotopiques (HoTT).

L'article fait deux choses :

Il construit un modèle d'ensembles qui autorise les boucles, en suivant les règles établies par un mathématicien nommé Scott.
Il construit un modèle différent d'ensembles qui autorise les boucles, en suivant les règles établies par un mathématicien nommé Aczel.

Les outils : Arbres, Coalgèbres et « déploiement »

Pour comprendre leurs modèles, imaginez un arbre.

Les arbres bien fondés (l'ancienne méthode) sont comme des arbres généalogiques. Ils ont une racine, des branches, et finissent par des feuilles. Ils cessent de croître.
Les arbres non bien fondés (la nouvelle méthode) peuvent être comme un fractale ou une galerie des glaces. Une branche peut boucler et redevenir la racine. Ou une branche peut se diviser en deux branches identiques qui ressemblent exactement à l'arbre entier.

Les auteurs utilisent un concept appelé Coalgèbre pour décrire ces arbres. Considérez une coalgèbre comme une « machine » qui vous dit comment regarder un nœud et voir ce qui vient après.

Si la machine dit « stop », vous avez une feuille.
Si la machine dit « va vers ces enfants », vous avez des branches.
Si la machine dit « va vers un enfant qui est en fait toi-même », tu as une boucle.

L'article pose la question suivante : Quelle est la machine « ultime » capable de décrire toutes les boucles possibles ?

Les deux modèles : Scott vs Aczel

Les auteurs construisent deux « machines ultimes » différentes (modèles mathématiques) pour gérer ces boucles. Elles correspondent à deux philosophies différentes sur la manière de traiter l'égalité dans ces mondes bouclés.

1. Le modèle « Miroir » (L'axiome de non-fondation de Scott)

L'analogie : Imaginez une galerie des glaces. Si vous vous tenez devant un miroir, vous voyez un reflet. Si ce reflet est dans un autre miroir, vous voyez un reflet d'un reflet.
La règle : Dans ce modèle, deux objets sont considérés comme « égaux » si leurs schémas de déploiement se ressemblent. Si vous continuez à ouvrir les couches d'un ensemble (comme éplucher un oignon ou déployer un arbre), et que le schéma des branches est identique à un autre ensemble, alors ils sont les mêmes.
Le résultat : Les auteurs ont construit un type spécifique de structure d'arbre (appelé $V^0_\infty$ ) qui sert de modèle à cela. C'est un « point fixe », ce qui signifie que si vous appliquez les règles de l'univers à celui-ci, vous obtenez le même univers en retour.
Résultat clé : Ce modèle n'est pas la machine « finale » ou « terminale » au sens strict. C'est une « troisième option » — ce n'est ni le point de départ (initial) ni le point final absolu (terminal). Il se situe entre les deux. Il satisfait les règles de Scott, qui sont plus strictes sur la manière dont les boucles sont identifiées.

2. Le modèle « Universel » (L'axiome de non-fondation d'Aczel)

L'analogie : Imaginez un catalogue maître de toutes les histoires possibles que vous pourriez raconter, y compris les histoires qui se racontent elles-mêmes.
La règle : Dans ce modèle, n'importe quel graphe (un dessin de points et de lignes) peut être transformé en un ensemble. Si vous avez le dessin d'une boucle, il existe un ensemble unique qui correspond parfaitement à ce dessin.
Le résultat : Les auteurs ont construit une « Coalgèbre Terminale » (la machine ultime) à cette fin. Cependant, pour construire cette machine spécifique, ils ont dû utiliser un outil mathématique spécial et quelque peu controversé appelé Redimensionnement Propositionnel (Propositional Resizing).
- Qu'est-ce que le Redimensionnement Propositionnel ? Imaginez une immense bibliothèque de livres (propositions). Cet outil vous permet de rétrécir toute la bibliothèque pour qu'elle tienne sur une seule étagère, sans perdre aucune des histoires. C'est un raccourci puissant qui rend la construction possible.
Résultat clé : Ce modèle satisfait les règles d'Aczel. C'est l'objet « terminal », ce qui signifie qu'il s'agit de la version la plus complète possible d'un univers d'ensembles en boucle.

L'énigme de l'identité : Qu'est-ce qui rend deux choses identiques ?

Une grande partie de l'article consiste à résoudre un puzzle complexe : Comment savoir si deux arbres bouclés sont réellement les mêmes ?

Dans les mathématiques standards, si deux choses se ressemblent, elles sont égales. Mais dans un monde de boucles, les choses deviennent étranges.

Les auteurs ont découvert que l'« égalité » entre deux points dans leurs arbres bouclés peut être décrite comme un autre type d'arbre (un « M-type indexé »).
La métaphore : Imaginez que vous comparez deux fractales infinies. Pour prouver qu'elles sont les mêmes, vous ne regardez pas seulement l'image entière ; vous devez comparer chaque branche, chaque sous-branche, et chaque sous-sous-branche. L'article fournit une recette précise (une « caractérisation ») pour effectuer cette comparaison. Ils ont prouvé que l'« égalité » de ces boucles complexes est elle-même un objet structuré et infini.

Résumé des accomplissements

Le modèle de Scott : Ils ont construit un univers d'ensembles qui autorise les boucles, où l'égalité est déterminée par la forme de l'arbre de « déploiement ». Ce modèle est un point fixe mais pas absolument « terminal ».
Le modèle d'Aczel : Ils ont construit l'univers « ultime » d'ensembles qui autorise les boucles, où n'importe quel graphe peut être transformé en un ensemble. Cela a nécessité une hypothèse mathématique spéciale (le Redimensionnement Propositionnel).
La recette de l'« Égalité » : Ils ont déterminé exactement comment définir la « similitude » pour ces structures infinies et bouclées, montrant que l'égalité est simplement un autre type de structure d'arbre.
Formalisation : Ils n'ont pas seulement écrit cela sur papier ; ils l'ont construit à l'intérieur d'un programme informatique appelé Agda, qui vérifie chaque étape logique pour s'assurer qu'il n'y a pas d'erreurs.

Pourquoi est-ce important ?

L'article ne prétend pas résoudre des problèmes d'ingénierie du monde réel ou des questions médicales. Au contraire, il résout un puzzle fondamental en mathématiques. Il montre que nous pouvons construire un univers cohérent et logique où les « cercles » et les « boucles » sont autorisés, en utilisant le langage moderne de la Théorie des Types Homotopiques. Il comble le fossé entre la théorie classique des ensembles (qui interdit les boucles) et la logique moderne de l'informatique (qui doit gérer des structures de données circulaires complexes comme les flux de données ou les systèmes de transition).

En bref : ils ont construit deux « univers » différents où les choses peuvent se contenir elles-mêmes, ont prouvé qu'ils fonctionnent selon des règles spécifiques, et ont montré exactement comment déterminer si deux de ces choses auto-contenues sont réellement les mêmes.

Résumé Technique : Coalgebres Terminaux et Ensembles Non-Bien-Fondés en Théorie des Types Homotopiques

Énoncé du Problème
L'article traite du défi que représente la modélisation d'ensembles matériels non bien-fondés au sein de la Théorie des Types Homotopiques (HoTT). Alors que les ensembles bien-fondés ont été modélisés avec succès dans HoTT en utilisant des types inductifs supérieurs (où l'égalité est le type d'identité), la modélisation des ensembles non bien-fondés — des ensembles qui peuvent se contenir eux-mêmes ou former des chaînes d'appartenance infinies — a historiquement reposé sur des setoids (où l'égalité est une relation binaire distincte) plutôt que sur le type d'identité. Les auteurs visent à construire des modèles d'ensembles non bien-fondés dans HoTT où l'égalité est interprétée strictement comme le type d'identité, intégrant ainsi les notions classiques de la coalgèbre universelle et de la théorie des ensembles non bien-fondés dans les structures de dimension supérieure supportées par HoTT. Plus précisément, l'article cherche à construire des coalgebres terminaux pour des foncteurs de parties restreints afin de modéliser l'axiome de non-fondation d'Aczel (AFA) et à construire des points fixes alternatifs modélisant l'axiome de non-fondation de Scott (SAFA).

Méthodologie
Les auteurs utilisent le cadre de la Théorie des Ensembles Matériels Univalents et la théorie des coalgebres pour les endofoncteurs sauvages sur l'univers des types. La méthodologie repose sur trois approches techniques principales :

Dualisation des Ensembles Itératifs : Les auteurs construisent une hiérarchie de types $V^n_\infty$ en dualisant la construction des ensembles itératifs ( $V^n$ ). Tandis que $V^n$ est l'algèbre initiale du foncteur de parties restreint $P^n$ , $V^n_\infty$ est construit comme un sous-type spécifique du M-type (le coalgebra terminal du foncteur de parties non restreint $P^\infty$ ). Ce sous-type est défini par un prédicat coinductif garantissant que les applications de branchement à chaque nœud sont tronquées à un niveau spécifique.
Caractérisation des Types d'Identité : Une étape technique cruciale consiste à caractériser les types d'identité des M-types. Les auteurs prouvent que le type d'identité entre deux éléments d'un M-type est équivalent à un M-type indexé (spécifiquement, le coalgebra terminal d'un foncteur polynomial indexé dérivé du « dépliage » d'une relation). Cette caractérisation est essentielle pour prouver la petiteur localité (local smallness) des modèles construits.
Adaptation de la Construction d'Aczel–Mendler : Pour construire un véritable coalgebra terminal pour le foncteur de parties restreint $P^0$ $P^{0}$ (qui modélise l'AFA), les auteurs adaptent le théorème classique d'Aczel–Mendler à la théorie des types. Cette adaptation nécessite de :
- Définir des foncteurs « basés sur U » (des foncteurs dont les valeurs sur les types larges sont des colimites de valeurs sur des types petits).
- Utiliser le relèvement de relation (relation lifting) et le concept de « précongruences » pour quotienter le coalgebra faiblement terminal.
- Supposer le redimensionnement propositionnel (propositional resizing) pour garantir que les types quotients résultants sont localement petits et que la construction tient pour les foncteurs à valeurs d'ensembles comme $P^0$ .

Contributions Clés et Résultats

Un Modèle de l'Axiome de Non-Fondation de Scott (SAFA) : Les auteurs construisent un type $V^0_\infty$ qui est un point fixe du foncteur de parties restreint $P^0$ , mais qui n'est ni l'algèbre initiale ni le coalgebra terminal. Ils prouvent que ce type, équipé de la relation d'appartenance induite, satisfait l'axiome de non-fondation de Scott. Dans ce modèle, l'égalité est le type d'identité, et le modèle est « simple » (tout morphisme vers lui est égal) mais non terminal.
Généralisation aux Types Supérieurs : La construction est généralisée à une hiérarchie $V^n_\infty$ pour tout niveau de troncature $n$ . Ces modèles satisfont les axiomes $k$ -SAFA généralisés pour tout $k \le n$ . L'article démontre que ces modèles satisfont les axiomes standards de la théorie des ensembles (ensemble vide, séparation, union, etc.) aux niveaux de troncature appropriés, à condition que les modèles soient localement petits.
Caractérisation des Types d'Identité des M-types : L'article fournit une caractérisation complète du type d'identité des M-types en tant que M-types indexés (Théorème 2.15). Ce résultat est utilisé pour prouver que les modèles construits sont localement petits, une condition nécessaire pour qu'ils servent de modèles valides de la théorie des ensembles matériels dans HoTT.
Un Modèle de l'Axiome de Non-Fondation d'Aczel (AFA) : En supposant l'axiome de redimensionnement propositionnel, les auteurs construisent un coalgebra terminal pour le foncteur de parties restreint $P^0$ (et plus généralement pour les foncteurs basés sur $U$ ). Ce coalgebra terminal sert de modèle de l'AFA d'Aczel, où chaque graphe possède une décoration unique.
Non-Terminalité de $V^0_\infty$ : L'article démontre explicitement que $V^0_\infty$ n'est pas le coalgebra terminal pour $P^0$ . Il fournit un contre-exemple montrant que des morphismes de coalgebra distincts peuvent exister à partir d'un graphe spécifique vers $V^0_\infty$ , le distinguant du coalgebra terminal construit via la méthode d'Aczel–Mendler.

Signification et Revendications
L'article affirme fournir les premiers modèles d'ensembles matériels non bien-fondés dans HoTT où l'égalité est le type d'identité, dépassant ainsi les modèles basés sur les setoids du passé.

Distinction entre AFA et SAFA : Le travail clarifie la relation entre les axiomes de non-fondation d'Aczel et de Scott (AFA et SAFA) dans le contexte de HoFF. Il montre que si le coalgebra terminal (nécessitant le redimensionnement propositionnel) valide l'AFA, le point fixe co-itératif (constructible sans redimensionnement) valide le SAFA. Les auteurs notent que dans le cas non tronqué ( $\infty$ ), l'AFA et le SAFA coïncident, mais qu'ils divergent aux niveaux de troncature inférieurs.
Nature Constructive : La construction du modèle SAFA ( $V^n_\infty$ ) est entièrement constructive et ne repose pas sur des axiomes impredicatifs comme le redimensionnement propositionnel.
Formalisation : Tous les principaux résultats sont formalisés dans l'assistant de preuve Agda, utilisant à la fois l'Agda standard et le Cubical Agda (pour la section 6), assurant la correction des arguments homotopiques complexes.
Questions Ouvertes : Les auteurs notent modestement que l'existence du coalgebra terminal pour $P^0$ sans redimensionnement propositionnel reste une question ouverte. Ils ne prétendent pas avoir résolu si une telle construction est possible ou si son existence implique des principes classiques, mais soulignent cela comme une motivation primaire pour des travaux futurs.

En résumé, l'article étend avec succès la théorie des ensembles non bien-fondés au cadre de dimension supérieure de HoTT, fournissant des modèles distincts pour différents axiomes de non-fondation et établissant le socle technique nécessaire concernant les M-types et les structures de coalgebra.