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

TL;DR

This paper constructs the $ abla$-category of $ abla$-categories within simplicial type theory, enabling formal proofs of foundational $ abla$-category theory results purely within type theory.

Contribution

It develops a type-theoretic construction of the $ abla$-category of $ abla$-categories, extending the formal framework for higher category theory in simplicial type theory.

Findings

Constructed the $ abla$-category of $ abla$-categories within STT.

Formalized the straightening--unstraightening equivalence in type theory.

Enabled new examples of the structure identity principle in a directed setting.

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.