Let $X$ be a set.
Map I
We define a map
\[ \Phi _{X,Y}\colon \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright ) \to \mathsf{Sets}\webleft (X,Y\webright ) \]
as in the statement, i.e. by
\[ \Phi _{X,Y}\webleft (f\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\circ \chi _{X} \]
for each $f\in \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )$.
Map II
We define a map
\[ \Psi _{X,Y}\colon \mathsf{Sets}\webleft (X,Y\webright )\to \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright ) \]
as in the statement, i.e. by
for each $f\in \mathsf{Sets}\webleft (X,Y\webright )$.
Invertibility I
We claim that
\[ \Psi _{X,Y}\circ \Phi _{X,Y}=\operatorname {\mathrm{id}}_{\mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )}. \]
We have
\begin{align*} \webleft [\Psi _{X,Y}\circ \Phi _{X,Y}\webright ]\webleft (f\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Psi _{X,Y}\webleft (\Phi _{X,Y}\webleft (f\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Psi _{X,Y}\webleft (f\circ \chi _{X}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {\mathrm{Lan}}_{\chi _{X}}\webleft (f\circ \chi _{X}\webright )\\ \end{align*}
for each $f\in \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )$. We now claim that
\[ \operatorname {\mathrm{Lan}}_{\chi _{X}}\webleft (f\circ \chi _{X}\webright )=f \]
for each $f\in \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )$. Indeed, we have
\begin{align*} \left[\operatorname {\mathrm{Lan}}_{\chi _{X}}\webleft (f\circ \chi _{X}\webright )\right]\webleft (U\webright ) & = \bigvee _{x\in U} f\webleft (\chi _{X}\webleft (x\webright )\webright )\\ & = f\left(\bigvee _{x\in U}\chi _{X}\webleft (x\webright )\right)\\ & = f\left(\bigcup _{x\in U}\left\{ x\right\} \right)\\ & = f\webleft (U\webright )\end{align*}
for each $U\in \mathcal{P}\webleft (X\webright )$, where we have used that $f$ is a morphism of suplattices and hence preserves joins for the second equality. This proves our claim. Since we have shown that
\[ \webleft [\Psi _{X,Y}\circ \Phi _{X,Y}\webright ]\webleft (f\webright )=f \]
for each $f\in \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )$, it follows that $\Psi _{X,Y}\circ \Phi _{X,Y}$ must be equal to the identity map $\operatorname {\mathrm{id}}_{\mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )}$ of $\mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )$.
Invertibility II
We claim that
\[ \Phi _{X,Y}\circ \Psi _{X,Y}=\operatorname {\mathrm{id}}_{\mathsf{Sets}\webleft (X,Y\webright )}. \]
We have
\begin{align*} \webleft [\Phi _{X,Y}\circ \Psi _{X,Y}\webright ]\webleft (f\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X,Y}\webleft (\Psi _{X,Y}\webleft (f\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X,Y}\webleft (\operatorname {\mathrm{Lan}}_{\chi _{X}}\webleft (f\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {\mathrm{Lan}}_{\chi _{X}}\webleft (f\webright )\circ \chi _{X}\end{align*}
for each $f\in \mathsf{Sets}\webleft (X,Y\webright )$. We now claim that
\[ \operatorname {\mathrm{Lan}}_{\chi _{X}}\webleft (f\webright )\circ \chi _{X}=f \]
for each $f\in \mathsf{Sets}\webleft (X,Y\webright )$. Indeed, we have
\begin{align*} \webleft [\operatorname {\mathrm{Lan}}_{\chi _{X}}\webleft (f\webright )\circ \chi _{X}\webright ]\webleft (x\webright ) & = \bigvee _{y\in \left\{ x\right\} }f\webleft (y\webright )\\ & = f\webleft (x\webright )\end{align*}
for each $x\in X$. This proves our claim. Since we have shown that
\[ \webleft [\Phi _{X,Y}\circ \Psi _{X,Y}\webright ]\webleft (f\webright )=f \]
for each $f\in \mathsf{Sets}\webleft (X,Y\webright )$, it follows that $\Phi _{X,Y}\circ \Psi _{X,Y}$ must be equal to the identity map $\operatorname {\mathrm{id}}_{\mathsf{Sets}\webleft (X,Y\webright )}$ of $\mathsf{Sets}\webleft (X,Y\webright )$.
Naturality for $\Phi $, Part I
We need to show that, given a function $f\colon X\to X'$, the diagram commutes. Indeed, we have
\begin{align*} \webleft [\Phi _{X,Y}\circ \mathcal{P}_{!}\webleft (f\webright )^{*}\webright ]\webleft (\xi \webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X,Y}\webleft (\mathcal{P}_{!}\webleft (f\webright )^{*}\webleft (\xi \webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X,Y}\webleft (\xi \circ f_{!}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\xi \circ f_{!}\webright )\circ \chi _{X}\\ & = \xi \circ \webleft (f_{!}\circ \chi _{X}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle (\dagger )}}{=}}}\xi \circ \webleft (\chi _{X'}\circ f\webright )\\ & = \webleft (\xi \circ \chi _{X'}\webright )\circ f\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X',Y}\webleft (\xi \webright )\circ f\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f^{*}\webleft (\Phi _{X',Y}\webleft (\xi \webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [f^{*}\circ \Phi _{X',Y}\webright ]\webleft (\xi \webright ), \end{align*}
for each $\xi \in \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X'\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )$, where we have used Item 1 of Proposition 4.5.4.1.3 for the fifth equality above.
Naturality for $\Phi $, Part II
We need to show that, given a morphism of suplattices
\[ g\colon \webleft (Y,\preceq _{Y}\webright )\to \webleft (Y',\preceq _{Y'}\webright ), \]
the diagram
commutes. Indeed, we have
\begin{align*} \webleft [\Phi _{X,Y'}\circ g_{!}\webright ]\webleft (\xi \webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X,Y'}\webleft (g_{!}\webleft (\xi \webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X,Y'}\webleft (g\circ \xi \webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (g\circ \xi \webright )\circ \chi _{X}\\ & = g\circ \webleft (\xi \circ \chi _{X}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g\circ \webleft (\Phi _{X,Y}\webleft (\xi \webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g_{!}\webleft (\Phi _{X,Y}\webleft (\xi \webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [g_{!}\circ \Phi _{X,Y}\webright ]\webleft (\xi \webright ). \end{align*}
for each $\xi \in \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )$.
Naturality for $\Psi $
Since $\Phi $ is natural in each argument and $\Phi $ is a componentwise inverse to $\Psi $ in each argument, it follows from Chapter 11: Categories, Item 2 of Proposition 11.9.7.1.2 that $\Psi $ is also natural in each argument.