Bastiaan Cnossen: Synthetic category theory in CaTT

Abstract: Up to now, most approaches to a synthetic theory of categories are based on Martin-Löf type theory (e.g. directed/simplicial type theory). In this talk, I discuss some first explorations for using the type theory CaTT as a basis for synthetic category theory.

The type theory CaTT, developed by Finster and Mimram, captures the internal language of a weak $\omega$-category: a categorical structure with $n$-morphisms for every $n$ with operations satisfying the weakest possible form of coherence laws. Unlike HoTT, CaTT may be interpreted directly within any $(\infty,1)$-category, without need for intricate strictification results. In particular, CaTT has a model given by the $(\infty,1)$-category $\mathsf{Cat}$ of small $(\infty,1)$-categories.

The long-term goal of our project is to enhance CaTT with additional rules capturing the internal language of $\mathsf{Cat}$. In this talk I will focus on a first step: after recalling the basics of CaTT, I will formulate additional rules in CaTT that force its models to be $(\infty,1)$-categories with products, pullbacks and/or internal homs. I will further explain how we hope to extend this in the future.

Everything is joint with Ivan Kobe.