Classifying topos (source code)

= Classifying topos
{title2=$\operatorname{Geom}(\mathcal F,\mathcal E_{\mathbb T})\simeq\mathbb T\text{-}\operatorname{Mod}(\mathcal F)$}
{wiki}

A topos classifies a geometric theory when geometric morphisms into it from any <Grothendieck topos> correspond naturally to internal models of that theory. Pulling back one generic model gives the corresponding model. For a finitary <algebraic theory>, the classifying topos is the covariant functor category on finitely presented models.