= Total functional relations define morphisms
{title2=$R\hookrightarrow A\times B\quad\Longrightarrow\quad f:A\to B$}
In a <regular category>, a relation $R\hookrightarrow A\times B$ is total if its projection to $A$ is a <regular epimorphism>, and single-valued if two pairs with the same first component have the same second component. The latter makes that projection a <monomorphism>. A regular epimorphism that is monic is invertible, so $f=\pi_B\pi_A^{-1}$ has graph exactly $R$. No axiom of choice or set-based element selection is used.
Back to article page
