If a Cartesian sequent fails to factor its antecedent subobject through its consequent, the covariant representable functor is a set-valued countermodel. It preserves finite limits, and the element named by the antecedent inclusion belongs to the antecedent but cannot belong to the consequent. Hence validity in every set model implies Cartesian derivability.
Articles by others on the same topic
There are currently no matching articles.