Definition 7.4.6.1.1 (00FJ): The Right Skew Right Unitor of $\rhd $

In other words, $\smash {\rho ^{\mathsf{Sets}_{*},\rhd }_{X}}$ acts on elements as

\begin{align*} \rho ^{\mathsf{Sets}_{*},\rhd }_{X}(x\rhd 0) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}x_{0},\\ \rho ^{\mathsf{Sets}_{*},\rhd }_{X}(x\rhd 1) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}x\end{align*}

for each $x\rhd 1\in X\rhd S^{0}$.

The morphism $\smash {\rho ^{\mathsf{Sets}_{*},\rhd }_{X}}$ is almost invertible, with its would-be-inverse

\[ \phi _{X}\colon X\to X\rhd S^{0} \]

given by

\[ \phi _{X}(x)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}x\rhd 1 \]

for each $x\in X$. Indeed, we have

\begin{align*} [\rho ^{\mathsf{Sets}_{*},\rhd }_{X}\circ \phi ](x) & = \rho ^{\mathsf{Sets}_{*},\rhd }_{X}(\phi (x))\\ & = \rho ^{\mathsf{Sets}_{*},\rhd }_{X}(x\rhd 1)\\ & = x\\ & = [\operatorname {\mathrm{id}}_{X}](x) \end{align*}

so that

\[ \rho ^{\mathsf{Sets}_{*},\rhd }_{X}\circ \phi =\operatorname {\mathrm{id}}_{X} \]

and

\begin{align*} [\phi \circ \rho ^{\mathsf{Sets}_{*},\rhd }_{X}](x\rhd 1) & = \phi (\rho ^{\mathsf{Sets}_{*},\rhd }_{X}(x\rhd 1))\\ & = \phi (x)\\ & = x\rhd 1\\ & = [\operatorname {\mathrm{id}}_{X\rhd S^{0}}](x\rhd 1), \end{align*}

but

\begin{align*} [\phi \circ \rho ^{\mathsf{Sets}_{*},\rhd }_{X}](x\rhd 0) & = \phi (\rho ^{\mathsf{Sets}_{*},\rhd }_{X}(x\rhd 0))\\ & = \phi (x_{0})\\ & = 1\rhd x_{0}, \end{align*}

where $x\rhd 0\neq 1\rhd x_{0}$. Thus

\[ \phi \circ \rho ^{\mathsf{Sets}_{*},\rhd }_{X}\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{?}}}=}}\operatorname {\mathrm{id}}_{X\rhd S^{0}} \]

holds for all elements in $X\rhd S^{0}$ except one.

Firstly, note that, given $(X,x_{0})\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{*})$, the map

\[ \rho ^{\mathsf{Sets}_{*},\rhd }_{X} \colon X\rhd S^{0}\to X \]

is indeed a morphism of pointed sets as we have

\[ \rho ^{\mathsf{Sets}_{*},\rhd }_{X}(x_{0}\rhd 0)=x_{0}. \]

Next, we claim that $\rho ^{\mathsf{Sets}_{*},\rhd }$ is a natural transformation. We need to show that, given a morphism of pointed sets

\[ f\colon (X,x_{0})\to (Y,y_{0}), \]

the diagram

commutes. Indeed, this diagram acts on elements as

and

and hence indeed commutes, showing $\rho ^{\mathsf{Sets}_{*},\rhd }$ to be a natural transformation. This finishes the proof.

The Clowder Project

7.4.6 The Right Skew Right Unitor