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 this problem relates to the problem of dealing with sizes in higher toposes, and argue that by extending our attention to class categories rather than elementary toposes clarifies the setting, precisely because they incorporate size considerations. I will present a (2,1)-categorical version of these which have the property that their internal language is a strong form of Martin-Löf type theory. See the slides here.
