Speaker
Ivan Kobe, University of Ljubljana
Abstract
We will present an approach to formalising synthetic category theory within CaTT. Since it syntactically recovers weak ω-categories, it provides a convenient language for higher category theory. By interpreting terms of the base type as synthetic categories and terms of hom-types as functors, natural isomorphisms and higher isomorphisms, the derivation rules of CaTT precisely axiomatise coherent functor composition. The aim of this project is to provide a first basis for such an interpretation by extending CaTT with additional derivation rules that postulate the existence of universal constructions such as pullbacks, internal homs, and groupoid cores of synthetic categories. While it is possible to state the fully coherent universal properties of these constructions ‘by hand’, manipulating them quickly leads to the coherence problem. To tame these coherence issues, we are developing a ‘diagram types’ framework that makes extensive use of the BMOSV naturality construction. We will also present our Agda formalisation of this framework.
Joint work with Bastiaan Cnossen.