Classifying topos

Definition

Let $\mathbb{T}$ be a geometric theory. This is a first-order theory whose axioms are sequents between formulas built from finite conjunctions, arbitrary disjunctions and existential quantifiers. For a Grothendieck topos $\mathcal{E}$, let $\mathbb{T}\text{-}\mathrm{Mod}(\mathcal{E})$ be the category of models of $\mathbb{T}$ in $\mathcal{E}$. For Grothendieck toposes $\mathcal{E}$ and $\mathcal{F}$, let $\mathbf{Geom}(\mathcal{E}, \mathcal{F})$ be the category of geometric morphisms $\mathcal{E} \to \mathcal{F}$, and write $f^*$ for the inverse image part of $f$. A classifying topos of $\mathbb{T}$ is a Grothendieck topos $\mathbf{Set}[\mathbb{T}]$ together with a model $U_{\mathbb{T}}$ of $\mathbb{T}$ in it with the following property. For every Grothendieck topos $\mathcal{E}$ the functor $$\mathbf{Geom}(\mathcal{E}, \mathbf{Set}[\mathbb{T}]) \to \mathbb{T}\text{-}\mathrm{Mod}(\mathcal{E}), \qquad f \mapsto f^*(U_{\mathbb{T}})$$ is an equivalence of categories. The model $U_{\mathbb{T}}$ is called the generic model of $\mathbb{T}$.