The internal languages of univalent categories

Technische Samenvatting: De Interne Talen van Univalente Categorieën

Probleemstelling
Stellingen over interne talen in de categorische logica vestigen een equivalentie tussen syntaxis (typetheorieën) en semantiek (categorische modellen). Een fundamenteel resultaat door Clairambault en Dybjer [CD14] corrigeerde de oorspronkelijke stelling van Seely [See84], en vestigde een biequivalentie tussen de bicategorie van lokaal cartesiaans gesloten categorieën (LCCC's) en de bicategorie van democratische categorieën met families (CwF's) die extensieve identiteitstypen, $\Sigma$-typen en $\Pi$-typen ondersteunen.

Dit resultaat werd echter geformuleerd binnen de verzamelingenbouwkundige fundamenten. In univalente fundamenten (Homotopietheorie) stuit het standaardbegrip van CwF op een fundamenteel obstakel: het univalentie-axioma impliceert dat de type van verzamelingen zelf geen verzameling is (het is een 1-type). Bijgevolg wordt de vereiste in CwF's dat de collectie van typen in een context een verzameling vormt, geschonden door de univalente categorie van verzamelingen. Bovendien creëert het onderscheid tussen "gekozen" structuur (bijv. split fibraties) en "bestaande" structuur (bijv. limieten tot isomorfisme) coherentieproblemen in de verzamelingenbouwkundige fundamenten, wat de axioma van keuze of strictificatieprocedures noodzakelijk maakt. In univalente fundamenten, waar isomorfisme identiteit impliceert, vervagen deze onderscheiden, maar het bestaande kader van CwF's is niet direct toepasbaar.

Methodologie
Het artikel ontwikkelt een nieuw kader voor categorische semantiek binnen univalente fundamenten, waarbij gebruik wordt gemaakt van univalente categorieën en comprehensie-categorieën in plaats van CwF's.

