elementary (infinity,1)-topos


(,1)(\infty,1)-Category theory

(,1)(\infty,1)-Topos Theory

(∞,1)-topos theory





Extra stuff, structure and property



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 (,1)(\infty,1)-toposes ought to be roughly the larger class of all (,1)(\infty,1)-categories that provide categorical semantics for such homotopy type theory. More precisely, we will define an elementary (,1)(\infty,1)-topos to have the (,1)(\infty,1)-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 (,1)(\infty,1)-topos is that Grothendieck (,1)(\infty,1)-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 (,1)(\infty,1)-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.

Definition (impredicative case)

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 (,1)(\infty,1)-topos is an (,1)(\infty,1)-category E\mathbf{E} 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 (,1)(\infty,1)-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 \infty-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 00 of E\mathbf{E} is strict, i.e. any morphism A0A\to 0 is an equivalence.


Just as for 1-categories, this is true in any cartesian closed (,1)(\infty,1)-category. For if there is a morphism f:A0f:A\to 0 then the projection A×0AA\times 0 \to A has a section (1 A,f)(1_A,f), so that AA is a retract of A×0A\times 0; but A×00A\times 0 \cong 0 by cartesian closedness since (A×)(A\times -) has a right adjoint and hence preserves colimits.


Binary coproducts in E\mathbf{E} are disjoint, i.e. the injections i:AA+Bi:A\to A+B and j:BA+Bj:B\to A+B are monic, and their pullback is initial.


This is also just like a corresponding proof for 1-toposes (see toposes are extensive). Define RR and SS to make the following squares pullbacks:

R r A s S r i A i A+B j B\array{ R & \xrightarrow{r} & A & \xleftarrow{s} & S\\ ^{r'}\downarrow && \downarrow^i && \downarrow\\ A & \xrightarrow{i} & A+B & \xleftarrow{j} & B}

Specifically, (r,r)(r,r') is the kernel pair of ii. In particular, there is an induced diagonal :AR\triangle : A \to R such that r=1 Ar \triangle = 1_A. On the other hand, since E\mathbf{E} is locally cartesian closed, pullback preserves colimits, so (r,s)(r,s) is a coproduct diagram. Thus, the pair of morphisms 1 R:RR1_R:R\to R and s:SR\triangle \circ s : S\to R factor (uniquely) through some h:ARh:A\to R, so that in particular hr=1 Rh r = 1_R. Thus, r:RAr:R\to A has both a left and a right inverse, so it is an equivalence, and hence ii is monic. Dually, jj is monic.

Now we claim that any two morphisms f,g:SXf,g:S\to X with domain SS are equivalent. For the pair of morphisms RrAA+XR \xrightarrow{r} A \to A+X and SfXA+XS \xrightarrow{f} X \to A+X factor uniquely through AA (which, recall, is the coproduct R+SR+S). But since rr is an equivalence, this factorization must be (equivalent to) the left coprojection AA+XA\to A+X. Therefore, the composite SfXA+XS \xrightarrow{f} X \to A+X is equivalent to the composite SsAA+XS \xrightarrow{s} A \to A+X, and similarly so is the composite SgXA+XS \xrightarrow{g} X \to A+X. Since XA+XX\to A+X is monic by the previous paragraph, fgf\simeq g.

Finally, since 00 is a strict initial object, 0S0\to S is monic. And of course 1 S:SS1_S : S\to S is also monic, and these two monomorphisms are classified by two maps f,g:SΩf,g:S\to \Omega into the subobject classifier. By the previous paragraph, fgf\simeq g, hence S0S\cong 0 and is initial.


For any finite family of morphisms {f i:Y iX i} iI\{f_i : Y_i \to X_i\}_{i\in I}, there exists a universe classifying all the f if_i.


Since f if_i is the pullback of if i\sum_i f_i along the injection X i iX iX_i \to \sum_i X_i (this follows from extensivity), a universe classifying if i\sum_i f_i must also classify each f if_i.

In particular, we have “universe cumulativity”:


For any universe p:VUp:V\to U, there is a universe p:VUp':V'\to U' that classifies both pp and U1U\to 1.


All finite colimits are van Kampen.


Since \mathcal{E} is locally cartesian closed, all colimits are pullback-stable, so it suffices to show descent. Suppose DD is a finite simplicial set and F :G :D F^\rhd:G^\rhd:D^\rhd \to \mathcal{E} are colimiting cones under diagrams F,G:DF,G:D\to \mathcal{E}, and let α :FG \alpha^\rhd : F\rhd \to G^\rhd be a natural transformation whose restriction α:FG:D\alpha:F\to G : D\to \mathcal{E} is equifibered. Let p:VUp:V\to U be a universe classifying α d:F dG d\alpha_d : F_d \to G_d for each vertex dD 0d\in D_0. Then α\alpha is the pullback of pp along a cocone q:GUq:G\to U, yielding a cocone r:αpr : \alpha \to p in \mathcal{E}^\to which is equifibered.

Since α \alpha^\rhd is colimiting under α:D \alpha:D\to \mathcal{E}^\to, we have an induced map α p\alpha_\star \to p, where D \star\in D^\rhd is the cocone vertex. But since colimits are pullback-stable, the pullback of G G^\rhd along pp is a colimiting cocone under FF, and hence isomorphic to F F^\rhd. Thus, α \alpha^\rhd is equifibered.


There exists a natural numbers object.

Intuitively, it seems as if Ω(S 1)\Omega(S^1) (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 p:VUp:V\to U 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 (,1)(\infty,1)-topos would have to be proven.

The case n=1n=-1 can be constructed impredicatively using the subobject classifier: internally, A\Vert A \Vert is the smallest truth value implied by AA. Then we can induct on external natural numbers, defining A n+1\Vert A \Vert_{n+1} to be the (1)(-1)-image of the composite AU A(U) AA \to U^A \to (U')^A, where the second map is the nn-truncation. Note that in general it “goes up a universe level”, so that the nn-truncation “goes up n+2n+2 universe levels”. However, unlike type theory, an elementary (,1)(\infty,1)-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 nn-truncation.

However, (Rijke17) shows (again in type theory) that using finite colimits and the natural numbers, the (1)(-1)-truncation can be constructed without raising the universe level. Assuming (as always) that this can be translated into (,1)(\infty,1)-category theory, it implies that we can find object classifiers closed under the (1)(-1)-truncation, and hence (by induction) under the nn-truncation for all nn. Moreover, with a natural numbers object this induction can be performed internally, obtaining in particular object classifiers closed under the nn-truncation for all nn at once.

It seems likely that the construction of W-types in any elementary 1-topos can be repeated in the (,1)(\infty,1)-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 (,1)(\infty,1)-topos. Moreover, it is even unclear exactly what (,1)(\infty,1)-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 (,1)(\infty,1)-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 (,1)(\infty,1)-categorical language.

Definition (predicative case)

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 (,1)(\infty,1)-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

See also

The construction of nn-truncations without recursive HITs is in

The construction of natural numbers from propositional resizing and univalence is in

Revised on April 16, 2017 20:13:51 by Colin Zwanziger (