nLab (infinity,1)Topos



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

(∞,1)-topos theory

structures in a cohesive (∞,1)-topos



By (,1)Topos(\infty,1)Topos is denoted the collection of all (∞,1)-toposes. This is the (∞,1)-category-theory analog of Topos.


(,1)Topos(\infty,1)\,Topos is the (non-full) sub-(∞,1)-category of (∞,1)Cat on (∞,1)-toposes and (∞,1)-geometric morphisms between them.

Morally, this should actually be an (∞,2)-category, just as Topos is a 2-category, but since the technology of (,2)(\infty,2)-categories is not well developed, this point of view is not often taken yet.


In the following, (,1)Cat(\infty,1)Cat will refer to the (superlarge) (,1)(\infty,1) category of large (,1)(\infty, 1)-categories.

Existence of sites of definition


Existence of limits and colimits

We discuss existence of (∞,1)-limits and (∞,1)-colimits in (,1)Topos(\infty,1)Topos.


The (,1)(\infty,1)-category (,1)Topos(\infty,1)Topos has all small (,1)(\infty,1)-colimits and functor

(,1)Topos op(,1)Cat (\infty,1)Topos^{op} \to (\infty,1)Cat

preserves small limits.

This is HTT, prop. In the notation there, LTopLTop is the (,1)(\infty,1)-category of toposes whose arrows are the inverse image morphisms, and thus opposite to (,1)Topos(\infty,1)Topos.


The (,1)(\infty,1)-category (,1)Topos(\infty,1)Topos has filtered (∞,1)-limits and the inclusion

(,1)Topos(,1)Cat (\infty,1)Topos \to (\infty,1)Cat

preserves these.

This is HTT, prop.


The (,1)(\infty,1)-category (,1)Topos(\infty,1)Topos has all small (∞,1)-limits.

This is HTT, prop.


The (,1)(\infty,1)-limits in (,1)Topos(\infty,1)Topos coincide actually with the proper (,2)(\infty,2)-limits.

This is HTT, remark


The terminal object in (∞,1)Topos is ∞Groupoids.

This is HTT, Prop., for details see at terminal geometric morphism.

Computation of limits and colimits

We discuss more or less explicit descriptions of (∞,1)-limits and (∞,1)-colimits in (,1)Topos(\infty,1)Topos.



𝒳 (g *g *) 𝒴 (f *f *) 𝒵 \array{ && \mathcal{X} \\ && \downarrow^{\mathrlap{(g^* \dashv g_*)}} \\ \mathcal{Y} &\stackrel{(f^* \dashv f_*)}{\to}& \mathcal{Z} }

be a diagram of (∞,1)-toposes. Then its (∞,1)-pullback is computed, roughly, by the (∞,1)-pushout of their (∞,1)-sites of definition (see above).

More in detail: there exist (∞,1)-sites 𝒟˜\tilde \mathcal{D}, 𝒟\mathcal{D}, and 𝒞\mathcal{C} with finite (∞,1)-limit and morphisms of sites

𝒟 g 𝒟˜ f 𝒞 \array{ && \mathcal{D} \\ && \uparrow^{\mathrlap{g}} \\ \tilde \mathcal{D} &\stackrel{f}{\leftarrow}& \mathcal{C} }

such that

( 𝒳 (g *g *) 𝒴 (f *f *) 𝒵)( Sh (,1)(𝒟) (Lan g()g) Sh (,1)(𝒟˜) (Lan f()f) Sh (,1)(𝒞)). \left( \array{ && \mathcal{X} \\ && \downarrow^{\mathrlap{(g^* \dashv g_*)}} \\ \mathcal{Y} &\stackrel{(f^* \dashv f_*)}{\to}& \mathcal{Z} } \right) \,\,\, \simeq \,\,\, \left( \array{ && Sh_{(\infty,1)}(\mathcal{D}) \\ && \downarrow^{\mathrlap{(Lan_g \dashv (-)\circ g)}} \\ Sh_{(\infty,1)}(\tilde \mathcal{D}) &\stackrel{(Lan_f \dashv (-)\circ f)}{\to}& Sh_{(\infty,1)}(\mathcal{C}) } \right) \,.

Let then

𝒟˜ 𝒞𝒟 f 𝒟 g g 𝒟˜ f 𝒞(,1)Cat lex \array{ \tilde \mathcal{D} \coprod_{\mathcal{C}} \mathcal{D} &\stackrel{f'}{\leftarrow}& \mathcal{D} \\ {}^{\mathllap{g'}}\uparrow &\swArrow_{\simeq}& \uparrow^{\mathrlap{g}} \\ \tilde \mathcal{D} &\stackrel{f}{\leftarrow}& \mathcal{C} } \,\,\,\,\, \in (\infty,1)Cat^{lex}

be the (∞,1)-pushout of the underlying (∞,1)-categories in the full sub-(∞,1)-category (∞,1)Cat lex(,1)Cat{}^{lex} \subset (\infty,1)Cat of (,1)(\infty,1)-categories with finite (,1)(\infty,1)-limits.

Let moreover

Sh (,1)(𝒟˜ 𝒞𝒟)PSh (,1)(𝒟˜ 𝒞𝒟) Sh_{(\infty,1)}(\tilde \mathcal{D} \coprod_{\mathcal{C}} \mathcal{D}) \hookrightarrow PSh_{(\infty,1)}(\tilde \mathcal{D} \coprod_{\mathcal{C}} \mathcal{D})

be the reflective sub-(∞,1)-category obtained by localization at the class of morphisms generated by the inverse image Lan f()Lan_{f'}(-) of the coverings of 𝒟\mathcal{D} and the inverse image Lan g()Lan_{g'}(-) of the coverings of 𝒟˜\tilde \mathcal{D}.


Sh (,1)(𝒟˜ 𝒞𝒟) 𝒳 (g *g *) 𝒴 (f *f *) 𝒵 \array{ Sh_{(\infty,1)}(\tilde \mathcal{D} \coprod_{\mathcal{C}} \mathcal{D}) &\to& \mathcal{X} \\ \downarrow &\swArrow_{\simeq}& \downarrow^{\mathrlap{(g^* \dashv g_*)}} \\ \mathcal{Y} &\stackrel{(f^* \dashv f_*)}{\to}& \mathcal{Z} }

is an (∞,1)-pullback square.

This is HTT, prop.

Colimits of over-toposes


For any (,1)(\infty,1) topos H\mathbf{H}, there is a colimit preserving functor H(,1)Topos\mathbf{H} \to (\infty,1)Topos sending an object XX to its over-topos H /X\mathbf{H}_{/X}, and sending an arrow f:XYf : X \to Y to the essential geometric morphism f *:H /XH /Yf_* : \mathbf{H}_{/X} \to \mathbf{H}_{/Y}.


HTT, Prop. implies the “terminal vertex” Cartesian fibration H [1]H\mathbf{H}^{[1]} \to \mathbf{H} is classified by a limit preserving functor H opPr L\mathbf{H}^{op} \to Pr^L, the (,1)(\infty,1)-category of locally presentable (,1)(\infty,1)-categories and colimit-preserving functors between them.

This functor factors through the subcategory (,1)Topos opPr L(\infty,1)Topos^{op} \subseteq Pr^L that sends a geometric morphism to its inverse image part. By [HTT, Prop.] and [HTT, Prop.], it follows that this is also a limit preserving functor.

The opposite category is then formed by taking right adjoints.

  • Topos

  • (,1)(\infty,1)Topos


section 6.3 in

category: category

Last revised on October 18, 2021 at 08:30:34. See the history of this page for a list of all contributions to it.