Let $A$ and $B$ be sets.
We have a natural bijection
with every adjunction in $\boldsymbol {\mathsf{Rel}}$ being of the form $\operatorname {\mathrm{Gr}}\webleft (f\webright )\dashv f^{-1}$ for some function $f$.
We proceed step by step:
From Adjunctions in $\boldsymbol {\mathsf{Rel}}$ to Functions. An adjunction in $\boldsymbol {\mathsf{Rel}}$ from $A$ to $B$ consists of a pair of relations
together with inclusions
We claim that these conditions imply that $R$ is total and functional, i.e. that $R\webleft (a\webright )$ is a singleton for each $a\in A$:
$R\webleft (a\webright )$ Has an Element. Given $a\in A$, since $\chi _{A}\subset S\mathbin {\diamond }R$, we must have $\left\{ a\right\} \subset S\webleft (R\webleft (a\webright )\webright )$, implying that there exists some $b\in B$ such that $a\sim _{R}b$ and $b\sim _{S}a$, and thus $R\webleft (a\webright )\neq \text{Ø}$, as $b\in R\webleft (a\webright )$.
$R\webleft (a\webright )$ Has No More Than One Element. Suppose that we have $a\sim _{R}b$ and $a\sim _{R}b'$ for $b,b'\in B$. We claim that $b=b'$:
Since $\chi _{A}\subset S\mathbin {\diamond }R$, there exists some $k\in B$ such that $a\sim _{R}k$ and $k\sim _{S}a$.
Since $R\mathbin {\diamond }S\subset \chi _{B}$, if $b''\sim _{S}a'$ and $a'\sim _{R}b'''$, then $b''=b'''$.
Applying the above to $b''=k$, $b'''=b$, and $a'=a$, since $k\sim _{S}a$ and $a\sim _{R}b'$, we have $k=b$.
Similarly $k=b'$.
Thus $b=b'$.
Together, the above two items show $R\webleft (a\webright )$ to be a singleton, being thus given by $\operatorname {\mathrm{Gr}}\webleft (f\webright )$ for some function $f\colon A\to B$, which gives a map
Moreover, by uniqueness of adjoints (
, of ), this implies also that $S=f^{-1}$.
From Functions to Adjunctions in $\boldsymbol {\mathsf{Rel}}$. By Chapter 9: Constructions With Relations, of , every function $f\colon A\to B$ gives rise to an adjunction $\operatorname {\mathrm{Gr}}\webleft (f\webright )\dashv f^{-1}$ in $\mathrm{Rel}$, giving a map
Invertibility: From Functions to Adjunctions Back to Functions. We need to show that starting with a function $f\colon A\to B$, passing to $\operatorname {\mathrm{Gr}}\webleft (f\webright )\dashv f^{-1}$, and then passing again to a function gives $f$ again. This is clear however, since we have $a\sim _{\operatorname {\mathrm{Gr}}\webleft (f\webright )}b$ iff $f\webleft (a\webright )=b$.
Invertibility: From Adjunctions to Functions Back to Adjunctions. We need to show that, given an adjunction $R\dashv S$ in $\boldsymbol {\mathsf{Rel}}$ giving rise to a function $f_{R,S}\colon A\to B$, we have
We check these explicitly:
$\operatorname {\mathrm{Gr}}\webleft (f_{R,S}\webright )=R$. We have
$f^{-1}_{R,S}=S$. We first claim that, given $a\in A$ and $b\in B$, the following conditions are equivalent:
We have $a\sim _{R}b$.
We have $b\sim _{S}a$.
Indeed:
If $a\sim _{R}b$, then $b\sim _{S}a$: Since $\chi _{A}\subset S\mathbin {\diamond }R$, there exists $k\in B$ such that $a\sim _{R}k$ and $k\sim _{S}a$, but since $a\sim _{R}b$ and $R$ is functional, we have $k=b$ and thus $b\sim _{S}a$.
If $b\sim _{S}a$, then $a\sim _{R}b$: First note that since $R$ is total we have $a\sim _{R}b'$ for some $b'\in B$. Now, since $R\mathbin {\diamond }S\subset \chi _{B}$, $b\sim _{S}a$, and $a\sim _{R}b'$, we have $b=b'$, and thus $a\sim _{R}b$.
Having show this, we now have
for each $b\in B$, showing $f^{-1}_{R,S}=S$.
This finishes the proof.
