For small category $\mathcal{C}$, presheaf category $[\mathcal{C}^{\text{op}}, \textbf{Set}]$ is topos with:

• Products/limits computed pointwise
• Exponentials: $(G^F)(c) = \text{Nat}(\mathcal{Y}(c) \times F, G)$
• Subobject classifier: $\Omega(c) = \text{Sieve}(c)$ (sieves on $c$)

For Grothendieck site $(\mathcal{C}, J)$ (category with coverage), sheaves $\textbf{Sh}(\mathcal{C}, J)$ form topos. The sheafification functor is left adjoint to inclusion $\textbf{Sh}(\mathcal{C}, J) \hookrightarrow [\mathcal{C}^{\text{op}}, \textbf{Set}]$.

Important cases:

• Topological spaces: opens form site
• Étale site: for algebraic geometry
• Flat site: for fpqc topology

Effective topos constructed from partial recursive functions on $\mathbb{N}$. Objects are "assemblies" (sets with realizability structure). This topos has all finite limits but law of excluded middle fails.

Realizability toposes model constructive mathematics and computability.

Every geometric theory $\mathbb{T}$ has classifying topos $\text{Set}[\mathbb{T}]$: geometric morphisms $\mathcal{E} \to \text{Set}[\mathbb{T}]$ correspond to models of $\mathbb{T}$ in $\mathcal{E}$.

Example: Topos of $G$-sets classifies transitive $G$-sets (single-sorted theory).

For monoid $M$, category $\textbf{Set}^M$ of $M$-actions (sets with $M$-action) is topos. More generally, for internal monoid in topos, category of actions is topos.

For topos $\mathcal{E}$ and object $A$, slice category $\mathcal{E}/A$ is topos with:

• Subobject classifier: $\Omega_A = \Omega^A$
• Exponentials via pullback
• This is "parameterized" topos over $A$

The Schanuel topos is presheaf topos on category of finitely generated free groups. It provides models of synthetic domain theory and computational type theory.