The internal languages of univalent categories

Résumé Technique : Les Langages Internes des Catégories Univalentes

Énoncé du Problème
Les théorèmes de langage interne en logique catégorique établissent une équivalence entre la syntaxe (théories des types) et la sémantique (modèles catégoriques). Un résultat séminal de Clairambault et Dybjer [CD14] a corrigé le théorème original de Seely [See84], établissant une biéquivalence entre la bicatégorie des catégories localement cartésiennes closes (LCCC) et la bicatégorie des catégories démocratiques avec familles (CwF) supportant les types d'identité extensionnels, les types $\Sigma$ et les types $\Pi$.

Cependant, ce résultat a été formulé au sein de fondements de la théorie des ensembles. Dans les fondements univalents (Théorie des Types Homotopiques), la notion standard de CwF rencontre un obstacle fondamental : l'axiome d'univalence implique que le type des ensembles n'est pas un ensemble lui-même (c'est un 1-type). Par conséquent, l'exigence des CwF selon laquelle la collection des types dans un contexte forme un ensemble est violée par la catégorie univalente des ensembles. De plus, la distinction entre la structure « choisie » (par exemple, les fibrations scindées) et la structure « existante » (par exemple, les limites à isomorphisme près) crée des problèmes de cohérence dans les fondements de la théorie des ensembles qui nécessitent l'axiome du choix ou des procédures de strictification. Dans les fondations univalentes, où l'isomorphisme implique l'identité, ces distinctions s'évaporent, mais le cadre existant des CwF n'est pas directement applicable.

Méthodologie
L'article développe un nouveau cadre pour la sémantique catégorique au sein des fondations univalentes, en utilisant des catégories univalentes et des catégories de compréhension au lieu des CwF.

1. Catégories Univalentes : L'auteur travaille avec des catégories où le type d'identité des objets est équivalent au type des isomorphismes (équivalences adjointes). Cela permet de traiter les équivalences adjointes comme des identités, simplifiant les preuves concernant la préservation de la structure (par exemple, les exponentielles) et éliminant le besoin de l'axiome du choix pour sélectionner des limites.
2. Catégories de Compréhension : Pour modéliser les types dépendants sans exiger que les types forment un ensemble, l'article adopte des catégories de compréhension (basées sur des fibrations et des catégories affichées). Une catégorie de compréhension consiste en une catégorie de base des contextes, une catégorie affichée des types, un clivage (fournissant la substitution), et un foncteur de compréhension. L'auteur limite son attention aux catégories de compréhension complètes univalentes, où la base et la catégorie affichée sont univalentes.
3. Bicatégories Affichées : La construction des bicatégories de modèles repose largement sur les bicatégories affichées [AFM+21]. Cette approche modulaire permet à l'auteur de construire des bicatégories complexes (comme les LCCC ou les topos avec des univers) en superposant des propriétés (par exemple, limites finies, types $\Pi$, univers) sur des bicatégories de base plus simples. Cette modularité facilite la preuve que les bicatégories résultantes sont elles-mêmes univalentes.
4. Propriétés Locales : Pour étendre les résultats des catégories avec limites finies à des structures plus complexes comme les topos, l'article adapte la notion de propriétés locales de Maietti [Mai05]. Une propriété locale est une condition sur les catégories fermées par tranche (slicing). L'auteur formalise cela au sein du cadre des bicatégories affichées pour étendre les biéquivalences du cas de base (limites finies) vers diverses classes de topos.
5. Réindexation et Univers : Pour le traitement des univers, l'article emploie la réindexation de bicatégories affichées. Cette technique permet de transférer une biéquivalence d'une catégorie de base vers une catégorie affichée sur elle, permettant la définition d'univers fermés sous des formeurs de types spécifiques (par exemple, $\Sigma$, $\Pi$, entiers naturels), non pas en exigeant des lois de stabilité strictes, mais plutôt une stabilité à isomorphisme près (ce qui devient une identité dans les catégories univalentes).

Contributions Principales
L'article apporte quatre contributions principales :

