Aspects of 2-dimensional elementary topos theory

We contribute to expand 2-dimensional elementary topos theory. We focus on the concept of 2-classifier, which is a 2-categorical generalization of the notion of subobject classifier. The idea is that of a discrete opfibration classifier. Interestingly, a 2-classifier can also be thought of as a Grothendieck construction inside a 2-category. We introduce the notion of good 2-classifier, that captures well-behaved 2-classifiers and is closer to the point of view of logic.

We substantially reduce the work needed to prove that something is a 2-classifier. We prove that both the conditions of 2-classifier and what gets classified by a 2-classifier can be checked just over the objects that form a dense generator. This technique allows us to produce a good 2-classifier in prestacks that classifies all discrete opfibrations with small fibres, and to restrict such good 2-classifier to one in stacks. This is the main part of a proof that Grothendieck 2-topoi are elementary 2-topoi. Our results also solve a problem posed by Hofmann and Streicher when attempting to lift Grothendieck universes to sheaves.

To produce our good 2-classifier in prestacks, we present an indexed version of the Grothendieck construction. This gives a pseudonatural equivalence of categories between opfibrations over a fixed base in the 2-category of 2-copresheaves and 2-copresheaves on the Grothendieck construction of the fixed base. Our result can be interpreted as the result that every (op)fibrational slice of a Grothendieck 2-topos is a Grothendieck 2-topos. We thus generalize what is called the fundamental theorem of elementary topos theory to dimension 2, in the Grothendieck topoi case.

In order to reach our theorems of reduction of the study of a 2-classifier to dense generators, we develop a calculus of colimits in 2-dimensional slices. We generalize to dimension 2 the well-known fact that a colimit in a 1-dimensional slice category is precisely the map from the colimit of the domains of the diagram which is induced by the universal property. We explain that we need to consider lax slices, and prove results of preservation, reflection and lifting of 2-colimits for the domain 2-functor from a lax slice. We then study the 2-functor of change of base between lax slices.

Our calculus of colimits in 2-dimensional slices is based on an original concept of colim fibration and on the reduction of weighted 2-colimits to essentially conical ones, which is regulated by the 2-category of elements construction. The latter construction is a natural extension of the Grothendieck construction. We study it in detail from an abstract point of view and we conceive it as the 2-Set-enriched Grothendieck construction, via an original notion of pointwise Kan extension. Our work is relevant to higher dimensional elementary topos theory as well as to a generalization of the Grothendieck construction to the enriched setting.