We have an adjunction
witnessed by a bijection of sets
\[ \mathrm{Rel}\webleft (\operatorname {\mathrm{Gr}}\webleft (X\webright ),Y\webright ) \cong \mathsf{Sets}\webleft (X,\mathcal{P}\webleft (Y\webright )\webright ) \]
natural in $X\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$ and $Y\in \operatorname {\mathrm{Obj}}\webleft (\mathrm{Rel}\webright )$, where $\operatorname {\mathrm{Gr}}$ is the graph functor of Chapter 9: Constructions With Relations, 
of and $\mathcal{P}_{!}$ is the functor of Chapter 9: Constructions With Relations, .
We have
|
$\mathrm{Rel}\webleft (\operatorname {\mathrm{Gr}}\webleft (A\webright ),B\webright )$
|
$\mathord {\cong }$
|
$\mathcal{P}\webleft (A\times B\webright )$
|
|
|
|
$\mathord {\cong }$
|
$\mathsf{Sets}\webleft (A\times B,\{ \mathsf{t},\mathsf{f}\} \webright )$
|
(by Item 2 of Proposition 4.5.1.1.4)
|
|
|
$\mathord {\cong }$
|
$\mathsf{Sets}\webleft (A,\mathsf{Sets}\webleft (B,\{ \mathsf{t},\mathsf{f}\} \webright )\webright )$
|
(by Item 2 of Proposition 4.1.3.1.3)
|
|
|
$\mathord {\cong }$
|
$\mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright )$,
|
(by Item 2 of Proposition 4.5.1.1.4)
|
where all bijections are natural in $A$, (where we are using Item 3 of Proposition 4.5.1.1.4). Explicitly, this isomorphism is given by sending a relation $R\colon \operatorname {\mathrm{Gr}}\webleft (A\webright )\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ to the map $R^{\dagger }\colon A\to \mathcal{P}\webleft (B\webright )$ sending $a$ to the subset $R\webleft (a\webright )$ of $B$, as in Chapter 8: Relations, Definition 8.1.1.1.1.
Naturality in $B$ is then the statement that given a relation $R\colon B\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B'$, the diagram
commutes, which follows from Chapter 9: Constructions With Relations, .
