Der Umgang mit schwachen unendlichdimensionalen Kategorien stellt selbst für Expert*innen eine Herausforderung dar. Dies begründet sich schon auf grundsätzlicher Ebene damit, dass die Sprache der Mengenlehre nicht invariant unter den Äquivalenzbegriffen dieser schwachen, höherdimensionalen Strukturen ist, wie z.B. Homotopieäquivalenz. Unter diesem Gesichtspunkt ist es naheliegend, nach einer alternativen Grundlagentheorie zu suchen, die mit den homotopietheoretischen Begriffen besser kompatibel ist.

Ein möglicher Ansatz wurde 2017 von Riehl–Shulman in Form einer synthetischen Theorie von (∞,1)-Kategorien vorgeschlagen. Zu diesem Zweck haben sie eine Erweiterung der sogenannten Homotopie-Typentheorie bzw. univalenten Grundlagen (engl. homotopy type theory/univalent foundations (HoTT/UF)) eingeführt. Hierbei handelt es sich um ein logisches System, entscheidend geprägt durch Wojewodski, das eine synthetische Grundlage für Homotopietheorie bieten soll: Die grundlegenden Objekte tragen bereits eine topologische Struktur. Genauer gesagt, handelt es sich um Homotopietypen. Wojewodskis Univalenz-Axiom bewirkt, dass in diesem System Homotopieäquivalenz mit logischer Äquivalenz übereinstimmt. Dies hat zur Folge, dass viele konzeptionelle Ideen aus der klassischen Homotopietheorie benutzt werden können, um eine synthetische Theorie aufzubauen.

Ein entscheidender Beitrag wurde 2019 von Shulman geleistet, der bewies, dass jeder höherdimensionale Topos (im Sinne von Grothendieck–Rezk–Lurie) Anlass zu einem Modell von Homotopie-Typentheorie gibt. Diese Vermutung war lange Zeit offen. Nach diesem Resultat kann man HoTT in einem genauen technischen Sinne als eine Art interne Sprache beliebiger (∞,1)-Topoi ℰ verstehen. Analog dazu lässt sich Riehl–Shulmans Erweiterung, die sog. simpliziale Homotopietypentheorie (sHoTT), in Diagramm-(∞,1)-Topoi der Form ℰ^(Δ^op) interpretieren. Vermöge syntaktischer Erweiterungen erlaubt die Theorie die Behandlung interner (∞,1)-Kategorien, modelliert durch sogenannte (vollständige) Segal-Objekte.

Ausgehend von Riehl–Shulmans Arbeit über synthetische (∞,1)-Kategorien und diskrete kovariante Fibrationen entwickeln wir eine Theorie ko-/kartesischer Fibrationen, die auch gefaserte und zweiseitige Verallgemeinerungen erfasst. Dabei dienen Riehl–Veritys Arbeiten über modellunabhängige (∞,1)-Kategorientheorie als wichtige Grundlage, deren Resultate für ∞-Kosmoi wir auf den typentheoretischen Kontext übertragen. Wir geben Charakterisierungssätze für kokartesische Fibrationen und ihre Verallgemeinerungen an, die als Existenzsätze bestimmter adjungierter Funktoren formuliert sind (Chevalley-Kriterien). Gemeinsame Vorarbeiten mit Buchholtz verallgemeinernd zeigen wir eine Auswahl von Abschlusseigenschaften zweiseitiger kartesischer Fibrationen sowie ein zweiseitiges Yoneda-Lemma. Desweiteren diskutieren wir sogenannte Beck–Chevalley-(Bi-)Fibrationen und beweisen eine synthetische (∞,1)-kategorielle Version des Satzes von Moens, basierend auf einem Beweis von Streicher.

Abschließend führen wir eine Kohärenzkonstruktion für Riehl–Shulmans strikte Erweiterungstypen durch, sodass diese auch in den homotopietheoretischen Topos-Modellen strikt substitutionsstabil interpretiert werden können. Diese Methode geht auf Wojewodski zurück und fand Anwendung in Arbeiten von z.B. Kapulkin, Lumsdaine, Warren, Awodey, Streicher und Shulman.

Unsere Arbeit folgt Vorschlägen aus dem ursprünglichen Artikel von Riehl–Shulman, die synthetische (∞,1)-Kategorientheorie in simplizialer Homotopie-Typentheorie weiterzuentwickeln, insbesondere bezüglich kokartesischer Fibrationen. Zusammen mit einer Reihe analytischer Resultate, v.a. von Riehl–Verity und Rasekh, folgt aus den genannten Betrachtungen, dass unser typentheoretischer Zugang eine synthetische Theorie von Fibrationen interner (∞,1)-Kategorien darstellt.