1. Analogue Univalent de Clairambault-Dybjer : L'auteur construit une biéquivalence entre la bicatégorie des catégories univalentes avec limites finies et la bicatégorie des catégories de compréhension DFL (déterminées par des limites finies) univalentes complètes. Cela établit que le langage interne des catégories univalentes avec limites finies est la théorie des types de Martin-Löf extensionnelle avec unité, produit binaire et types $\Sigma$.
2. Extension aux Catégories Localement Cartésiennes Closes : La biéquivalence est étendue aux catégories univalentes localement cartésiennes closes et aux catégories de compréhension DFL supportant les types $\Pi$. Cela confirme que le langage interne des LCCC univalentes est la théorie des types de Martin-Löf extensionnelle avec types $\Pi$.
3. Extension aux Topos et Univers : La méthode est généralisée à diverses classes de topos (prétopos, $\Pi$-prétopos, topos élémentaires, et topos avec objet naturel des entiers) en utilisant des propriétés locales. De plus, l'auteur définit des univers dans ces catégories qui sont fermés sous des formeurs de types (entiers naturels, classificateur de sous-objets, réduction propositionnelle, types $\Sigma$ et types $\Pi$), établissant une biéquivalence pour les topos élémentaires avec un univers.
4. Formalisation : Toutes les constructions et preuves sont formalisées dans l'assistant de preuve Rocq en utilisant la bibliothèque UniMath, garantissant la correction et fournissant une référence vérifiée par machine pour la théorie.

Résultats
L'article prouve que pour diverses classes de catégories univalentes, il existe une biéquivalence avec des classes correspondantes de catégories de compréhension univalentes. Spécifiquement :

• Limites Finies : Catégories univalentes avec limites finies $\simeq$ catégories de compréhension DFL (Unité, Produit, Égaliseur, $\Sigma$).
• LCCC : LCCC univalentes $\simeq$ catégories de compréhension DFL avec types $\Pi$.
• Topos : Topos élémentaires univalents (avec/sans NNO) $\simeq$ catégories de compréhension DFL avec les propriétés locales correspondantes (par exemple, classificateurs de sous-objets, sommes disjointes, quotients).
• Univers : Topos élémentaires univalents avec un univers fermé sous des formeurs de types spécifiques $\simeq$ catégories de compréhension DFL avec un objet univers satisfaisant les conditions de fermeture correspondantes.

L'article démontre que dans les fondations univalentes, le langage interne de ces structures catégoriques est la théorie des types de Martin-Löf extensionnelle. L'utilisation de catégories univalentes simplifie la théorie en supprimant le besoin de fibrations scindées et de l'axiome du choix, car les isomorphismes sont des identités.

Signification et Revendications
L'article affirme que son développement fournit une nouvelle perspective sur la sémantique de la théorie des types dépendants. En utilisant des catégories univalentes, l'auteur évite la surcharge technique des fibrations scindées et de l'axiome du choix, qui sont nécessaires dans les fondations de la théorie des ensembles pour assurer la correction. Les principes d'identité de structure inhérents aux fondations univalentes permettent un traitement plus naturel des structures catégoriques où les objets sont identifiés à équivalence près plutôt que par égalité stricte.

L'auteur déclare explicitement qu'il ne construit pas la syntaxe ou le modèle initial dans ce travail ; il se concentre plutôt sur le côté catégorique du théorème du langage interne (l'équivalence entre les modèles). Il note que bien que les catégories de compréhension soient appropriées pour les fondations univalentes, d'autres structures comme les CwF ne le sont pas, en raison de la restriction sur les ensembles pour les types. Le papier se positionne comme une étape fondamentale, laissant le développement d'une syntaxe appropriée (telle que la syntaxe de groupeïde) et son interprétation comme travaux futurs. La signification réside dans l'établissement d'une correspondance robuste et vérifiée par machine entre les structures catégoriques univalentes et les théories des types, démontant que les fondations univalentes supportent naturellement ces théorèmes de langage interne sans les défauts trouvés dans les formulations antérieures de la théorie des ensembles.