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