= Cartesian syntactic category
{c}
{title2=$\mathcal C_{\mathbb T}$}
Objects are Cartesian formulas-in-context modulo provable equivalence, and arrows are provably total single-valued Cartesian relations. Composition quantifies the unique intermediate tuple. Context concatenation, conjunction and equality give finite limits. Its canonical model interprets a formula as its own context subobject, so factorization of antecedent through consequent is exactly sequent derivability.
Back to article page
