Question: How can I complete the following sentence: "For all $\mathsf{Rel}$-arrows $f : X \rightarrow Y$, $f$ is a function iff ..."?
Of course, this is easily done: "For all $\mathsf{Rel}$-arrows $f : X \rightarrow Y$, $f$ is a function iff for all $x \in X$ there exists unique $y \in Y$ such that $(x,y) \in f$." However, I'm looking for something more category-theoretic in "spirit."
I'm also interested in variants of the sentence: replace "function" with injection/surjection/partial function/left-total relation etc.
First, one must recall that $\textbf{Rel}$ is an allegory and in particular is a 2-category. Thus there is a notion of adjunction in $\textbf{Rel}$. It is traditional to say that a map in an allegory is a morphism with a right adjoint. So what does this notion give us in $\textbf{Rel}$? Well, suppose $\phi : X \to Y$ has a right adjoint $\psi : Y \to X$. That means that $\textrm{id}_X \le \psi \circ \phi$ and $\phi \circ \psi \le \textrm{id}_Y$. So, for each $x$, there exists $y$ such that $\phi (x, y)$ and $\psi (y, x)$; and for each $x, y, y'$, if $\psi (y, x)$ and $\phi (x, y')$, then $y = y'$. We thus deduce that $\phi$ is an total functional relation, and moreover $\psi (y, x) \equiv \phi (x, y)$. So a map in $\textbf{Rel}$ is what we expect to be: the relation induced by a function.
More generally: