Left adjoint relation is a function
ID: left-adjoint-relation-is-a-function
In the inclusion-ordered category of sets and relations, a relation has a right adjoint exactly when it is the graph of a total single-valued function; its right adjoint is the converse relation.
New to topics? Read the docs here!