The notion of 2-pretopos captures, I believe, pretty much everything we need in order to do “elementary” category theory. Its 2-internal logic is also quite convenient, and we can do a lot of category theory in a 2-pretopos?. The notion of Grothendieck 2-topos extends this with infinitary structure, and makes a nice connection with the theory of stacks, i.e. 2-sheaves via the 2-Giraud theorem.
However, “naive” category theory also includes size distinctions, and the study of large versus small categories, and these are not visible in a 2-pretopos. That is, we are interested in 2-categories that are like “the 2-category of large categories,” or perhaps better “the 2-category of locally small categories,” equipped with some information about smallness. These size distinctions are naturally described by the presence of a classifying discrete opfibration. This “feels” kind of analogous to the presence of subobject classifiers in an elementary topos, but the analogy isn’t perfect, because an elementary topos has a classifier for all subobjects, whereas in a 2-category we cannot really expect to classify all discrete opfibrations, only those that are small in some sense.
However, there is a 1-dimensional structure which is like a topos, but which has a classifier not for all subobjects, but for some restricted class of them: namely a quasitopos. It turns out that some of the other axioms one might want to assert in a 2-category of large categories are also quite similar to those for a quasitopos, and also quite similar to those for a category of classes in algebraic set theory. Thus the notion of 2-quasitopos is actually quite an appealing one. Perhaps the existence of the notion of elementary 1-topos at the nexus of Grothendieck 1-topoi and 1-quasitopoi is an accident in 1-dimension, while in higher dimensions the important notions are Grothendieck 2-topos and 2-quasitopos, without necessarily a good notion of “elementary 2-topos.”
A 1-quasitopos can be defined as a 1-category which
has finite limits and colimits,
is locally cartesian closed,
is equipped with a subcategory of monomorphisms, such that
there exists a universal -map, i.e. a map in of which every map in is uniquely a pullback.
A 1-quasitopos is always a Heyting category. It is called solid if it is extensive. It is not generally exact, unless it is an elementary topos, but it is quasi-exact in the sense that every 1-congruence which lies in has an effective quotient. One can in fact prove that must be the class of all regular monics, but from our point of view at the moment this is irrelevant.
Possibly it isn’t stretching the analogy too much to define a (solid) 2-quasitopos to be a 2-category which
has finite colimits,
is equipped with a subcategory of discrete morphisms, such that
there is a classifying discrete opfibration which classifies exactly the discrete opfibrations in ,
every 2-congruence which lies in has an effective quotient, and
the small fibrations and opfibrations are exponentiable.
The structure of a Heyting 2-category, and the “quasi-exactness” property of having quotients for small 2-congruences, are not present in the definition of 1-quasitopos, but since they follow from it, it is not unreasonable to ask for them to remain true in the 2-dimensional case. And the subcategory clearly looks like a version of the subcategory , and the classifying discrete opfibration looks like the strong-subobject classifier of a 1-quasitopos.
Of course exponentials are a 2-categorical version of local cartesian closure. Unfortunately, we can’t expect to simultaneously have all exponentials and also ask for all objects to be locally small (i.e. all inserters to be small). This is seemingly a break with the 1-categorical world in which we can have all exponentials, but still have all equalizers (i.e. all diagonals) be in .
Many 2-quasitopoi have duality involutions. Since those have no counterpart in 1-categories, it’s not entirely clear whether they should be included in the definition. It’s certainly part of what we expect for “doing naive category theory.” However, recall that not every Grothendieck 2-topos has a duality involution. The proof that an exact 2-category with enough groupoids has a duality involution should work here if there are enough groupoids; the “bounded” exactness property should be sufficient. However, I don’t want to assume there are enough groupoids, either, since as in the Grothendieck case, that would eliminate any genuinely 2-categorical examples (i.e. those not constructed from (2,1)-categorical examples).
I actually regard the finite colimits as kind of debatable too. I wonder whether finite colimits are really necessary in the definition of a 1-quasitopos either, or whether quasi-exactness is sufficient.
Note that we have assumed that all inserters are in . This amounts to assuming that all objects are locally small, in the sense that is in . This should be compared with the “bounded exact” setting for algebraic set theory, in which one works in a positive Heyting category with a class of “small maps” such that all diagonals are small and any small congruence has an effective quotient.
(The other setting for algebraic set theory is to work in a Heyting pretopos, so that all congruences have effective quotients, but where not all diagonals are small. If the category is exact and all diagonals are small, then all congruences are small, which is hard to justify in the absence of the separation axiom (which states that all monics are small). One could also formulate a version of this for 2-categories, but in view of the fact that most large categories of interest are locally small, the version we have given seems the most interesting.)
It seems likely that from a suitably structured category of classes , we could construct a 2-quasitopos whose objects are the “locally small” internal categories in .
In the other direction, if is a (solid) 2-quasitopos, then is an extensive Heyting category, and equipped with a pullback-stable subcategory of maps called “small,” such that every small equivalence relation has an effective quotient and every small map is exponentiable. Thus, it looks something like a bounded-exact category of classes. If we construct a classifying cosieve from the classifying discrete opfibration in , and if this cosieve has a core, then that core will classify all the monics in which additionally lie in . Since this class of monics is a pullback-stable subcategory containing all equalizers (those being identifiable with inserters between discrete objects), looks very much like a 1-quasitopos. Or perhaps is more like a 1-quasitopos.
Just as a 2-pretopos is a natural place in which to do elementary category theory (i.e. the theory of small categories), a 2-quasitopos is a natural place in which to do “naive large category theory.”