A type theory for category theory

One of the major draws of working inside of type theory—or any formal system—is the ability to systematically interpret a single proof into a variety of different models, thereby recovering multiple results from a single argument. This methodology leads to "synthetic mathematics": extending type theory with custom axioms to facilitate reasoning in some specific and non-standard model. The most famous example of this approach is homotopy type theory (HoTT), which extends type theory with axioms derived from homotopical models.

In this talk, we explore a synthetic approach to category theory based on Riehl and Shulman's simplicial type theory [1]. In particular, we observe that a handful of axioms and extensions to HoTT give rise to a type theory suitable for synthetic (∞-)category theory—the ∞ is largely silent thanks to the magic of type theory—and argue that proofs in the system are far simpler than their classical counterparts. Results in this talk are joint with Jonathan Weinberger and Ulrik Buchholtz and largely contained in [2] and [3].

[1] https://arxiv.org/abs/1705.07442
[2] https://arxiv.org/abs/2407.09146
[3] https://arxiv.org/abs/2501.13229