(0,1)-topos, Heyting algebra, locale
category of presheaves
category of sheaves
coverage, pretopology, topology
base topos, indexed topos
natural numbers object
direct image/inverse image
surjective geometric morphism
essential geometric morphism
locally connected geometric morphism
connected geometric morphism
totally connected geometric morphism
étale geometric morphism
open geometric morphism
proper geometric morphism, compact topos
separated geometric morphism, Hausdorff topos
local geometric morphism
bounded geometric morphism
localic geometric morphism
hyperconnected geometric morphism
atomic geometric morphism
petit topos/gros topos
locally connected topos, connected topos, totally connected topos, strongly connected topos
abelian sheaf cohomology
model structure on simplicial presheaves
higher topos theory
(∞,1)-sheaf, ∞-stack, derived stack
Edit this sidebar
A Π\Pi-pretopos is a pretopos that is also a locally cartesian closed category.
A ΠW-pretopos is a Π\Pi-pretopos that also has all W-types.
A predicative topos is ΠW\Pi W-pretopos with axiom of multiple choice.
See at predicative topos.