Ivan Kobe: CaTT – The internal language of ω-categories

Abstract: We will present the type theory CaTT and show that the category of its set-theoretic models is equivalent to the category of Grothendieck-Maltsiniotis ω-categories. Having this type-theoretic handle on the internal language of ω-categories has several advantages: It significantly simplifies the definition of these objects, making it easier to prove results about them, and it offers a good framework for the development of synthetic category theory. If time permits, we will also discuss our ongoing effort to formalize CaTT in Agda.