= Solution
A signature $\Sigma$ specifies sorts, finite-arity function symbols and finite-arity relation symbols. A <coherent formula> is built from atomic relations and equality using $\top,\bot$, finite conjunction, finite disjunction and existential quantification. A <coherent theory> consists of <coherent sequents> $\phi\vdash_{\vec x}\psi$ in finite typed contexts. The context expresses universal quantification of the free variables; unrestricted universal quantification or negation is not a formula constructor here.
Construct the <coherent syntactic category> $\mathcal C_{\mathbb T}$ as follows. Objects are formulas in context $\{\vec x.\phi\}$, modulo renaming and provable equivalence. An arrow to $\{\vec y.\psi\}$ is a formula $\rho(\vec x,\vec y)$, modulo provable equivalence, for which the theory proves
$$
\rho\vdash\phi\wedge\psi,\qquad\phi\vdash_{\vec x}\exists\vec y\,\rho,\qquad\rho(\vec x,\vec y)\wedge\rho(\vec x,\vec y')\vdash\vec y=\vec y'.
$$
These say that the relation is supported on the specified objects, total and single-valued. The identity is equality on the context, and composition is
$$
(\sigma\circ\rho)(\vec x,\vec z)=\exists\vec y\,(\rho(\vec x,\vec y)\wedge\sigma(\vec y,\vec z)).
$$
The logical rules give associativity and the identity laws. The empty-context true formula is terminal; conjunction in disjoint contexts gives products; conjunction with equality of the two functional relations gives <equalizers>. Existential quantification gives images, and finite disjunction gives unions of <subobjects>. Substitution preserves these constructions, so images and unions are stable under pullback. This makes $\mathcal C_{\mathbb T}$ a <coherent category>.
Let $M$ be a $\mathbb T$-model in a <topos> $\mathcal E$. Interpret each context as a finite product of its sort objects and each formula as its corresponding <subobject>. Define
$$
F_M(\{\vec x.\phi\})=\llbracket\vec x.\phi\rrbracket_M.
$$
The interpretation of an arrow relation $\rho$ is a total single-valued relation between these objects. Its projection to the domain is both an <epimorphism>, by totality, and a <monomorphism>, by single-valuedness, hence invertible in a topos. Its other projection therefore determines a unique morphism. Composition agrees with relational composition, so $F_M$ is a <functor>. Finite limits interpret equality and conjunction; images interpret existential quantification; finite unions interpret disjunction, including the empty union for $\bot$. Consequently $F_M$ is a <coherent functor>.
Conversely there is a canonical syntactic model $U$ in $\mathcal C_{\mathbb T}$. Interpret a sort $s$ by $\{x:s.\top\}$, a function symbol by its term graph, and a relation symbol by its atomic formula-in-context <subobject>. Induction on formulas identifies the interpretation of every $\phi$ in $U$ with its formula-in-context object. Every axiom is then an inclusion of the associated <subobjects>, because it is provable in $\mathbb T$.
For a <coherent functor> $F:\mathcal C_{\mathbb T}\to\mathcal E$, set $M_F=F(U)$. Preservation of <finite limits>, images and unions proves inductively that $F$ preserves all coherent interpretations, so every axiom holds in $M_F$. The same induction supplies natural isomorphisms
$$
F(\{\vec x.\phi\})\cong\llbracket\vec x.\phi\rrbracket_{M_F},
$$
compatible with the functional relations defining arrows. Thus $F\cong F_{M_F}$; directly on the sorts, operations and relations, $M_{F_M}\cong M$.
Finally these constructions agree on morphisms. A model homomorphism $h:M\to N$ induces maps on finite contexts. Atomic relations are preserved by definition; finite conjunction and disjunction and existential witnesses then show that each formula object maps to the corresponding formula object. Compatibility with functional relations makes these maps a <natural transformation> $F_M\to F_N$. Conversely a <natural transformation> between <coherent functors> restricts to its components on sort objects; naturality for term graphs preserves operations, and naturality for relation inclusions preserves relations. It is therefore a model homomorphism. The two correspondences are inverse. We have proved the categorical, not merely objectwise, equivalence
$$
\boxed{\operatorname{Mod}_{\mathbb T}(\mathcal E)\simeq\operatorname{Coh}(\mathcal C_{\mathbb T},\mathcal E).}
$$
Back to article page
