The universal property of Definition 5.2.2.1.1 is equivalent to the following one:
- We have a bijection
\[ \mathsf{Sets}_{*}\webleft (K,A\pitchfork X\webright ) \cong \mathsf{Sets}^{\otimes }_{\mathbb {E}_{0}}\webleft (A\times K,X\webright ), \]
natural in $\webleft (K,k_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, where $\mathsf{Sets}^{\otimes }_{\mathbb {E}_{0}}\webleft (A\times K,X\webright )$ is the set defined by
\[ \mathsf{Sets}^{\otimes }_{\mathbb {E}_{0}}\webleft (A\times K,X\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ f\in \mathsf{Sets}\webleft (A\times K,X\webright )\ \middle |\ \begin{aligned} & \text{for each $a\in A$, we}\\ & \text{have $f\webleft (a,k_{0}\webright )=x_{0}$}\end{aligned} \webright\} . \]
