Michael Shulman What is a 2-topos

What is a 2-topos?

Of course, a 2-topos is the 2-categorical version of a topos. In other words, it is a (vertically) categorified topos. However, as we know, categorification, like quantization and groupoidification, is an art rather than a science; it depends on deciding what the crucial properties are of the thing we want to categorify.

The problem is especially acute for toposes, because of their many-faceted nature. To speak figuratively, which attributes of an elephant do we want to categorify? It isn’t even necessarily clear that there is a single beast which decategorifies to all the aspects of an elephant at once; perhaps we have 2-legs, 2-trunks, 2-ears, 2-tails, and so on but no actual 2-elephant.

According to WeberYS2T,

• a 2-topos is a finitely complete 2-category which is cartesian closed and has a duality involution and a classifying discrete opfibration.

This is evidently a categorification of a definition such as

• a topos is a finitely complete category which is cartesian closed and has a subobject classifier.

On the other hand, according to StreetCBS,

• a 2-topos is a 2-category which is equivalent to the 2-category of stacks (2-sheaves) on some 2-site.

This is evidently a categorification of a definition such as

• a topos is a category which is equivalent to the category of sheaves on some site.

The definition I propose to categorify is

• a topos is a locally cartesian closed, finitely complete and cocomplete Heyting pretopos with a subobject classifier.

Of course, this definition contains a good deal of redundancy, but not all of that was apparent in the early days of topos theory, and there seems less reason to believe that the redundancy will remain under categorification. Moreover, for the purposes of logic, having a Heyting pretopos is the most important part of the definition; it is what enables the internal interpretation of first-order logic. (Local cartesian closure and a subobject classifier then enable the interpretation of higher-order logic.) It may be simply an accident that in the 1-categorical case, the higher-order structure automatically implies the first-order structure.

Thus, in order to obtain an internal logic of a 2-category, it is natural to start with a notion of Heyting 2-pretopos. This is especially attractive because it is less clear how to categorify the “higher-order structure” of local cartesian closure and a subobject classifier. The 2-category Cat, which one expects to be the prototypical 2-topos just as Set is the prototypical topos, does not have a subobject classifier, nor is it locally cartesian closed (though it is cartesian closed). What is true is that fibrations are exponentiable, and that it has objects (namely, full subcategories of $Set$) that classify some discrete opfibrations.

Another guiding desideratum for us will be that all the notions we consider should be stable under slicing, just like the corresponding 1-categorical notions. For instance, this demands the upgrading of ordinary cartesian closure to some sort of local cartesian closure. However, in the 2-categorical case it turns out that usually the correct notion to consider is not the slice 2-category but rather the fibrational slice.

Thus, the proposed definition we will arrive at will be something like:

• an (elementary) 2-topos is a finitely complete and cocomplete Heyting 2-pretopos with exponentials and (some sort of discrete opfibration classifier).

The goal, again, is to find a notion of 2-topos that has an internal logic in which we can reason about categories. Street’s “Grothendieck 2-toposes” turn out to have (almost) all of these properties of an “elementary 2-topos.” The intersection of this notion with Weber’s consists of finite limits, cartesian closure (strictly weaker than our notion of “exponentials”), and a discrete fibration classifier. While some of our 2-toposes admit duality involutions, others (perhaps surprisingly) do not.