Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
A binary relation from a set $X$ to a set $Y$ is called functional if every element of $X$ is related to at most one element of $Y$. Notice that this is the same thing as a partial function, seen from a different point of view. A (total) function is precisely a relation that is both functional and entire.
Like any relation, a functional relation $r$ can be viewed as a span
Such a span is a relation iff the pairing map from the domain $\Delta_r$ to $X \times Y$ is an injection, and such a relation is functional iff the inclusion map $\iota_r$ is also an injection. Such a relation is entire iff the inclusion map $\iota_r$ is a surjection.
(Total) functions can be characterized as the left adjoints in the bicategory of relations, in other words relations $r: X \to Y$ in $Rel$ for which there exists $s: Y \to X$ satisfying
in which case it may be proven that $s = r^{op}$. A relation is functional if and only if $r \circ r^{op} \leq 1_Y$, and is entire if and only if $1_X \leq r^{op} \circ r$.
Further to this: surjectivity of a function $r: X \to Y$ can be expressed as the condition $1_Y \leq r \circ r^{op}$, and injectivity as $r^{op} \circ r \leq 1_X$.