structures in a cohesive (∞,1)-topos
The notion of an elementary (∞,1)-topos is an analogue of the notion of elementary topos in (∞,1)-category theory. This is in contrast to the notion of a Grothendieck (∞,1)-topos equivalent to an (∞,1)-category of (∞,1)-sheaves, the analogue of a sheaf topos, which is more specific (see geometric homotopy type theory).
Note that every Grothendieck (∞,1)-topos provides categorical semantics for homotopy type theory with univalent weakly-Tarskian types of types and also higher inductive types (HITs). Elementary -toposes ought to be roughly the larger class of all -categories that provide categorical semantics for such homotopy type theory. More precisely, we will define an elementary -topos to have the -categorical structure that ought to correspond to that type-theoretic structure; a coherence theorem making it actually model the corresponding type theory is still unknown.
In general, the problem with “elementary-izing” the notion of -topos is that Grothendieck -toposes have many properties that are not reflected in type theory due to the finitary nature of type theory; the question is to find appropriate “finitary shadows” of them. For instance, one can construct initial algebras for endofunctors using a transfinite induction argument; thus in type theory we postulate the existence of inductive types. Deciding what class of “infinitary constructions” that are available in Grothendieck -toposes can be described finitarily by something that deserves the name “higher inductive type” is overall an open question, but we can obtain reasonable definitions by restricting the class of HITs we ask for.
There are at least two ambiguities in the above sketch of a definition based on type theory: what exactly do we assume of the universes, and what general class of HITs do we ask for? One reasonable answer to the universe question is that every object should be contained in a universe closed under all the relevant operations, and one reasonable answer to the HITs question is just the non-recursive ones. This leads to the following definition.
An elementary -topos is an -category such that
Note that this definition is “impredicative” just like an elementary topos, in that it has a classifier for all subobjects. We can’t categorify this to a classifier for all objects due to size paradoxes; the existence of “enough” object classifiers closed under all the basic operations is the “next best thing”. We will refer to an object classifier satisfying (2) above as a universe.
It is reasonable to hope for a coherence theorem showing that any elementary -topos in the above sense admits a model of homotopy type theory with non-recursive HITs (corresponding to the the finite colimits), univalent universes (perhaps only weakly Tarski ones), and propositional resizing?. See, for instance, model of type theory in an (infinity,1)-topos and relation between type theory and category theory – Univalent homotopy type theory and infinity-toposes.
In an elementary 1-topos we can construct finite colimits and dependent exponentials from non-dependent exponentials and the subobject classifier (or equivalently from power objects). In the -case this seems less likely to be true, since subobjects tell us less about objects that are not 0-truncated. However, there is still a good deal of extra structure that “comes for free” from the above definition.
The initial object of is strict, i.e. any morphism is an equivalence.
Just as for 1-categories, this is true in any cartesian closed -category. For if there is a morphism then the projection has a section , so that is a retract of ; but by cartesian closedness since has a right adjoint and hence preserves colimits.
Binary coproducts in are disjoint, i.e. the injections and are monic, and their pullback is initial.
This is also just like a corresponding proof for 1-toposes (see toposes are extensive). Define and to make the following squares pullbacks:
Specifically, is the kernel pair of . In particular, there is an induced diagonal such that . On the other hand, since is locally cartesian closed, pullback preserves colimits, so is a coproduct diagram. Thus, the pair of morphisms and factor (uniquely) through some , so that in particular . Thus, has both a left and a right inverse, so it is an equivalence, and hence is monic. Dually, is monic.
Now we claim that any two morphisms with domain are equivalent. For the pair of morphisms and factor uniquely through (which, recall, is the coproduct ). But since is an equivalence, this factorization must be (equivalent to) the left coprojection . Therefore, the composite is equivalent to the composite , and similarly so is the composite . Since is monic by the previous paragraph, .
Finally, since is a strict initial object, is monic. And of course is also monic, and these two monomorphisms are classified by two maps into the subobject classifier. By the previous paragraph, , hence and is initial.
For any finite family of morphisms , there exists a universe classifying all the .
Since is the pullback of along the injection (this follows from extensivity), a universe classifying must also classify each .
In particular, we have “universe cumulativity”:
For any universe , there is a universe that classifies both and .
All finite colimits are van Kampen.
Since is locally cartesian closed, all colimits are pullback-stable, so it suffices to show descent. Suppose is a finite simplicial set and are colimiting cones under diagrams , and let be a natural transformation whose restriction is equifibered. Let be a universe classifying for each vertex . Then is the pullback of along a cocone , yielding a cocone in which is equifibered.
Since is colimiting under , we have an induced map , where is the cocone vertex. But since colimits are pullback-stable, the pullback of along is a colimiting cocone under , and hence isomorphic to . Thus, is equifibered.
There exists a natural numbers object.
Intuitively, it seems as if (which can be constructed using finite limits and colimits) ought to be the integers and we should be able to construct the natural numbers from it; but it is unclear to the authors of this page how to do that. Instead, we can (using the impredicative subobject classifier) define the smallest subobject of an object classifier that contains the initial object and is closed under taking coproducts with the terminal object. This is almost right, but it is not 0-truncated. We could 0-truncate it, but to get a universal property relative to all objects rather than only 0-truncated ones, we can instead impose structure making the objects rigid, such as a partial order or a graph. This argument is formalized in type theory here; to be precise either it would have to be translated manually into category-theoretic language, or the above conjecture about interpreting type theory in an elementary -topos would have to be proven.
There is an (n-connected, n-truncated) factorization system.
The case can be constructed impredicatively using the subobject classifier: internally, is the smallest truth value implied by . Then we can induct on external natural numbers, defining to be the -image of the composite , where the second map is the -truncation. Note that in general it “goes up a universe level”, so that the -truncation “goes up universe levels”. However, unlike type theory, an elementary -topos has no globally chosen tower of universes, so this doesn’t literally make sense to say. What we can say is that with this construction, it is not clear whether we can find object classifiers that are closed under the -truncation.
However, (Rijke17) shows (again in type theory) that using finite colimits and the natural numbers, the -truncation can be constructed without raising the universe level. Assuming (as always) that this can be translated into -category theory, it implies that we can find object classifiers closed under the -truncation, and hence (by induction) under the -truncation for all . Moreover, with a natural numbers object this induction can be performed internally, obtaining in particular object classifiers closed under the -truncation for all at once.
It seems likely that the construction of W-types in any elementary 1-topos can be repeated in the -case.
There is some structure that the definition probably does not imply, namely a semantic counterpart of arbitrary recursive higher inductive types, such as arbitrary localization. It is certain that these cannot always be constructed in an elementary 1-topos: for instance, HITs imply that all (even infinitary) algebraic theories have initial algebras, whereas this cannot be proven in ZF without the axiom of choice (under appropriate large cardinal hypotheses). Thus, it seems very unlikely that they can be constructed in an elementary -topos. Moreover, it is even unclear exactly what -categorical structure should correspond to arbitrary higher inductive types, not least because we lack an accepted general definition of an “arbitrary HIT”.
However, although this is an open question, it is arguably not a question about the definition of “elementary -topos”, but some stronger notion, analogous to a stronger notion of 1-topos that lacks an accepted name. Moreover, a great deal of homotopy type theory (including synthetic homotopy theory) can be done with only non-recursive HITs, truncations, and a natural numbers type, and even in the absence of a general coherence theorem any particular result of HoTT could probably be explicitly written down in -categorical language.
Since there is no consensus even on the definition of predicative 1-topos, it seems less likely that there is a definitive answer for a predicative -topos. However, it should probably include at least the following axioms (which as we have seen above, are all true in the impredicative case although not included in the definition):
Note that the stronger universe axiom implies, as above, that finite colimits are van Kampen, and in particular therefore that finite coproducts are disjoint. Instead of strengthening this axiom, we could assume explicitly that finite coproducts are disjoint, and then repeat the proof of descent given above.
A vague version of the above proposed definition is on the very last slide of
The construction of -truncations without recursive HITs is in
The construction of natural numbers from propositional resizing and univalence is in