The Clowder Project

We claim we have a bijection

natural in $\webleft (K,k_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$. Indeed, this bijection is a restriction of the bijection

of Chapter 2: Constructions With Sets, Item 2 of Proposition 2.1.3.1.2:

• A map
  
  in $\mathsf{Sets}\webleft (A,\mathsf{Sets}_{*}\webleft (X,K\webright )\webright )$ gets sent to the map
  \[ \xi ^{\dagger }\colon A\times X\to K \]

  defined by

  \[ \xi ^{\dagger }\webleft (a,x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi _{a}\webleft (x\webright ) \]

  for each $\webleft (a,x\webright )\in A\times X$, which indeed lies in $\mathsf{Sets}^{\otimes }_{\mathbb {E}_{0}}\webleft (A\times X,K\webright )$, as we have

  \begin{align*} \xi ^{\dagger }\webleft (a,x_{0}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi _{a}\webleft (x_{0}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}k_{0}\end{align*}

  for each $a\in A$, where we have used that $\xi _{a}\in \mathsf{Sets}_{*}\webleft (X,K\webright )$ is a morphism of pointed sets.

• Conversely, a map
  \[ \xi \colon A\times X\to K \]

  in $\mathsf{Sets}^{\otimes }_{\mathbb {E}_{0}}\webleft (A\times X,K\webright )$ gets sent to the map

  
  where
  \[ \xi ^{\dagger }_{a}\colon X \to K \]

  is the map defined by

  \[ \xi ^{\dagger }_{a}\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi \webleft (a,x\webright ) \]

  for each $x\in X$, and indeed lies in $\mathsf{Sets}_{*}\webleft (X,K\webright )$, as we have

  \begin{align*} \xi ^{\dagger }_{a}\webleft (x_{0}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi \webleft (a,x_{0}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}k_{0}.\end{align*}