The internal languages of univalent categories

Technisches Resümee: Die internen Sprachen univalenter Kategorien

Problemstellung
Sätze über interne Sprachen in der kategorischen Logik etablieren eine Äquivalenz zwischen Syntax (Typentheorien) und Semantik (kategorische Modelle). Ein wegweisendes Resultat von Clairambault und Dybjer [CD14] korrigierte Seelys ursprüngliches Theorem [See84] und etablierte eine Biequivalenz zwischen der Bikategorie der lokal kartesisch abgeschlossenen Kategorien (LCCCs) und der Bikategorie der demokratischen Kategorien mit Familien (CwFs), die extensionalale Identitätstypen, $\Sigma$-Typen und $\Pi$-Typen unterstützen.

Dieses Resultat wurde jedoch innerhalb set-theoretischer Fundamente formuliert. In den univalenten Fundamenten (Homotopietypentheorie) stößt die Standardvorstellung einer CwF auf ein grundlegendes Hindernis: Das Univalenzaxiom impliziert, dass die Typenmenge der Mengen nicht selbst eine Menge ist (sie ist ein 1-Typ). Folglich wird die Anforderung in CwFs, dass die Sammlung der Typen in einem Kontext eine Menge bildet, durch die univalente Kategorie der Mengen verletzt. Darüber hinaus erzeugt die Unterscheidung zwischen „gewählter“ Struktur (z. B. gesplitterte Fibrationen) und „existierender“ Struktur (z. B. Limite bis auf Isomorphie) Kohärenzprobleme in set-theoretischen Fundamenten, die das Auswahlaxiom oder Striktifizierungsverfahren erfordern. In univalenten Fundamenten, in denen Isomorphie Implikation von Identität ist, verschwinden diese Unterscheidungen, aber das bestehende Framework von CwFs ist nicht direkt anwendbar.

Methodik
Die Arbeit entwickelt ein neues Framework für die kategorische Semantik innerhalb der univalenten Fundamente unter Verwendung von univalenten Kategorien und Komprehensionskategorien anstelle von CwFs.

1. Univalente Kategorien: Der Autor arbeitet mit Kategorien, in denen der Identitätstyp von Objekten äquivalent zum Typ der Isomorphien (Adjunktionsequivalenzen) ist. Dies ermöglicht die Behandlung von Adjunktionsequivalenzen als Identitäten, was die Beweise bezüglich der Erhaltung von Strukturen (z. B. Exponentiale) vereinfacht und die Notwendigkeit des Auswahlaxioms zur Auswahl von Limiten eliminiert.
2. Komprehensionskategorien: Um abhängige Typen zu modellieren, ohne die Anforderung zu stellen, dass Typen eine Menge bilden, verwendet das Paper Komprehensionskategorien (basierend auf Fibrationen und Displayed Categories). Eine Komprehensionskategorie besteht aus einer Basiskategorie der Kontexte, einer Displayed Category der Typen, einer Cleaving (die Substitution bereitstellt) und einem Komprehensionsfunktor. Der Autor beschränkt sich auf univalente volle Komprehensionskategorien, bei denen sowohl die Basis als auch die Displayed Category univalent sind.
3. Displayed Bicategories: Die Konstruktion der Bikategorien der Modelle stützt sich stark auf Displayed Bicategories [AFM+21]. Dieser modulare Ansatz ermöglicht es dem Autor, komplexe Bikategorien (wie die von LCCCs oder Topoi mit Universen) aufzubauen, indem Eigenschaften (z. B. endliche Limite, $\Pi$-Typen, Universen) über einfachere Basiskategorien geschichtet werden. Diese Modularität erleichtert den Beweis, dass die resultierenden Bikategorien selbst univalent sind.
4. Lokale Eigenschaften: Um Ergebnisse von Kategorien mit endlichen Limiten auf komplexere Strukturen wie Topoi zu erweitern, adaptiert das Paper Maiettis Begriff der lokalen Eigenschaften [Mai05]. Eine lokale Eigenschaft ist eine Bedingung auf Kategorien, die unter Slicing abgeschlossen sind. Der Autor formalisiert dies innerhalb des Displayed-Bicategory-Frameworks, um Biequivalenzen von der Basisfall (endliche Limite) auf verschiedene Klassen von Topoi zu erweitern.
5. Reindizierung und Universen: Für die Behandlung von Universen verwendet das Paper die Reindizierung von Displayed Bicategories. Diese Technik ermöglicht den Transfer einer Biequivalenz von einer Basiskategorie auf eine Displayed Category über ihr, was die Definition von Universen ermöglicht, die unter spezifischen Typbildnern (z. B. $\Sigma$, $\Pi$, natürliche Zahlen) abgeschlossen sind, ohne dass strikte Stabilitätsgesetze erforderlich sind, sondern vielmehr Stabilität bis auf Isomorphie (was in univalenten Kategorien zu Identität wird).

Zentrale Beiträge
Das Paper leistet vier primäre Beiträge:

