We have an adjunction
natural in $X\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$ and $Y\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}^{\mathsf{op}})$.
We have
|
$\mathsf{Sets}^{\mathsf{op}}(\mathcal{P}(A),B)$ |
$\mathord {\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}}$ |
$\mathsf{Sets}(B,\mathcal{P}(A))$ |
|
|
$\mathord {\cong }$ |
$\mathsf{Sets}(B,\mathsf{Sets}(A,\{ \mathsf{t},\mathsf{f}\} ))$ |
(by Item 2 of Proposition 4.5.1.1.4) |
|
|
$\mathord {\cong }$ |
$\mathsf{Sets}(A\times B,\{ \mathsf{t},\mathsf{f}\} )$ |
(by Item 2 of Proposition 4.1.3.1.3) |
|
|
$\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$ and $B$.1
