7.4.6 The Right Skew Right Unitor
The skew right unitor of the right tensor product of pointed sets is the natural transformation
whose component
\[ \rho ^{\mathsf{Sets}_{*},\rhd }_{X} \colon X\rhd S^{0}\to X \]
at $(X,x_{0})\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{*})$ is given by the composition
\begin{align*} X\rhd S^{0} & \cong |X|\odot S^{0}\\ & \cong \bigvee _{x\in X}S^{0}\\ & \rightarrow X, \end{align*}
where $\bigvee _{x\in X}S^{0}\to X$ is the map given by
\begin{align*} [(x,0)] & \mapsto x_{0},\\ [(x,1)] & \mapsto x \end{align*}
for each $x\in X$.
(Proven below in a bit.)
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.
