Definition 7.3.5.1.1 (00E5): The Left Skew Left Unitor of $\lhd $

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

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

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

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

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

given by

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

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

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

so that

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

and

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

but

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

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

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

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

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

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

is indeed a morphism of pointed sets, as we have

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

Next, we claim that $\lambda ^{\mathsf{Sets}_{*},\lhd }$ 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 $\lambda ^{\mathsf{Sets}_{*},\lhd }$ to be a natural transformation. This finishes the proof.

The Clowder Project

7.3.5 The Left Skew Left Unitor