\[ \mathsf{Sets}_{*}\webleft (A\odot X,K\webright )\cong \mathsf{Sets}\webleft (A,\mathsf{Sets}_{*}\webleft (X,K\webright )\webright ) \]
natural in $\webleft (K,k_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$.
- Map I. We define a map
\[ \Phi _{K}\colon \mathsf{Sets}_{*}\webleft (A\odot X,K\webright ) \to \mathsf{Sets}\webleft (A,\mathsf{Sets}_{*}\webleft (X,K\webright )\webright ) \]
by sending a morphism of pointed sets
\[ \xi \colon \webleft (A\odot X,a\odot x_{0}\webright )\to \webleft (K,k_{0}\webright ) \]
to the map of sets
where
\[ \xi _{a}\colon \webleft (X,x_{0}\webright )\to \webleft (K,k_{0}\webright ) \]
is the morphism of pointed sets defined by
\[ \xi _{a}\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi \webleft (a\odot x\webright ) \]
for each $x\in X$. Note that we have
\begin{align*} \xi _{a}\webleft (x_{0}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi \webleft (a\odot x_{0}\webright )\\ & = k_{0},\end{align*}
so that $\xi _{a}$ is indeed a morphism of pointed sets, where we have used that $\xi $ is a morphism of pointed sets.
- Map II. We define a map
\[ \Psi _{K}\colon \mathsf{Sets}\webleft (A,\mathsf{Sets}_{*}\webleft (X,K\webright )\webright )\to \mathsf{Sets}_{*}\webleft (A\odot X,K\webright ) \]
given by sending a map
to the morphism of pointed sets
\[ \xi ^{\dagger }\colon \webleft (A\odot X,a\odot x_{0}\webright )\to \webleft (K,k_{0}\webright ) \]
defined by
\[ \xi ^{\dagger }\webleft (a\odot x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi _{a}\webleft (x\webright ) \]
for each $a\odot x\in A\odot X$. Note that $\xi ^{\dagger }$ is indeed a morphism of pointed sets, as we have
\begin{align*} \xi ^{\dagger }\webleft (a\odot x_{0}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi _{a}\webleft (x_{0}\webright )\\ & = k_{0}, \end{align*}
where we have used that $\xi \webleft (a\webright )\in \mathsf{Sets}_{*}\webleft (X,K\webright )$ is a morphism of pointed sets.
- Invertibility I. We claim that
\[ \Psi _{K}\circ \Phi _{K}=\text{id}_{\mathsf{Sets}_{*}\webleft (A\odot X,K\webright )}. \]
Indeed, given a morphism of pointed sets
\[ \xi \colon \webleft (A\odot X,a\odot x_{0}\webright )\to \webleft (K,k_{0}\webright ), \]
we have
\begin{align*} \webleft [\Psi _{K}\circ \Phi _{K}\webright ]\webleft (\xi \webright ) & = \Psi _{K}\webleft (\Phi _{K}\webleft (\xi \webright )\webright )\\ & = \Psi _{K}\webleft ([\mspace {-3mu}[a\mapsto [\mspace {-3mu}[x\mapsto \xi \webleft (a\odot x\webright )]\mspace {-3mu}]]\mspace {-3mu}]\webright )\\ & = \Psi _{K}\webleft ([\mspace {-3mu}[a'\mapsto [\mspace {-3mu}[x'\mapsto \xi \webleft (a'\odot x'\webright )]\mspace {-3mu}]]\mspace {-3mu}]\webright )\\ & = [\mspace {-3mu}[a\odot x\mapsto \mathrm{ev}_{x}\webleft (\mathrm{ev}_{a}\webleft ([\mspace {-3mu}[a'\mapsto [\mspace {-3mu}[x'\mapsto \xi \webleft (a'\odot x'\webright )]\mspace {-3mu}]]\mspace {-3mu}]\webright )\webright )]\mspace {-3mu}]\\ & = [\mspace {-3mu}[a\odot x\mapsto \mathrm{ev}_{x}\webleft ([\mspace {-3mu}[x'\mapsto \xi \webleft (a\odot x'\webright )]\mspace {-3mu}]\webright )]\mspace {-3mu}]\\ & = [\mspace {-3mu}[a\odot x\mapsto \xi \webleft (a\odot x\webright )]\mspace {-3mu}]\\ & = \xi .\end{align*}
- Invertibility II. We claim that
\[ \Phi _{K}\circ \Psi _{K}=\text{id}_{\mathsf{Sets}\webleft (A,\mathsf{Sets}_{*}\webleft (X,K\webright )\webright )}. \]
Indeed, given a morphism $\xi \colon A\to \mathsf{Sets}_{*}\webleft (X,K\webright )$, we have
\begin{align*} \webleft [\Phi _{K}\circ \Psi _{K}\webright ]\webleft (\xi \webright ) & = \Phi _{K}\webleft (\Psi _{K}\webleft (\xi \webright )\webright )\\ & = \Phi _{K}\webleft ([\mspace {-3mu}[a\odot x\mapsto \xi _{a}\webleft (x\webright )]\mspace {-3mu}]\webright )\\ & = [\mspace {-3mu}[a\mapsto [\mspace {-3mu}[x\mapsto \xi _{a}\webleft (x\webright )]\mspace {-3mu}]]\mspace {-3mu}]\\ & = [\mspace {-3mu}[a\mapsto \xi \webleft (a\webright )]\mspace {-3mu}]\\ & = \xi .\end{align*}
- Naturality of $\Phi $. We need to show that, given a morphism of pointed sets
\[ \phi \colon \webleft (K,k_{0}\webright )\to \webleft (K',k'_{0}\webright ), \]
the diagram
commutes. Indeed, given a morphism of pointed sets
\[ \xi \colon \webleft (A\odot X,a\odot x_{0}\webright )\to \webleft (K,k_{0}\webright ), \]
we have
\begin{align*} \webleft [\Phi _{K'}\circ \phi _{*}\webright ]\webleft (\xi \webright ) & = \Phi _{K'}\webleft (\phi _{*}\webleft (\xi \webright )\webright )\\ & = \Phi _{K'}\webleft (\phi \circ \xi \webright )\\ & = \webleft (\phi \circ \xi \webright )^{\dagger }\\ & = [\mspace {-3mu}[a\mapsto \phi \circ \xi \webleft (a\odot -\webright )]\mspace {-3mu}]\\ & = [\mspace {-3mu}[a\mapsto \phi _{*}\webleft (\xi \webleft (a\odot -\webright )\webright )]\mspace {-3mu}]\\ & = \webleft (\phi _{*}\webright )_{*}\webleft ([\mspace {-3mu}[a\mapsto \xi \webleft (a\odot -]\mspace {-3mu}]\webright )\webright )\\ & = \webleft (\phi _{*}\webright )_{*}\webleft (\Phi _{K}\webleft (\xi \webright )\webright )\\ & = \webleft [\webleft (\phi _{*}\webright )_{*}\circ \Phi _{K}\webright ]\webleft (\xi \webright ). \end{align*}
- Naturality of $\Psi $. Since $\Phi $ is natural and $\Phi $ is a componentwise inverse to $\Psi $, it follows from Chapter 9: Preorders, Item 2 of Proposition 9.9.7.1.2 that $\Psi $ is also natural.
This finishes the proof.
