Abstract: It is well known that the internal language of a 1-dimensional elementary topos is some form of Zermelo-Fraenkel set theory. In 2-dimensions, however, the landscape becomes far less clear. In this talk, I will argue that extending our attention to class categories rather than elementary toposes clarifies the setting, and I will present a 2-categorical version of these which have the property that their internal language is some form of Martin-Löf type theory.
