- Map I. We define a map
\[ \Phi _{X,Y}\colon \mathsf{Sets}_{*}\webleft (X^{+},Y\webright )\to \mathsf{Sets}\webleft (X,Y\webright ) \]
by sending a morphism of pointed sets
\[ \xi \colon \webleft (X^{+},\star _{X}\webright )\to \webleft (Y,y_{0}\webright ) \]
to the function
\[ \xi ^{\dagger }\colon X\to Y \]
given by
\[ \xi ^{\dagger }\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi \webleft (x\webright ) \]
for each $x\in X$.
- Map II. We define a map
\[ \Psi _{X,Y}\colon \mathsf{Sets}\webleft (X,Y\webright )\to \mathsf{Sets}_{*}\webleft (X^{+},Y\webright ) \]
given by sending a function $\xi \colon X\to Y$ to the morphism of pointed sets
\[ \xi ^{\dagger }\colon \webleft (X^{+},\star _{X}\webright )\to \webleft (Y,y_{0}\webright ) \]
defined by
\[ \xi ^{\dagger }\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} \xi \webleft (x\webright ) & \text{if $x\in X$,}\\ y_{0} & \text{if $x=\star _{X}$} \end{cases} \]
for each $x\in X^{+}$.
- Invertibility I. Given a morphism of pointed sets
\[ \xi \colon \webleft (X^{+},\star _{X}\webright )\to \webleft (Y,y_{0}\webright ), \]
we have
\begin{align*} \webleft [\Psi _{X,Y}\circ \Phi _{X,Y}\webright ]\webleft (\xi \webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Psi _{X,Y}\webleft (\Phi _{X,Y}\webleft (\xi \webright )\webright )\\ & = \Psi _{X,Y}\webleft (\xi ^{\dagger }\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft[\mspace {-6mu}\webleft[x\mapsto {\begin{cases} \xi ^{\dagger }\webleft (x\webright )& \text{if $x\in X$}\\ y_{0}& \text{if $x=\star _{X}$}\end{cases}}\webright]\mspace {-6mu}\webright]\\ & = \webleft[\mspace {-6mu}\webleft[x\mapsto {\begin{cases} \xi \webleft (x\webright )& \text{if $x\in X$}\\ y_{0}& \text{if $x=\star _{X}$}\end{cases}}\webright]\mspace {-6mu}\webright]\\ & = \xi \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [\text{id}_{\mathsf{Sets}_{*}\webleft (X^{+},Y\webright )}\webright ]\webleft (\xi \webright ).\end{align*}
Therefore we have
\[ \Psi _{X,Y}\circ \Phi _{X,Y}=\text{id}_{\mathsf{Sets}_{*}\webleft (X^{+},Y\webright )}. \]
- Invertibility II. Given a map of sets $\xi \colon X\to Y$, we have
\begin{align*} \webleft [\Phi _{X,Y}\circ \Psi _{X,Y}\webright ]\webleft (\xi \webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X,Y}\webleft (\Psi _{X,Y}\webleft (\xi \webright )\webright )\\ & = \Phi _{X,Y}\webleft (\xi ^{\dagger }\webright )\\ & = \Phi _{X,Y}\webleft (\webleft[\mspace {-6mu}\webleft[x\mapsto {\begin{cases} \xi \webleft (x\webright )& \text{if $x\in X$}\\ y_{0}& \text{if $x=\star _{X}$}\end{cases}}\webright]\mspace {-6mu}\webright]\webright )\\ & = [\mspace {-3mu}[x\mapsto \xi \webleft (x\webright )]\mspace {-3mu}]\\ & = \xi \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [\text{id}_{\mathsf{Sets}\webleft (X,Y\webright )}\webright ]\webleft (\xi \webright ).\end{align*}
Therefore we have
\[ \Phi _{X,Y}\circ \Psi _{X,Y}=\text{id}_{\mathsf{Sets}\webleft (X,Y\webright )}. \]
- Naturality for $\Phi $, Part I. We need to show that, given a morphism of pointed sets
\[ f\colon \webleft (X,x_{0}\webright )\to \webleft (X',x'_{0}\webright ), \]
the diagram
commutes. Indeed, given a morphism of pointed sets $\xi \colon X^{\prime ,+}\to Y$, we have
\begin{align*} \webleft [\Phi _{X,Y}\circ f^{*}\webright ]\webleft (\xi \webright ) & = \Phi _{X,Y}\webleft (f^{*}\webleft (\xi \webright )\webright )\\ & = \Phi _{X,Y}\webleft (\xi \circ f\webright )\\ & = \xi \circ f\\ & = \Phi _{X',Y}\webleft (\xi \webright )\circ f\\ & = f^{*}\webleft (\Phi _{X',Y}\webleft (\xi \webright )\webright )\\ & = f^{*}\webleft (\Phi _{X',Y}\webleft (\xi \webright )\webright )\\ & = \webleft [f^{*}\circ \Phi _{X',Y}\webright ]\webleft (\xi \webright ). \end{align*}
Therefore we have
\[ \Phi _{X,Y}\circ f^{*}=f^{*}\circ \Phi _{X',Y} \]
and the naturality diagram for $\Phi $ above indeed commutes.
- Naturality for $\Phi $, Part II. We need to show that, given a morphism of pointed sets
\[ g\colon \webleft (Y,y_{0}\webright )\to \webleft (Y',y'_{0}\webright ), \]
the diagram
commutes. Indeed, given a morphism of pointed sets
\[ \xi ^{\dagger }\colon X^{+} \to Y, \]
we have
\begin{align*} \webleft [\Phi _{X,Y'}\circ g_{*}\webright ]\webleft (\xi \webright ) & = \Phi _{X,Y'}\webleft (g_{*}\webleft (\xi \webright )\webright )\\ & = \Phi _{X,Y'}\webleft (g\circ \xi \webright )\\ & = g\circ \xi \\ & = g\circ \Phi _{X,Y'}\webleft (\xi \webright )\\ & = g_{*}\webleft (\Phi _{X,Y'}\webleft (\xi \webright )\webright )\\ & = \webleft [g_{*}\circ \Phi _{X,Y'}\webright ]\webleft (\xi \webright ). \end{align*}
Therefore we have
\[ \Phi _{X,Y'}\circ g_{*}=g_{*}\circ \Phi _{X,Y'} \]
and the naturality diagram for $\Phi $ above indeed commutes.
- 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 9: Preorders, Item 2 of Proposition 9.9.7.1.2 that $\Psi $ is also natural in each argument.
This finishes the proof.
- The Strong Monoidality Constraints. The isomorphism
\[ \webleft (-\webright )^{+,\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{X,Y}\colon X^{+}\vee Y^{+}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright )^{+} \]
is given by
\[ \webleft (-\webright )^{+,\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{X,Y}\webleft (z\webright )=\begin{cases} x & \text{if $z=\webleft [\webleft (0,x\webright )\webright ]$ with $x\in X$,}\\ y & \text{if $z=\webleft [\webleft (1,y\webright )\webright ]$ with $y\in Y$,}\\ \star _{X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y} & \text{if $z=\webleft [\webleft (0,\star _{X}\webright )\webright ]$,}\\ \star _{X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y} & \text{if $z=\webleft [\webleft (1,\star _{Y}\webright )\webright ]$}\end{cases} \]
for each $z\in X^{+}\vee Y^{+}$, with inverse
\[ \webleft (-\webright )^{+,\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},-1}_{X,Y} \colon \webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright )^{+} \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }X^{+}\vee Y^{+} \]
given by
\[ \webleft (-\webright )^{+,\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},-1}_{X,Y}\webleft (z\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} \webleft [\webleft (0,x\webright )\webright ] & \text{if $z=\webleft [\webleft (0,x\webright )\webright ]$,}\\ \webleft [\webleft (1,y\webright )\webright ] & \text{if $z=\webleft [\webleft (1,y\webright )\webright ]$,}\\ p_{0} & \text{if $z=\star _{X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y}$} \end{cases} \]
for each $z\in \webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright )^{+}$.
- The Strong Monoidal Unity Constraint. The isomorphism
\[ \webleft (-\webright )^{+,\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\mathbb {1}}_{X,Y}\colon \text{pt}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\text{Ø}^{+} \]
is given by sending $\star _{X}$ to $\star _{\text{Ø}}$.
The verification that these isomorphisms satisfy the coherence conditions making the functor $\webleft (-\webright )^{+}$ into a symmetric strong monoidal functor is omitted.
- The Strong Monoidality Constraints. The isomorphism
\[ \webleft (-\webright )^{+}_{X,Y}\colon X^{+}\wedge Y^{+}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\webleft (X\times Y\webright )^{+} \]
is given by
\[ \webleft (-\webright )^{+}_{X,Y}\webleft (x\wedge y\webright )=\begin{cases} \webleft (x,y\webright ) & \text{if $x\neq \star _{X}$ and $y\neq \star _{Y}$}\\ \star _{X\times Y} & \text{otherwise}\end{cases} \]
for each $x\wedge y\in X^{+}\wedge Y^{+}$, with inverse
\[ \webleft (-\webright )^{+,-1}_{X,Y} \colon \webleft (X\times Y\webright )^{+} \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }X^{+}\wedge Y^{+} \]
given by
\[ \webleft (-\webright )^{+,-1}_{X,Y}\webleft (z\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} x\wedge y & \text{if $z=\webleft (x,y\webright )$ with $\webleft (x,y\webright )\in X\times Y$,}\\ \star _{X}\wedge \star _{Y} & \text{if $z=\star _{X\times Y}$,} \end{cases} \]
for each $z\in \webleft (X\times Y\webright )^{+}$.
- The Strong Monoidal Unity Constraint. The isomorphism
\[ \webleft (-\webright )^{+,\mathbb {1}}_{X,Y}\colon S^{0}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\text{pt}^{+} \]
is given by sending $0$ to $\star _{\text{pt}}$ and $1$ to $\star $, where $\text{pt}^{+}=\webleft\{ \star ,\star _{\text{pt}}\webright\} $.
The verification that these isomorphisms satisfy the coherence conditions making the functor $\webleft (-\webright )^{+}$ into a symmetric strong monoidal functor is omitted.