Coherent syntactic category
= Coherent syntactic category
{title2=$\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>.