left and right euclidean;
A binary relation from a set to a set is called functional if every element of is related to at most one element of . 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 can be viewed as a span
Such a span is a relation iff the pairing map from the domain to is an injection, and such a relation is functional iff the inclusion map is also an injection. Such a relation is entire iff the inclusion map is a surjection.
(Total) functions can be characterized as the left adjoints in the bicategory of relations, in other words relations in for which there exists satisfying
in which case it may be proven that . A relation is functional if and only if , and is entire if and only if .
Further to this: surjectivity of a function can be expressed as the condition , and injectivity as .