Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The $\infty$-category of $\infty$-categories in simplicial type theory

Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz

TL;DR

The paper resolves a long-standing foundation gap by constructing the $\infty$-category of $\infty$-categories inside simplicial/triangulated type theory and proving a fully synthetic straightening--unstraightening theorem. It introduces directed univalence for ${\mathsf{Cat}}$, builds a universal cocartesian framework, and demonstrates that ${\mathsf{Cat}}$ is a simplicial, Segal, and Rezk category, thereby modeling $\infty$-categorical structures directly in type theory. The approach relies on modal dependent type theory (MTT) with the $\flat$ modality and an amazing right adjoint to $\mathbb{I}\to -$, yielding a synthetic account of cocartesian fibrations and a robust SHP for constructing new $\infty$-categories. This work provides a self-contained, model-agnostic path from STT to $\infty$-category theory, enabling synthetic development of higher algebra, adjunctions, and reflective subcategories within a unified type-theoretic framework.

Abstract

Simplicial type theory (STT) was introduced by Riehl and Shulman to leverage homotopy type theory to prove results about $(\infty,1)$-categories. Initial work on simplicial type theory focused on "formal" arguments in higher category theory and, in particular, no non-trivial examples of $\infty$-category theory were constructible within STT. More recent work has changed this state of affairs by applying techniques developed initial for cubical type theory to construct the $\infty$-category of spaces. We complete this process by constructing the $\infty$-category of $\infty$-categories, recovering one of the main foundational results of $\infty$-category theory (straightening--unstraightening) purely type-theoretically. We also show how this construction enables new examples of the directed version of the structure identity principle, the structure homomorphism principle.

The $\infty$-category of $\infty$-categories in simplicial type theory

TL;DR

The paper resolves a long-standing foundation gap by constructing the -category of -categories inside simplicial/triangulated type theory and proving a fully synthetic straightening--unstraightening theorem. It introduces directed univalence for , builds a universal cocartesian framework, and demonstrates that is a simplicial, Segal, and Rezk category, thereby modeling -categorical structures directly in type theory. The approach relies on modal dependent type theory (MTT) with the modality and an amazing right adjoint to , yielding a synthetic account of cocartesian fibrations and a robust SHP for constructing new -categories. This work provides a self-contained, model-agnostic path from STT to -category theory, enabling synthetic development of higher algebra, adjunctions, and reflective subcategories within a unified type-theoretic framework.

Abstract

Simplicial type theory (STT) was introduced by Riehl and Shulman to leverage homotopy type theory to prove results about -categories. Initial work on simplicial type theory focused on "formal" arguments in higher category theory and, in particular, no non-trivial examples of -category theory were constructible within STT. More recent work has changed this state of affairs by applying techniques developed initial for cubical type theory to construct the -category of spaces. We complete this process by constructing the -category of -categories, recovering one of the main foundational results of -category theory (straightening--unstraightening) purely type-theoretically. We also show how this construction enables new examples of the directed version of the structure identity principle, the structure homomorphism principle.
Paper Structure (31 sections, 48 theorems, 34 equations)

This paper contains 31 sections, 48 theorems, 34 equations.

Table of Contents

  1. Introduction
  2. Directed univalence and the category of categories
  3. Contributions and outline
  4. Simplicial and triangulated type theory
  5. First steps in triangulated type theory
  6. Multimodal type theory
  7. Modalities in triangulated type theory
  8. Category theory in triangulated type theory
  9. Technical results on iso-inner fibrations
  10. Recollections on cocartesian fibrations
  11. The definition of cocartesian families
  12. The directed gluing of cocartesian families
  13. The universe of amazingly cocartesian types
  14. The category of categories
  15. Classifying cocartesian fibrations
  16. ...and 16 more sections

Key Result

theorem 1.1

${\mathsf{Cat}}$ is the base of the universal cocartesian family, i.e., for any $C \mathrel{:_{\flat}} \mathcal{U}$, we have $\DelimGl{\flat \mid C \to {\mathsf{Cat}}} \simeq \DelimGl{\flat \mid \Sum{E : C \to \mathcal{U}} \mathop{\mathrm{isCocart}}\nolimits\DelimPrn{E}}$.

Theorems & Definitions (66)

  • theorem 1.1
  • corollary 1.0: Directed univalence
  • proposition 2.1
  • definition 2.2
  • definition 2.4
  • definition 2.5
  • remark 2.6
  • proposition 2.8
  • lemma 2.9
  • theorem 2.10
  • ...and 56 more