Strict stability of extension types

Technische Samenvatting: Strikte Stabiliteit van Extensietypen

Probleemstelling
Het artikel behandelt een fundamenteel gat in de synthetische ontwikkeling van $(\infty, 1)$-categorieën binnen de Homotopietheorie (HoTT), specif으로 de door Riehl en Shulman geïntroduceerde systematiek. Hoewel de semantiek van dit systeem werd geschetst met behulp van simpliciale homotopietheorie en de Segal-ruimte-modellen, liet de oorspronkelijke formulering de demonstratie van strikte stabiliteit voor extensietypen onder substitutie open. In typetheoretische modellen vereist deze "strikte stabiliteit" dat de interpretatie van type-vormers (zoals extensietypen) strikt commuteert met pullbacks (substitutie), in plaats van enkel tot isomorfie of homotopie. Zonder deze eigenschap kan het systeem niet volledig worden geïnterpreteerd in de interne taal van een $\infty$-topos op een wijze die de strikte gelijkheid ondersteunt die vereist is voor bepaalde interne categorietheorieën (bijv. die van Martini–Wolf).

Methodologie
De auteur maakt gebruik van de splitsingsmethode (splitting method), oorspronkelijk beschreven door Voevodsky en later gegeneraliseerd door Lumsdaine en Warren voor lokale universa. De aanpak omvat de volgende technische stappen:

1. Universumcategorieën: Het werk is gesitueerd binnen een universumcategorie (een categorie $\mathcal{C}$ uitgerust met een universumobject $U$ en een universele fibratie $\pi: \tilde{U} \to U$). De auteur gaat uit van de existentie van een "splitsing", wat een globale keuze is van pullback-vierkanten voor de universele fibratie. Dit zorgt ervoor dat herindexering (substitutie) wordt gemodelleerd door strikte gelijkheid van objecten en morfismen, niet slechts door isomorfie.
2. Generieke Contexten: In de stijl van het werk van Awodey over natuurlijke modellen, definieert het artikel generieke contexten (classificerende objecten) voor de vorming en introductie van extensietypen.
   • $U_{\text{Ext}@j}$ wordt gedefinieerd als het object dat paren classificeert van een typefamilie $A$ en een gedeeltelijke sectie $a$ over een vorm-inclusie $j: \phi \hookrightarrow \psi$.
   • $U_{\lambda@j}$ wordt gedefinieerd als het object dat triples $\langle A, a, b \rangle$ classificeert waarbij $b$ een totale extensie van $a$ is.
3. Strikte Pullback-constructie: De auteur construeert de extensietype-vormer $\text{Ext}@j$ en de introductiemap $\lambda@j$ als morfismen tussen deze generieke contexten en het universum. Door gebruik te maken van de splitsing van de universele fibratie, demonstreert het artikel dat het vierkant gevormd door deze kaarten een strikte pullback is (niet slechts een zwakke pullback).
4. Fibrantie-aannames: Om de technische setting te vereenvoudigen met behoud van toepasbaarheid op standaardmodellen (simpliciale objecten in een $\infty$-topos), neemt de auteur aan dat de "vormen" (de simpliciale contexten) fibrant zijn. Dit zorgt ervoor dat Leibniz-cotensoren fibraties zijn, waardoor extensietypen gemodelleerd kunnen worden als gewone 1-categorische pullbacks.

Belangrijkste Bijdragen en Resultaten
De primaire bijdrage is Theorema 3.8, dat de strikte stabiliteit van extensietypen vaststelt. Het theorema bewijst dat voor een typetheoretisch model-topos $\mathcal{E}$ en de bijbehorende simpliciale model $s\mathcal{E}$, een vaste splitsing van de standaard type-vormers een interpretatie van extensietypen oplevert die de volgende strikte gelijkheden bevredigt voor elke context-morfisme $\sigma: \Delta \to \Gamma$:

1. Vormingsstabiliteit: $\sigma^*(\text{Ext}@j(A, a)) = \text{Ext}@j(\sigma^*A, \sigma^*a)$
2. Introductiestabiliteit: $\sigma^*(\lambda@j_{A,a}(b)) = \lambda@j_{\sigma^*A, \sigma^*a}(\sigma^*b)$
3. Eliminatiestabiliteit: $\sigma^*(\text{app}@j_{A,a}(f, s)) = \text{app}@j_{\sigma^*A, \sigma^*a}(\sigma^*f, \sigma^*s)$

Het artikel beschrijft verder hoe de $\beta$- en $\eta$-rekenregels worden voldaan binnen dit strikt stabiele kader, leunend op de universele eigenschap van de pullback-vierkanten gedefinieerd door de splitsing.

Betekenis en Claims
Het artikel claimt dat dit resultaat het openstaande probleem betreffende de strikte stabiliteit van extensietypen in de systematiek van Riehl–Shulman oplost. Het praktische gevolg is dat het systeem nu een robuuste semantiek bezit in de simpliciale objecten van een $\infty$-topos. Dit maakt het mogelijk om het systeem te gebruiken om stellingen te bewijzen over interne $\infty$-categorieën in de zin van Martini–Wolf, aangezien de strikte stabiliteit ervoor zorgt dat de typetheoretische operaties perfect overeenkomen met de categorische pullbacks die vereist zijn voor interne categorietheorie.

De auteur merkt op dat hoewel het werk een enkel universum en fibrante vormen veronderstelt voor technische eenvoud, de redenering naar verwachting kan generaliseren naar hiërarchieën van universa en complexere gefibreerde structuren zonder essentiële obstructie. Het werk dient als een brug tussen de synthetische syntaxis van de simpliciale HoTT en de rigoureuze semantiek van $\infty$-topoi.