nLab model topos

Idea

A model topos is a model category that presents an (∞,1)-topos.

Definition

A model category $\mathcal{C}$ is a model topos if there is a simplicial site $K$ and a Quillen equivalence $\mathcal{C} \simeq sPSh(K)_{loc}$ to the local model structure on sSet-presheaves over $K$.

This appears as Rezk, 6.1.

Related concepts

• model site, model structure on simplicial presheaves

• Ho(CombModCat)

flavors of higher toposes

• 1-topos

  • (0,1)-topos

  • (1,1)-topos = topos

  • (2,1)-topos

  • $(n,1)$-topos

  • (∞,1)-topos ($n$-localic)

    $\;\;\;\;$ model topos

• 2-topos

  • (2,2)-topos ($n$-localic)

  • (∞,2)-topos

• $n$-topos

  • $(\infty,n)$-topos

Locally presentable categories: Cocomplete possibly-large categories generated under filtered colimits by small generators under small relations. Equivalently, accessible reflective localizations of free cocompletions. Accessible categories omit the cocompleteness requirement; toposes add the requirement of a left exact localization.

$\phantom{A}$(n,r)-categories$\phantom{A}$	$\phantom{A}$toposes$\phantom{A}$	locally presentable	loc finitely pres	localization theorem	free cocompletion	accessible
(0,1)-category theory	locales	suplattice	algebraic lattices	Porst’s theorem	powerset	poset
category theory	toposes	locally presentable categories	locally finitely presentable categories	Gabriel–Ulmer’s theorem	presheaf category	accessible categories
model category theory	model toposes	combinatorial model categories		Dugger's theorem	global model structures on simplicial presheaves	n/a
(∞,1)-category theory	(∞,1)-toposes	locally presentable (∞,1)-categories		Simpson’s theorem	(∞,1)-presheaf (∞,1)-categories	accessible (∞,1)-categories

References

The terminology “model topos” is due to:

• Charles Rezk, Toposes and homotopy toposes, 2010 (pdf, pdf)

Essentially this idea appears earlier in:

• Carlos Simpson, A Giraud-type characterization of the simplicial categories associated to closed model categories as $\infty$-pretopoi (arXiv:math/9903167)

• Bertrand Toën, Gabriele Vezzosi, Homotopical Algebraic Geometry I: Topos theory, Advances in Mathematics 193 2 (2005) 257-372 [arXiv:math.AG/0207028, doi:10.1016/j.aim.2004.05.004]

In the context of categorical semantics for univalent homotopy type theory, the combination of terminology “model topos” with type-theoretic model category to type-theoretic model topos:

• Michael Shulman, §1.3 in: All $(\infty,1)$-toposes have strict univalent universes (arXiv:1904.07004)

reviewed in

• Emily Riehl, §6.1 of: On the $\infty$-topos semantics of homotopy type theory, lecture at Logic and higher structures CIRM (Feb. 2022) [pdf, pdf]