The Clowder Project

• •

  Preservation of Identities. Let $X\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$. We have

  \[ \operatorname {\mathrm{id}}^{+}_{X}(x)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} x & \text{if $x\in X$,}\\ \star _{X} & \text{if $x=\star _{X}$,} \end{cases} \]

  for each $x\in X^{+}$, so $\operatorname {\mathrm{id}}^{+}_{X}=\operatorname {\mathrm{id}}_{X^{+}}$.

• •

  Preservation of Composition. Given morphisms of sets

  \begin{align*} f & \colon X \to Y,\\ g & \colon Y \to Z, \end{align*}

  we have

  \begin{align*} [g^{+}\circ f^{+}](x) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g^{+}(f^{+}(x))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g^{+}(f(x))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g(f(x))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[g\circ f]^{+}(x)\end{align*}

  for each $x\in X$ and

  \begin{align*} [g^{+}\circ f^{+}](\star _{X}) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g^{+}(f^{+}(\star _{X}))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g^{+}(\star _{Y})\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\star _{Z}\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[g\circ f]^{+}(\star _{X}), \end{align*}

  so $(g\circ f)^{+}=g^{+}\circ f^{+}$.

This finishes the proof.

• •

  Map I. We define a map

  \[ \Phi _{X,Y}\colon \mathsf{Sets}_{*}(X^{+},Y)\to \mathsf{Sets}(X,Y) \]

  by sending a morphism of pointed sets

  \[ \xi \colon (X^{+},\star _{X})\to (Y,y_{0}) \]

  to the function

  \[ \xi ^{\dagger }\colon X\to Y \]

  given by

  \[ \xi ^{\dagger }(x)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi (x) \]

  for each $x\in X$.

