A category $\mathcal{E}$ is a Grothendieck topos (equivalent to category of sheaves on some site) if and only if:

1. $\mathcal{E}$ has all small colimits and these are universal (stable under pullback)
2. Coproducts in $\mathcal{E}$ are disjoint and universal
3. Every equivalence relation is effective (quotient by equivalence relation exists)
4. $\mathcal{E}$ has a small set of generators

Every Grothendieck topos has a surjection from a Boolean topos. More precisely, there exists complete Boolean topos $\mathcal{B}$ and geometric surjection $\mathcal{B} \to \mathcal{E}$.

This provides classical "cover" of any topos, enabling proof techniques using classical logic.

In topos $\mathcal{E}$, the following are equivalent:

1. Axiom of choice holds (every epic splits)
2. Every object is projective
3. Law of excluded middle holds in internal logic

Most geometric toposes fail these conditions, being inherently constructive.

Every topos $\mathcal{E}$ has internal language: type theory where:

• Types correspond to objects
• Terms of type $A$ are morphisms $1 \to A$
• Predicates on $A$ are subobjects (morphisms $A \to \Omega$)

Theorems provable in internal language hold in all toposes.

For propositional geometric theory $\mathbb{T}$, model $\mathbb{T} \vdash \phi$ in all toposes if and only if $\mathbb{T} \vdash \phi$ is provable constructively.

This gives completeness theorem for intuitionistic logic via toposes.

Every coherent topos has enough points: it can be recovered from its functor of points (geometric morphisms from $\textbf{Set}$).

This connects abstract toposes to concrete "generalized spaces."