1. Univalente Categorieën: De auteur werkt met categorieën waarin het identiteitstype van objecten equivalent is aan het type van isomorfismen (adjuncte equivalenties). Dit maakt het mogelijk om adjuncte equivalenties als identiteiten te behanden, wat het bewijs over het behoud van structuur (bijv. exponentiële functies) vereenvoudigt en de noodzaak voor het axioma van keuze om limieten te selecteren elimineert.
2. Comprehensie-categorieën: Om afhankelijke typen te modelleren zonder de vereiste dat typen een verzameling vormen, hanteert het artikel comprehensie-categorieën (gebaseerd op fibraties en gedisplayde categorieën). Een comprehensie-categorie bestaat uit een basiscategorie van contexten, een gedisplayde categorie van typen, een cleaving (die substitutie levert) en een comprehensie-functor. De auteur beperkt zich tot univalente volledige comprehensie-categorieën, waarbij zowel de basis als de gedisplayde categorie univalent zijn.
3. Gedisplayde Bicategorieën: De constructie van de bicategorieën van modellen steunt zwaar op gedisplayde bicategorieën [AFM+21]. Deze modulaire aanpak stelt de auteur in staat om complexe bicategorieën (zoals die van LCCC's of toposes met universa) te bouwen door eigenschappen (bijv. eindige limieten, $\Pi$-typen, universa) over eenvoudigere basisbicategorieën te leggen. Deze modulariteit vergemakkelijkt het bewijs dat de resulterende bicategorieën zelf univalent zijn.
4. Lokale Eigenschappen: Om resultaten van categorieën met eindige limieten uit te breiden naar complexere structuren zoals toposes, past het artikel de notie van lokale eigenschappen van Maietti [Mai05] aan. Een lokale eigenschap is een conditie op categorieën die gesloten is onder slicing. De auteur formaliseert dit binnen het gedisplayde bicategorie-kader om biequivalenties uit te breiden van de basisgeval (eindige limieten) naar diverse klassen van toposes.
5. Re-indexing en Universa: Voor de behandeling van universa gebruikt het artikel de re-indexing van gedisplayde bicategorieën. Deze techniek maakt het mogelijk om een biequivalentie van een basiscategorie over te dragen naar een gedisplayde categorie over deze, wat de definitie van universa mogelijk maakt die gesloten zijn onder specifieke type-vormers (bijv. $\Sigma$, $\Pi$, natuurlijke getallen), zonder dat strikte stabiliteitswetten nodig zijn, maar eerder stabiliteit tot isomorfisme (wat identiteit wordt in univalente categorieën).

Belangrijkste Bijdragen
Het artikel levert vier primaire bijdragen:

1. Univalent Analoog van Clairambault-Dybjer: De auteur construeert een biequivalentie tussen de bicategorie van univalente categorieën met eindige limieten en de bicategorie van univalente volledige democratische eindige limiet (DFL) comprehensie-categorieën. Dit vestigt dat de interne taal van univalente categorieën met eindige limieten extensieve Martin-Löf type-theorie is met unit, binaire product en $\Sigma$-typen.
2. Uitbreiding naar Lokaal Cartesiaans Gesloten Categorieën: De biequivalentie wordt uitgebreid naar univalente lokaal cartesiaans gesloten categorieën en DFL comprehensie-categorieën die $\Pi$-typen ondersteunen. Dit bevestigt dat de interne taal van univalente LCCC's extensieve Martin-Löf type-theorie is met $\Pi$-typen.
3. Uitbreiding naar Toposes en Universa: De methode wordt gegeneraliseerd naar diverse klassen van toposes (pretoposes, $\Pi$-pretoposes, elementaire toposes en toposes met een natuurlijk getallenobject) met behulp van lokale eigenschappen. Verder definieert de auteur universa in deze categorieën die gesloten zijn onder type-vormers (natuurlijke getallen, subobject classifier, propositionele resizing, $\Sigma$-typen en $\Pi$-typen), waarmee een biequivalentie wordt vastgesteld voor elementaire toposes met een universum.
4. Formalisering: Alle constructies en bewijzen zijn geformaliseerd in de Rocq proof assistant met behulp van de UniMath library, wat de correctheid garandeert en een machine-gecontroleerde referentie voor de theorie biedt.

Resultaten
Het artikel bewijst dat er voor diverse klassen van univalente categorieën een biequivalentie bestaat met corresponderende klassen van univalente comprehensie-categorieën. Specifiek:

• Eindige Limieten: Univalente categorieën met eindige limieten $\simeq$ DFL comprehensie-categorieën (Unit, Product, Equalizer, $\Sigma$).
• LCCC: Univalente LCCC's $\simeq$ DFL comprehensie-categorieën met $\Pi$-typen.
• Toposes: Univalente elementaire toposes (met/zonder NNO) $\simeq$ DFL comprehensie-categorieën met corresponderende lokale eigenschappen (bijv. subobject classifiers, disjoint sums, quotients).
• Universa: Univalente elementaire toposes met een universum dat gesloten is onder specifieke type-vormers $\simeq$ DFL comprehensie-categorieën met een universe-object dat aan de corresponderende afsluitingscondities voldoet.

Het artikel demonstreert dat in univalente fundamenten de interne taal van deze categorische structuren extensieve Martin-Löf type-theorie is. Het gebruik van univalente categorieën vereenvoudigt de theorie door de noodzaak van split fibraties en het axioma van keuze weg te nemen, die nodig zijn in verzamelingenbouwkundige fundamenten om de deugdelijkheid te garanderen. De coherentieproblemen die de verzamelingenmodellen (waar substitutie strikt moet zijn) teisteren, worden opgelost omdat isomorfismen identiteiten zijn.

Betekenis en Claims
Het artikel claimt dat de ontwikkeling een nieuw perspectief op de semantiek van afhankelijke type-theorie biedt. Door gebruik te maken van univalente categorieën vermijdt de auteur de technische overhead van split fibraties en het axioma van keuze, die in verzamelingenbouwkundige fundamenten noodzakelijk zijn om de deugdelijkheid te waarborgen. De structurele identiteitsprincipes inherent aan univalente fundamenten maken een natuurlijkere behandeling mogelijk van categorische structuren waarbij objecten worden geïdentificeerd op basis van equivalentie in plaats van strikte gelijkheid.

De auteur stelt expliciet dat hij niet de syntaxis of het initiële model construeert in dit werk; in plaats daarvan richt hij zich op de categorische zijde van de interne taal-stelling (de equivalentie tussen modellen). De auteur merkt op dat hoewel comprehensie-categorieën geschikt zijn voor univalente fundamenten, andere structuren zoals CwF's dat niet zijn, vanwege de verzameling-restrictie op typen. Het artikel positioneert zichzelf als een fundamentele stap, waarbij de ontwikkeling van geschikte syntaxis (zoals groepoid-syntaxis) en de interpretatie daarvan als toekomstig werk wordt gelaten. De betekenis ligt in het vestigen van een robuuste, machine-gecontroleerde correspondentie tussen univalente categorische structuren en type-theorieën, en het aantonen dat univalente fundamenten deze interne taal-stellingen natuurlijk ondersteunen zonder de gebreken die in eerdere verzamelingenbouwkundige formuleringen werden gevonden.