Past exam of the mathematics course of the University of Cambridge / 2010 / iii / Paper 75 / 7

The equality predicate on $A$ is interpreted by the diagonal monomorphism ${\Delta }_A:A\hookrightarrow A\times A$. The antecedent equality of the two $f$-values is the kernel pair $A{\times }_{B}A\hookrightarrow A\times A$. Semantic validity of the implication says that the kernel-pair subobject is contained in the diagonal; the reverse containment always holds. Hence the sequent is valid exactly whenIf $f$ is monic, this equality is its cancellation property expressed by the pullback. Conversely, if $fr=fs$ for $r,s:X\to A$, then $(r,s)$ factors through this kernel pair and therefore through the diagonal, giving $r=s$. Thus the sequent holds exactly when the map is a monomorphism. This argument uses generalized arrows from arbitrary $X$, not a claim that global elements detect maps.

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 $\mathrm{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. This is precisely the cover condition in a regular category.

Interpret the given relation by a subobject $R\hookrightarrow A\times B$ and write its projections as $p:R\to A$, $q:R\to B$. Totality says that the image of $p$ is all of $A$, so $p$ is a regular epimorphism. Single-valuedness makes $p$ monic: if $pr=ps$ for two arrows into $R$, the functionality sequent forces $qr=qs$, and the inclusion into $A\times B$ then gives $r=s$.

A regular epimorphism that is monic is invertible. Indeed its kernel pair consists of equal projections, and its coequalizer universal property supplies an inverse. Therefore defineThe graph of this map is exactly the original relation $R$, since $(p,q)=(1_A,f)p$. The graph also makes the map unique. This proves total functional relations define morphisms, using regular-category semantics and no choice of individual witnesses.