• •

  Map II. We define a map

  \[ \Psi _{X,Y}\colon \mathsf{Sets}(X,Y)\to \mathsf{Sets}_{*}(X^{+},Y) \]

  given by sending a function $\xi \colon X\to Y$ to the morphism of pointed sets

  \[ \xi ^{\dagger }\colon (X^{+},\star _{X})\to (Y,y_{0}) \]

  defined by

  \[ \xi ^{\dagger }(x)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} \xi (x) & \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 (X^{+},\star _{X})\to (Y,y_{0}), \]

  we have

  \begin{align*} [\Psi _{X,Y}\circ \Phi _{X,Y}](\xi ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Psi _{X,Y}(\Phi _{X,Y}(\xi ))\\ & = \Psi _{X,Y}(\xi ^{\dagger })\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left[\mspace {-6mu}\left[x\mapsto {\begin{cases} \xi ^{\dagger }(x)& \text{if $x\in X$}\\ y_{0}& \text{if $x=\star _{X}$}\end{cases}}\right]\mspace {-6mu}\right]\\ & = \left[\mspace {-6mu}\left[x\mapsto {\begin{cases} \xi (x)& \text{if $x\in X$}\\ y_{0}& \text{if $x=\star _{X}$}\end{cases}}\right]\mspace {-6mu}\right]\\ & = \xi \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[\operatorname {\mathrm{id}}_{\mathsf{Sets}_{*}(X^{+},Y)}](\xi ).\end{align*}

  Therefore we have

  \[ \Psi _{X,Y}\circ \Phi _{X,Y}=\operatorname {\mathrm{id}}_{\mathsf{Sets}_{*}(X^{+},Y)}. \]
• •

  Invertibility II. Given a map of sets $\xi \colon X\to Y$, we have

  \begin{align*} [\Phi _{X,Y}\circ \Psi _{X,Y}](\xi ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X,Y}(\Psi _{X,Y}(\xi ))\\ & = \Phi _{X,Y}(\xi ^{\dagger })\\ & = \Phi _{X,Y}(\left[\mspace {-6mu}\left[x\mapsto {\begin{cases} \xi (x)& \text{if $x\in X$}\\ y_{0}& \text{if $x=\star _{X}$}\end{cases}}\right]\mspace {-6mu}\right])\\ & = [\mspace {-3mu}[x\mapsto \xi (x)]\mspace {-3mu}]\\ & = \xi \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[\operatorname {\mathrm{id}}_{\mathsf{Sets}(X,Y)}](\xi ).\end{align*}

  Therefore we have

  \[ \Phi _{X,Y}\circ \Psi _{X,Y}=\operatorname {\mathrm{id}}_{\mathsf{Sets}(X,Y)}. \]
• •

  Naturality for $\Phi $, Part I. We need to show that, given a morphism of pointed sets

  \[ f\colon (X,x_{0})\to (X',x'_{0}), \]

  the diagram

  
  commutes. Indeed, given a morphism of pointed sets $\xi \colon X^{\prime ,+}\to Y$, we have
  \begin{align*} [\Phi _{X,Y}\circ f^{*}](\xi ) & = \Phi _{X,Y}(f^{*}(\xi ))\\ & = \Phi _{X,Y}(\xi \circ f)\\ & = \xi \circ f\\ & = \Phi _{X',Y}(\xi )\circ f\\ & = f^{*}(\Phi _{X',Y}(\xi ))\\ & = f^{*}(\Phi _{X',Y}(\xi ))\\ & = [f^{*}\circ \Phi _{X',Y}](\xi ). \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 (Y,y_{0})\to (Y',y'_{0}), \]

  the diagram

  
  commutes. Indeed, given a morphism of pointed sets
  \[ \xi ^{\dagger }\colon X^{+} \to Y, \]

  we have

  \begin{align*} [\Phi _{X,Y'}\circ g_{*}](\xi ) & = \Phi _{X,Y'}(g_{*}(\xi ))\\ & = \Phi _{X,Y'}(g\circ \xi )\\ & = g\circ \xi \\ & = g\circ \Phi _{X,Y'}(\xi )\\ & = g_{*}(\Phi _{X,Y'}(\xi ))\\ & = [g_{*}\circ \Phi _{X,Y'}](\xi ). \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 11: Categories, Item 2 of Proposition 11.9.7.1.2 that $\Psi $ is also natural in each argument.

This finishes the proof.

• •

  The Strong Monoidality Constraints. The isomorphism

  \[ (-)^{+,\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 }(X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y)^{+} \]

  is given by

  \[ (-)^{+,\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{X,Y}(z)=\begin{cases} x & \text{if $z=[(0,x)]$ with $x\in X$,}\\ y & \text{if $z=[(1,y)]$ 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=[(0,\star _{X})]$,}\\ \star _{X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y} & \text{if $z=[(1,\star _{Y})]$}\end{cases} \]

  for each $z\in X^{+}\vee Y^{+}$, with inverse

  \[ (-)^{+,\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},-1}_{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 }X^{+}\vee Y^{+} \]

  given by

  \[ (-)^{+,\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},-1}_{X,Y}(z)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} [(0,x)] & \text{if $z=[(0,x)]$,}\\ [(1,y)] & \text{if $z=[(1,y)]$,}\\ 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 (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y)^{+}$.

• •

  The Strong Monoidal Unity Constraint. The isomorphism

  \[ (-)^{+,\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\mathbb {1}}_{X,Y}\colon \mathrm{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 $(-)^{+}$ into a symmetric strong monoidal functor is omitted.

• •

  The Strong Monoidality Constraints. The isomorphism

  \[ (-)^{+}_{X,Y}\colon X^{+}\wedge Y^{+}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }(X\times Y)^{+} \]

  is given by

  \[ (-)^{+}_{X,Y}(x\wedge y)=\begin{cases} (x,y) & \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

  \[ (-)^{+,-1}_{X,Y} \colon (X\times Y)^{+} \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }X^{+}\wedge Y^{+} \]

  given by

  \[ (-)^{+,-1}_{X,Y}(z)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} x\wedge y & \text{if $z=(x,y)$ with $(x,y)\in X\times Y$,}\\ \star _{X}\wedge \star _{Y} & \text{if $z=\star _{X\times Y}$,} \end{cases} \]

  for each $z\in (X\times Y)^{+}$.

• •

  The Strong Monoidal Unity Constraint. The isomorphism

  \[ (-)^{+,\mathbb {1}}_{X,Y}\colon S^{0}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\mathrm{pt}^{+} \]

  is given by sending $0$ to $\star _{\mathrm{pt}}$ and $1$ to $\star $, where $\mathrm{pt}^{+}=\left\{ \star ,\star _{\mathrm{pt}}\right\} $.

The verification that these isomorphisms satisfy the coherence conditions making the functor $(-)^{+}$ into a symmetric strong monoidal functor is omitted.