= Presheaf classifier of a Horn theory
{title2=$\mathbf{Set}[\mathbb T]\simeq[(\mathcal C_{\mathbb T}^{\mathrm{cart}})^{\mathrm{op}},\mathbf{Set}]$}
Internal Horn models are finite-limit-preserving <functors> out of the <Cartesian syntactic category>. Since that category has <finite limits>, these are exactly <flat functors>; the presheaf <Diaconescu equivalence for geometric morphisms> proves the classifying property. Equivalently the classifier is the covariant <functor> category on finitely presented set-based models.
Back to article page
