- Map I. We define a map
\[ \Phi _{X,Y}\colon \mathsf{Sets}\webleft (X^{-},Y\webright )\to \mathsf{Sets}^{\mathrm{actv}}_{*}\webleft (X,Y^{+}\webright ) \]
by sending a map $\xi \colon X^{-}\to Y$ to the active morphism of pointed sets
\[ \xi ^{\dagger }\colon X\to Y^{+} \]
given by
\[ \xi ^{\dagger }\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} \xi \webleft (x\webright ) & \text{if $x\in X^{-}$,}\\ \star _{Y} & \text{if $x=x_{0}$,} \end{cases} \]
for each $x\in X$, where this morphism is indeed active since $\xi \webleft (x\webright )\in Y=Y^{+}\setminus \webleft\{ \star _{Y}\webright\} $ for all $x\in X^{-}$.
- Map II. We define a map
\[ \Psi _{X,Y}\colon \mathsf{Sets}^{\mathrm{actv}}_{*}\webleft (X,Y^{+}\webright )\to \mathsf{Sets}\webleft (X^{-},Y\webright ) \]
given by sending an active morphism of pointed sets $\xi \colon X\to Y^{+}$ to the map
\[ \xi ^{\dagger }\colon X^{-}\to Y \]
defined by
\[ \xi ^{\dagger }\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi \webleft (x\webright ) \]
for each $x\in X^{-}$, which is indeed well-defined (in that $\xi \webleft (x\webright )\in Y$ for all $x\in X^{-}$) since $\xi $ is active.
- Invertibility I. Given a map of sets $\xi \colon X^{-}\to Y$, 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 )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Psi _{X,Y}\webleft (\webleft[\mspace {-6mu}\webleft[x\mapsto {\begin{cases} \xi \webleft (x\webright )& \text{if $x\in X^{-}$}\\ \star _{Y}& \text{if $x=x_{0}$}\end{cases}}\webright]\mspace {-6mu}\webright]\webright )\\ & = [\mspace {-3mu}[x\mapsto \xi \webleft (x\webright )]\mspace {-3mu}]\\ & = \xi \\ & = \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 morphism of pointed sets
\[ \xi \colon \webleft (X,x_{0}\webright )\to \webleft (Y^{+},\star _{Y}\webright ), \]
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 ([\mspace {-3mu}[x\mapsto \xi \webleft (x\webright )]\mspace {-3mu}]\webright )\\ & = \webleft[\mspace {-6mu}\webleft[x\mapsto {\begin{cases} \xi \webleft (x\webright )& \text{if $x\in X^{-}$}\\ \star _{Y}& \text{if $x=x_{0}$}\end{cases}}\webright]\mspace {-6mu}\webright]\\ & = \xi \\ & = \webleft [\text{id}_{\mathsf{Sets}^{\mathrm{actv}}_{*}\webleft (X,Y^{+}\webright )}\webright ]\webleft (\xi \webright ). \end{align*}
Therefore we have
\[ \Phi _{X,Y}\circ \Psi _{X,Y}=\text{id}_{\mathsf{Sets}^{\mathrm{actv}}_{*}\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 map of sets $\xi \colon X'\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 )\\ & = \webleft[\mspace {-6mu}\webleft[x\mapsto {\begin{cases} \xi \webleft (f\webleft (x\webright )\webright )& \text{if $f\webleft (x\webright )\in X^{\prime ,-}$}\\ \star _{Y}& \text{if $f\webleft (x\webright )=x'_{0}$}\end{cases}}\webright]\mspace {-6mu}\webright]\\ & = f^{*}\webleft (\webleft[\mspace {-6mu}\webleft[x'\mapsto {\begin{cases} \xi \webleft (x'\webright )& \text{if $x'\in X^{\prime ,-}$}\\ \star _{Y}& \text{if $x'=x'_{0}$}\end{cases}}\webright]\mspace {-6mu}\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 map of sets $\xi \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 )\\ & = \webleft[\mspace {-6mu}\webleft[x\mapsto {\begin{cases} g\webleft (\xi \webleft (x\webright )\webright )& \text{if $x\in X^{-}$}\\ \star _{Y'}& \text{if $x=x_{0}$}\end{cases}}\webright]\mspace {-6mu}\webright]\\ & = g_{*}\webleft (\webleft[\mspace {-6mu}\webleft[x\mapsto {\begin{cases} \xi \webleft (x\webright )& \text{if $x\in X^{-}$}\\ \star _{Y}& \text{if $x=x_{0}$}\end{cases}}\webright]\mspace {-6mu}\webright]\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.
- Fully Faithfulness of $\webleft (-\webright )^{-}$. We aim to show that the assignment $f\mapsto f^{-}$ sets up a bijection
\[ \webleft (-\webright )^{-}_{X,Y}\colon \mathsf{Sets}^{\mathrm{actv}}_{*}\webleft (X,Y\webright )\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\mathsf{Sets}\webleft (X^{-},Y^{-}\webright ). \]
Indeed, the inverse map
\[ \webleft (-\webright )^{-,-1}_{X,Y}\colon \mathsf{Sets}\webleft (X^{-},Y^{-}\webright )\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\mathsf{Sets}^{\mathrm{actv}}_{*}\webleft (X,Y\webright ) \]
is given by sending a map of sets $f\colon X^{-}\to Y^{-}$ to the active morphism of pointed sets $f^{\dagger }\colon X\to Y$ defined by
\[ f^{\dagger }\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} f\webleft (x\webright ) & \text{if $x\in X^{-}$,}\\ y_{0} & \text{if $x=x_{0}$} \end{cases} \]
for each $x\in X$.
- Essential Surjectivity of $\webleft (-\webright )^{-}$. We need to show that, given an object $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, there exists some $X'\in \text{Obj}\webleft (\mathsf{Sets}^{\mathrm{actv}}_{*}\webright )$ such that $\webleft (X'\webright )^{-}\cong X$. Indeed, taking $X'=X^{+}$, we have
\begin{align*} \webleft (X^{+}\webright )^{-} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (X\cup \webleft\{ \star _{X}\webright\} \webright )^{-}\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (X\cup \webleft\{ \star _{X}\webright\} \webright )\setminus \webleft\{ \star _{X}\webright\} \\ & = X, \end{align*}
and thus we have in fact an equality $\webleft (X^{+}\webright )^{-}=X$, showing $\webleft (-\webright )^{-}$ to be essentially surjective.
- The Functor $\webleft (-\webright )^{-}$ Is an Equivalence. Since $\webleft (-\webright )^{-}$ is fully faithful and essentially surjective, it is an equivalence by Chapter 9: Preorders, Item 1 of Proposition 9.6.7.1.2.
This finishes the proof.
- The Strong Monoidality Constraints. The isomorphism
\[ \webleft (-\webright )^{-,\vee }_{X,Y}\colon X^{-}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y^{-}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\webleft (X\vee Y\webright )^{-} \]
is given by
\[ \webleft (-\webright )^{-,\vee }_{X,Y}\webleft (z\webright )=\begin{cases} \webleft [\webleft (0,x\webright )\webright ] & \text{if $z=\webleft (0,x\webright )$ with $x\in X$,}\\ \webleft [\webleft (1,y\webright )\webright ] & \text{if $z=\webleft (1,y\webright )$ with $y\in Y$}\end{cases} \]
for each $z\in X^{-}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y^{-}$, with inverse
\[ \webleft (-\webright )^{-,\vee ,-1}_{X,Y} \colon \webleft (X\vee Y\webright )^{-} \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }X^{-}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y^{-} \]
given by
\[ \webleft (-\webright )^{-,\vee ,-1}_{X,Y}\webleft (z\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} \webleft (0,x\webright ) & \text{if $z=\webleft [\webleft (0,x\webright )\webright ]$,}\\ \webleft (1,y\webright ) & \text{if $z=\webleft [\webleft (1,y\webright )\webright ]$,} \end{cases} \]
for each $z\in \webleft (X\vee Y\webright )^{-}$.
- The Strong Monoidal Unity Constraint. The isomorphism
\[ \webleft (-\webright )^{+,\vee ,\mathbb {1}}_{X,Y}\colon \text{Ø}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\text{pt}^{-} \]
is an equality.
The verification that these isomorphisms satisfy the coherence conditions making the functor $\webleft (-\webright )^{-}$ into a symmetric strong monoidal functor is omitted.
\begin{align*} \mathsf{Sets}\webleft (X^{-},Y\webright )\cong \mathsf{Sets}_{*}\webleft (X,Y^{+}\webright ),\end{align*}
