We have an adjunction
natural in $X\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$ and $Y\in \operatorname {\mathrm{Obj}}(\mathrm{Rel})$, where $\operatorname {\mathrm{Gr}}$ is the graph functor of Chapter 8: Relations, Item 1 of Proposition 8.2.2.1.2 and $\mathcal{P}_{!}$ is the functor of Chapter 8: Relations, Proposition 8.7.6.1.1.
We have
|
$\mathrm{Rel}(\operatorname {\mathrm{Gr}}(A),B)$ |
$\mathord {\cong }$ |
$\mathcal{P}(A\times B)$ |
|
|
$\mathord {\cong }$ |
$\mathsf{Sets}(A\times B,\{ \mathsf{t},\mathsf{f}\} )$ |
(by Item 2 of Proposition 4.5.1.1.4) |
|
|
$\mathord {\cong }$ |
$\mathsf{Sets}(A,\mathsf{Sets}(B,\{ \mathsf{t},\mathsf{f}\} ))$ |
(by Item 2 of Proposition 4.1.3.1.3) |
|
|
$\mathord {\cong }$ |
$\mathsf{Sets}(A,\mathcal{P}(B))$, |
(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}}(A)\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ to the map $R^{\dagger }\colon A\to \mathcal{P}(B)$ sending $a$ to the subset $R(a)$ 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
