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$ Dec 11 '15 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$ Dec 11 '15 at 23:53
  • $\begingroup$ @AntonFetisov To clarify, what is meant by "absolutely flat functor"? $\endgroup$ Jan 12 '17 at 15:52
  • 1
    $\begingroup$ See the last slide of Mike Shulman's talk:(home.sandiego.edu/~shulman/hottminicourse2012/04induction.pdf) $\endgroup$ Jan 12 '17 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$ Jan 12 '17 at 16:53

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, privacy policy and cookie policy

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