A Cartesian formula is built from atoms and equality using truth, finite conjunction and uniquely witnessed existential quantification. Uniqueness is proved relative to the theory before admitting the quantifier. In a finite-limit category, such a quantified relation projects monomorphically into the remaining context, so its semantics needs no arbitrary image operation.
New to topics? Read the docs here!