topos theory
category theory
category
functor
(0,1)-topos, Heyting algebra, locale
pretopos
topos
Grothendieck topos
category of presheaves
presheaf
representable presheaf
category of sheaves
site
sieve
coverage, pretopology, topology
sheaf
sheafification
quasitopos
base topos, indexed topos
categorical semantics
internal logic
subobject classifier
natural numbers object
logical morphism
geometric morphism
direct image/inverse image
global sections
geometric embedding
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
base change
localic geometric morphism
hyperconnected geometric morphism
atomic geometric morphism
topological locale
localic topos
petit topos/gros topos
locally connected topos, connected topos, totally connected topos, strongly connected topos
local topos
cohesive topos
classifying topos
smooth topos
cohomology
homotopy
abelian sheaf cohomology
model structure on simplicial presheaves
higher topos theory
(0,1)-topos
2-topos
2-site
2-sheaf, stack
(∞,1)-topos
(∞,1)-site
(∞,1)-sheaf, ∞-stack, derived stack
Diaconescu's theorem
Barr's theorem
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 $\Pi W$-pretopos with axiom of multiple choice.
See at predicative topos.