Solution

ID: past-exam-of-the-mathematics-course-of-the-university-of-cambridge/2010/iii/paper-75/7/ii/solution

In a regular category, interpret existential quantification by the image of the appropriate projection. The relation is the graph of , isomorphic to ; its projection to is itself. Thus the subobject interpreting the existential predicate is . Semantic validity of the sequent means this image is the whole object.
The regular image factorization writes with a regular epimorphism and its monic image inclusion. Its image is all of exactly when is invertible, equivalently when is itself a regular epimorphism. This is precisely the cover condition in a regular category.

New to topics? Read the docs here!