Def (Rezk): A (Grothendieck) homotopy topos is a homotopy left exact Bousfield localization of the model category of simplicial presheaves sPsh(C) on a small simplicial category C.

Thm (Rezk): A presentable model category E is a (Grothendieck) homotopy topos iff it has descent.

Note: A (Grothendieck) topos is a presentable elementary topos.


Is there some homotopical definition of an elementary topos?

Are there some references for (approaches, attacks...) Elementary "homotopy" topos?

Motivation: Generalize Elementary "homotopy" topos to Elementary higher topos in analogy to Higher topos theory (à la Lurie, Rezk).


Sheaves in geometry and logic, an intro to topos theory. Maclane and Moerdijk.

Toposes and homotopy toposes, Rezk.

  • 4
    $\begingroup$ To the best of my knowledge, there are proposals but I do not think that there is a definition on which everyone agrees. See ncatlab.org/nlab/show/elementary+%28infinity,1%29-topos $\endgroup$ Commented Dec 11, 2015 at 21:00
  • 2
    $\begingroup$ I'd say that it is a locally cartesian closed $(\infty,1)$-category, such that the groupoid of fibrations satisfies descent. There are two problems: what is its internal logic and what exactly is meant by descent (since with an arbitrary elementary topos it is difficult to talk about diagram size). The best version of the second condition that I can state is that the functor $X\mapsto E/X: E^{op} \to Top$ is absolutely flat (a substitute for representability). The first condition should be satisfied by some version of HoTT (not the current one, it is interpretable only in model categories). $\endgroup$ Commented Dec 11, 2015 at 23:53
  • $\begingroup$ @AntonFetisov To clarify, what is meant by "absolutely flat functor"? $\endgroup$ Commented Jan 12, 2017 at 15:52
  • 1
    $\begingroup$ See the last slide of Mike Shulman's talk:(home.sandiego.edu/~shulman/hottminicourse2012/04induction.pdf) $\endgroup$ Commented Jan 12, 2017 at 15:59
  • $\begingroup$ @CharlesRezk, a functor $C \to Type$ is absolutely flat if it is $\alpha$-flat for any regular cardinal $\alpha$. An $\alpha$-flat functor is the one which is an $\alpha$-filtered colimit of representables, or equivalently which has an $\alpha$-cofiltered category of elements. $\alpha$-filtered is the same as filtered with finite sets swapped for $\alpha$-finite sets. See [Handbook of categorical algebra I. Basic category theory, p. 271]. I suppose we can just use $\alpha$-filtered 1-categories since the type theory, being a set of formulas, is naturally 1-categorical. (cont..) $\endgroup$ Commented Jan 12, 2017 at 16:53

1 Answer 1


Since the time when Denis referred in the comments to the relevant nLab page, there has been a new proposal written up by Mike Shulman there:

An elementary $(\infty,1)$-topos is an $(\infty,1)$-category $\mathbf{E}$ such that

  • $\mathbf{E}$ has finite (∞,1)-limits and colimits
  • $\mathbf{E}$ is locally cartesian closed
  • There exists a subobject classifier (an object classifier that classifies the collection of all monomorphisms in an (∞,1)-category)
  • For any morphism $f:Y\to X$ in $\mathbf{E}$, there exists an object classifier in $\mathbf{E}$ classifying a class of morphisms that (1) includes $f$ and (2) is closed under fiberwise finite limits and colimits, composition (i.e. dependent sums), and dependent products.

For discussion see at the n-Category Café here.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.