 Cartesian syntactic category

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.