Coherent syntactic category (${\mathcal{C}}_{\mathbb{T}}$)

Objects are coherent formulas in context and arrows are provably total, single-valued relations, modulo provable equivalence. Composition existentially eliminates the intermediate tuple. Conjunction constructs finite limits, existential formulas construct images and disjunction constructs finite unions. It is a coherent category.

The canonical model interprets each sort as its truth-context object, each operation by its term graph and each relation by its atomic subobject. A coherent formula is interpreted by its own formula-in-context object. Consequently a coherent sequent holds in this model exactly when it is derivable in the theory.