The Clowder Project

defined by

for each $x\in X$. Indeed:

• Invertibility I. We have
  $$\begin{array}{rl}[{\lambda }_X^{\mathsf{Sets},-1}\circ {\lambda }_X^{\mathsf{Sets}}](\text{pt},x)& ={\lambda }_X^{\mathsf{Sets},-1}\left({\lambda }_X^{\mathsf{Sets}}(\text{pt},x)\right)\\ & ={\lambda }_X^{\mathsf{Sets},-1}\left(x\right)\\ & =(\text{pt},x)\\ & =\left[{\text{id}}_{\text{pt}\times X}\right](\text{pt},x)\end{array}$$

  for each $(\text{pt},x)\in \text{pt}\times X$, and therefore we have

  $${\lambda }_X^{\mathsf{Sets},-1}\circ {\lambda }_X^{\mathsf{Sets}}={\text{id}}_{\text{pt}\times X}.$$

• Invertibility II. We have
  $$\begin{array}{rl}[{\lambda }_X^{\mathsf{Sets}}\circ {\lambda }_X^{\mathsf{Sets},-1}]\left(x\right)& ={\lambda }_X^{\mathsf{Sets}}\left({\lambda }_X^{\mathsf{Sets},-1}\left(x\right)\right)\\ & ={\lambda }_X^{\mathsf{Sets},-1}(\text{pt},x)\\ & =x\\ & =\left[{\text{id}}_X\right]\left(x\right)\end{array}$$

  for each $x\in X$, and therefore we have

  $${\lambda }_X^{\mathsf{Sets}}\circ {\lambda }_X^{\mathsf{Sets},-1}={\text{id}}_X.$$

commutes. Indeed, this diagram acts on elements as