The left unitor of the product of sets is the natural isomorphism
whose component
\[ \lambda ^{\mathsf{Sets}}_{X} \colon \text{pt}\times X \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }X \]
at $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ is given by
\[ \lambda ^{\mathsf{Sets}}_{X}\webleft (\star ,x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}x \]
for each $\webleft (\star ,x\webright )\in \text{pt}\times X$.
Invertibility
The inverse of $\lambda ^{\mathsf{Sets}}_{X}$ is the morphism
\[ \lambda ^{\mathsf{Sets},-1}_{X}\colon X\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\text{pt}\times X \]
defined by
\[ \lambda ^{\mathsf{Sets},-1}_{X}\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\star ,x\webright ) \]
for each $x\in X$. Indeed:
- Invertibility I. We have
\begin{align*} \webleft [\lambda ^{\mathsf{Sets},-1}_{X}\circ \lambda ^{\mathsf{Sets}}_{X}\webright ]\webleft (\text{pt},x\webright ) & = \lambda ^{\mathsf{Sets},-1}_{X}\webleft (\lambda ^{\mathsf{Sets}}_{X}\webleft (\text{pt},x\webright )\webright )\\ & = \lambda ^{\mathsf{Sets},-1}_{X}\webleft (x\webright )\\ & = \webleft (\text{pt},x\webright )\\ & = \webleft [\text{id}_{\text{pt}\times X}\webright ]\webleft (\text{pt},x\webright ) \end{align*}
for each $\webleft (\text{pt},x\webright )\in \text{pt}\times X$, and therefore we have
\[ \lambda ^{\mathsf{Sets},-1}_{X}\circ \lambda ^{\mathsf{Sets}}_{X}=\text{id}_{\text{pt}\times X}. \]
- Invertibility II. We have
\begin{align*} \webleft [\lambda ^{\mathsf{Sets}}_{X}\circ \lambda ^{\mathsf{Sets},-1}_{X}\webright ]\webleft (x\webright ) & = \lambda ^{\mathsf{Sets}}_{X}\webleft (\lambda ^{\mathsf{Sets},-1}_{X}\webleft (x\webright )\webright )\\ & = \lambda ^{\mathsf{Sets},-1}_{X}\webleft (\text{pt},x\webright )\\ & = x\\ & = \webleft [\text{id}_{X}\webright ]\webleft (x\webright ) \end{align*}
for each $x\in X$, and therefore we have
\[ \lambda ^{\mathsf{Sets}}_{X}\circ \lambda ^{\mathsf{Sets},-1}_{X}=\text{id}_{X}. \]
Therefore $\lambda ^{\mathsf{Sets}}_{X}$ is indeed an isomorphism.
Naturality
We need to show that, given a function $f\colon X\to Y$, the diagram
commutes. Indeed, this diagram acts on elements as
and hence indeed commutes. Therefore $\lambda ^{\mathsf{Sets}}$ is a natural transformation.
Being a Natural Isomorphism
Since $\lambda ^{\mathsf{Sets}}$ is natural and $\lambda ^{\mathsf{Sets},-1}$ is a componentwise inverse to $\lambda ^{\mathsf{Sets}}$, it follows from Chapter 9: Preorders, Item 2 of Proposition 9.9.7.1.2 that $\lambda ^{\mathsf{Sets},-1}$ is also natural. Thus $\lambda ^{\mathsf{Sets}}$ is a natural isomorphism.
