Strict stability of extension types

Résumé Technique : Stabilité Stricte des Types d'Extension

Énoncé du Problème
L'article traite d'une lacune fondamentale dans le développement synthétique des $(\infty, 1)$-catégories au sein de la Théorie des Types Homotopiques (HoTT), spécifiquement le système introduit par Riehl et Shulman. Bien que la sémantique de ce système ait été esquissée en utilisant la théorie homotopique simpliciale et le modèle des espaces de Segal, la formulation originale a laissé en suspens la démonstration de la stabilité stricte des types d'extension sous substitution. Dans les modèles de théorie des types, la « stabilité stricte » exige que l'interprétation des formateurs de types (comme les types d'extension) commute strictement avec les carrés de tirés en arrière (substitutions), et non simplement à isomorphisme ou par homotopie. Sans cette propriété, le système ne peut pas être pleinement interprété dans le langage interne d'un $\infty$-topos d'une manière qui supporte l'égalité stricte requise pour certaines théories de catégories internes (par exemple, celles de Martini–Wolf).

Méthodologie
L'auteur emploie la méthode de scission (splitting method) décrite originellement par Voevodsky et plus tard généralisée par Lumsdaine et Warren pour les univers locaux. L'approche implique les étapes techniques suivantes :

1. Catégories d'Univers : Le travail se situe au sein d'une catégorie d'univers (une catégorie $\mathcal{C}$ équipée d'un objet univers $U$ et d'une fibration universelle $\pi: \tilde{U} \to U$). L'auteur suppose l'existence d'une « scission », qui est un choix global de carrés de tirés en arrière pour la fibration universelle. Cela garantit que le réindexage (substitution) est modélisé par l'égalité stricte d'objets et de morphismes, et non par simple isomorphisme.
2. Contextes Génériques : Suivant le style des travaux d'Awodey sur les modèles naturels, le papier définit des contextes génériques (objets classifiants) pour la formation et l'introduction des types d'extension.
   • $U_{\text{Ext}@j}$ est défini comme l'objet classifiant les paires d'une famille de types $A$ et d'une section partielle $a$ sur une inclusion de forme $j: \phi \hookrightarrow \psi$.
   • $U_{\lambda@j}$ est défini comme l'objet classifiant les triplets $\langle A, a, b \rangle$ où $b$ est une extension totale de $a$.
3. Construction de Tiré en Arrière Strict : L'auteur construit le formateur de type d'extension $\text{Ext}@j$ et la fonction d'introduction $\lambda@j$ comme des morphismes entre ces contextes génériques et l'univers. En utilisant la scission de la fibration universelle, le papier démontre que le carré formé par ces applications est un tiré en arrière strict (et non un simple tiré en arrière faible).
4. Hypothèses de Fibrance : Pour simplifier le cadre technique tout en conservant l'applicabilité aux modèles standards (objets simpliciaux dans un $\infty$-topos), l'auteur suppose que les « formes » (les contextes simpliciaux) sont fibrantes. Cela garantit que les cotenseurs de Leibniz sont des fibrations, permettant ainsi de modéliser les types d'extension comme des tirés en arrière catégoriques ordinaires (1-catégoriques).

Contributions Clés et Résultats
La contribution primaire est le Théorème 3.8, qui établit la stabilité stricte des types d'extension. Le théorème prouve que pour un $\infty$-topos de type théorique $\mathcal{E}$ et son modèle simplicial associé $s\mathcal{E}$, une scission fixée des formateurs de types standards produit une interprétation des types d'extension qui satisfait les égalités strictes suivantes pour tout morphisme de contexte $\sigma: \Delta \to \Gamma$ :

1. Stabilité de Formation : $\sigma^*(\text{Ext}@j(A, a)) = \text{Ext}@j(\sigma^*A, \sigma^*a)$
2. Stabilité d'Introduction : $\sigma^*(\lambda@j_{A,a}(b)) = \lambda@j_{\sigma^*A, \sigma^*a}(\sigma^*b)$
3. Stabilité d'Élimination : $\sigma^*(\text{app}@j_{A,a}(f, s)) = \text{app}@j_{\sigma^*A, \sigma^*a}(\sigma^*f, \sigma^*s)$

Le papier détaille ensuite comment les règles de calcul $\beta$ et $\eta$ sont satisfaites au sein de ce cadre strictement stable, en s'appuyant sur la propriété universelle des carrés de tirés en arrière définis par la scission.

Signification et Revendications
Le papier affirme que ce résultat résout le problème ouvert concernant la stabilité stricte des types d'extension dans le système de Riehl–Shulman. La conséquence pratique est que le système possède désormais une sémantique robuste dans les objets simpliciaux d'un $\infty$-topos. Cela permet l'utilisation du système pour prouver des théorèmes sur les $\infty$-catégories internes au sens de Martini–Wolf, car la stabilité stricte garantit que les opérations de type théorique s'alignent parfaitement avec les tirés en arrière catégoriques requis par la théorie des catégories internes.

L'auteur note que bien que le travail suppose un univers unique et des formes fibrantes pour des raisons de simplification technique, le raisonnement est censé se généraliser à des hiérarchies d'univers et des structures fibrées plus complexes sans obstruction essentielle. Ce travail sert de pont entre la syntaxe synthétique de la HoTT simpliciale et la sémantique rigoureuse des $\infty$-topoi.