1. Univalentes Analogon zu Clairambault-Dybjer: Der Autor konstruiert eine Biequivalenz zwischen der Bikategorie der univalenten Kategorien mit endlichen Limiten und der Bikategorie der univalenten vollen demokratischen endlichen Limit (DFL) Komprehensionskategorien. Dies etabliert, dass die interne Sprache univalenter Kategorien mit endlichen Limiten die extensionale Martin-Löf-Typentheorie mit Unit, binärem Produkt und $\Sigma$-Typen ist.
2. Erweiterung auf lokal kartesisch abgeschlossene Kategorien: Die Biequivalenz wird auf univalente lokal kartesisch abgeschlossene Kategorien und DFL-Komprehensionskategorien erweitert, die $\Pi$-Typen unterstützen. Dies bestätigt, dass die interne Sprache univalenter LCCCs die extensionale Martin-Löf-Typentheorie mit $\Pi$-Typen ist.
3. Erweiterung auf Topoi und Universen: Die Methode wird auf verschiedene Klassen von Topoi (Prätopoi, $\Pi$-Prätoi, elementare Topoi und Topoi mit einem natürlichen Zahlensystem) unter Verwendung lokaler Eigenschaften generalisiert. Des Weiteren definiert der Autor Universen in diesen Kategorien, die unter Typbildnern (natürliche Zahlen, Subobjektklassifikator, propositionale Resizing, $\Sigma$-Typen und $\Pi$-Typen) abgeschlossen sind, und etabliert eine Biequivalenz für elementare Topoi mit einem Universum.
4. Formalisierung: Alle Konstruktionen und Beweise wurden im Rocq Proof Assistant unter Verwendung der UniMath Library formalisiert, was die Korrektheit sicherstellt und eine maschinenprüfbare Referenz für die Theorie bietet.

Resultate
Das Paper beweist, dass für verschiedene Klassen von univalenten Kategorien eine Biequivalenz mit entsprechenden Klassen von univalenten Komprehensionskategorien existiert. Speziell:

• Endliche Limite: Univalente Kategorien mit endlichen Limiten $\simeq$ DFL-Komprehensionskategorien (Unit, Produkt, Äquivalenz, $\Sigma$).
• LCCC: Univalente LCCCs $\simeq$ DFL-Komprehensionskategorien mit $\Pi$-Typen.
• Topoi: Univalente elementare Topoi (mit/ohne NNO) $\simeq$ DFL-Komprehensionskategorien mit entsprechenden lokalen Eigenschaften (z. B. Subobjektklassifikatoren, disjunkte Summen, Quotienten).
• Universen: Univalente elementare Topoi mit einem Universum, das unter spezifischen Typbildnern abgeschlossen ist $\simeq$ DFL-Komprehensionskategorien mit einem Universumsobjekt, das entsprechende Abschlussbedingungen erfüllt.

Das Paper demonstriert, dass in univalenten Fundamenten die interne Sprache dieser kategorischen Strukturen die extensionale Martin-Löf-Typentheorie ist. Die Verwendung univalenter Kategorien vereinfacht die Theorie, da sie die Notwendigkeit gesplitterter Fibrationen und des Auswahlaxioms aufhebt, die in set-theoretischen Fundamenten notwendig sind, um Korrektheit zu gewährleisten; die Kohärenzprobleme, die set-theoretische Modelle plagen (wo Substitution strikt gelten muss), werden gelöst, da Isomorphien Identitäten sind.

Bedeutung und Ansprüche
Das Paper behauptet, dass seine Entwicklung eine neue Perspektive auf die Semantik abhängiger Typentheorie bietet. Durch die Nutzung univalenter Kategorien vermeidet der Autor den technischen Overhead gesplitterter Fibrationen und des Auswahlaxioms, die in set-theoretischen Fundamenten zur Gewährleistung der Korrektheit notwendig sind. Die inhärenten Strukturidentitätsprinzipien in univalenten Fundamenten ermöglichen eine natürlichere Behandlung kategorischer Strukturen, bei denen Objekte bis auf Äquivalenz und nicht bis auf strikte Gleichheit identifiziert werden.

Der Autor stellt explizit klar, dass er nicht die Syntax oder das initiale Modell in dieser Arbeit konstruiert, sondern sich auf die kategorische Seite des internen Sprachsatzes (die Äquivalenz zwischen Modellen) konzentriert. Er merkt an, dass zwar Komprehensionskategorien für univalente Fundamente geeignet sind, andere Strukturen wie CwFs jedoch nicht, aufgrund der Mengenbeschränkung auf Typen. Das Paper positioniert sich als ein fundierter Schritt, der die Entwicklung geeigneter Syntax (wie etwa Gruppenoid-Syntax) und deren Interpretation als zukünftige Arbeit offen lässt. Die Bedeutung liegt darin, eine robuste, maschinenprüfbare Korrespondenz zwischen univalenten kategorischen Strukturen und Typentheorien zu etablieren und zu zeigen, dass univalente Fundamente diese internen Sprachsätze natürlich unterstützen, ohne die Defekte, die in früheren set-theoretischen Formulierungen gefunden wurden.