= Solution
In a <regular category>, interpret existential quantification by the image of the appropriate projection. The relation $f(x)=y$ is the graph of $f$, isomorphic to $A$; its projection to $B$ is $f$ itself. Thus the subobject interpreting the existential predicate is $\operatorname{im}(f)\hookrightarrow B$. Semantic validity of the sequent means this image is the whole object.
The regular image factorization writes $f=me$ with $e$ a <regular epimorphism> and $m$ its monic image inclusion. Its image is all of $B$ exactly when $m$ is invertible, equivalently when $f$ is itself a regular epimorphism. \b[This is precisely the cover condition in a regular category.]
Back to article page
