= Solution
\b[Yes, with the Horn/Cartesian-fragment convention.] A <Horn theory> uses positive finite-conjunction sequents and has a <Cartesian syntactic category> $\mathcal C_{\mathbb T}^{\mathrm{cart}}$ with <finite limits>. Provably uniquely witnessed existential formulas can also be admitted without changing the finite-limit nature of its semantics. Its internal models are precisely finite-limit-preserving <functors> from that category.
For a category with <finite limits>, <flat functors> into a <Grothendieck topos> are exactly finite-limit-preserving <functors>. In sets, the reason is concrete: the <category of elements> of a covariant left-exact <functor> is cofiltered. Its <terminal object> supplies nonemptiness, products supply cones over pairs of elements, and <equalizers> supply equalizing cones over parallel arrows. Conversely a cofiltered <category of elements> expresses the <functor> as a filtered <colimit> of covariant representables; filtered <colimits> of sets commute with <finite limits>. The internal version uses the same cone conditions locally.
The presheaf form of the <Diaconescu equivalence for geometric morphisms> therefore identifies <geometric morphisms> into
$$
\boxed{[(\mathcal C_{\mathbb T}^{\mathrm{cart}})^{\mathrm{op}},\mathbf{Set}]}
$$
with internal Horn models, naturally in the domain topos. This is the <presheaf classifier of a Horn theory>.
Equivalently, using a small skeleton of the category $\mathcal A$ of finitely presented set-based Horn models, the classifier is $[\mathcal A,\mathbf{Set}]$, with covariant <functors>. The duality $\mathcal A\simeq(\mathcal C_{\mathbb T}^{\mathrm{cart}})^{\mathrm{op}}$ sends a formula to the model generated by its tuple subject to its finite constraints. \b[The presheaf claim does not extend merely because a general geometric or regular theory has no written disjunctions]: arbitrary existential witnesses are not uniquely witnessed Horn data.
Back to article page
