Simplicial type theory (STT) was introduced by Riehl and Shulman to leverage homotopy type theory to prove results about (∞,1)-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 initially 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.

Riehl and Shulman [1] introduced simplicial type theory (STT), a variant of homotopy type theory which aimed to study not just homotopy theory, but its fusion with category theory: (∞, 1)-category theory. While notoriously technical, manipulating ∞-categories in simplicial type theory is often easier than working with ordinary categories, with the type theory handling infinite stacks of coherences in the background. We capitalize on recent work by Gratzer et al. [2] defining the (∞, 1)-category of ∞-groupoids in STT to define presheaf categories within STT and systematically develop their theory. In particular, we construct the Yoneda embedding, prove the universal property of presheaf categories, refine the theory of adjunctions in STT, introduce the theory of Kan extensions, and prove Quillen’s Theorem A. In addition to a large amount of category theory in STT, we offer substantial evidence that STT can be used to produce difficult results in ∞-category theory at a fraction of the complexity.

Formalized 1-category theory forms a core component of various libraries of mathematical proofs. However, more sophisticated results in fields from algebraic topology to theoretical physics, where objects have “higher structure,” rely on infinite-dimensional categories in place of 1-dimensional categories, and ∞-category theory has thusfar proved unamenable to computer formalization.

Abstract This paper explain how the geometric notions of local contractibility and properness are related to the $\Sigma$ -types and $\Pi$ -types constructors of dependent type theory. We shall see how every Grothendieck fibration comes canonically with such a pair of notions—called smooth and proper maps—and how this recovers the previous examples and many more. This paper uses category theory to reveal a common structure between geometry and logic, with the hope that the parallel will be beneficial to both fields. The style is mostly expository, and the main results are proved in external references.