= Solution
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 define
$$
\boxed{f=q\circ p^{-1}:A\to B}.
$$
The 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.
Back to article page
