Let \\(x\in\mathcal{X}\\).
\[ \lambda_\mathcal{X}^{-1}(x)=I\otimes x.\]
\[ ( \cap\_\mathcal{X}\otimes1\_\mathcal{X})(I\otimes x)=\bigvee\_{y\in\mathcal{X}}(y\otimes y^\mathrm{op})\otimes x .\]
\[ \alpha_\mathcal{X,X^\mathrm{op},X}(\bigvee\_{y\in\mathcal{X}}(y\otimes y^\mathrm{op})\otimes x)=\bigvee\_{y\in\mathcal{X}}y\otimes(y^\mathrm{op}\otimes x). \]
\[ (1\_\mathcal{X}\otimes\cup\_\mathcal{X})(\bigvee\_{y\in\mathcal{X}}y\otimes(y^\mathrm{op}\otimes x))=(x\otimes I)\vee(\bigvee\_{y\neq x}y\otimes0)=(x\otimes I)\vee 0=x\otimes I.\]
\[ \rho_\mathcal{X}(x\otimes I)=x.\]
So, the first composite is the identity.
Let \\(x\in\mathcal{X^\mathrm{op}}\\).
\[ \rho_\mathcal{X^\mathrm{op}}^{-1}(x)=x\otimes I.\]
\[ (1\_\mathcal{X}\otimes\cap\_\mathcal{X})(x\otimes I)=\bigvee\_{y\in\mathcal{X}}x\otimes(y\otimes y^\mathrm{op}).\]
\[ \alpha_\mathcal{X^\mathrm{op},X,X^\mathrm{op}}^{-1}(\bigvee\_{y\in\mathcal{X}}x\otimes(y\otimes y^\mathrm{op}))=\bigvee\_{y\in\mathcal{X}}(x\otimes y)\otimes y^\mathrm{op}.\]
\[ (\cup\_\mathcal{X}\otimes1\_\mathcal{X^\mathrm{op}})(\bigvee\_{y\in\mathcal{X}}(x\otimes y)\otimes y^\mathrm{op})=(I\otimes x)\vee(\bigvee\_{y\neq x}0\otimes y^\mathrm{op})=(I\otimes x)\vee 0=I\otimes x .\]
\[ \lambda_\mathcal{X^\mathrm{op}}(I\otimes x)=x.\]
So, the second composite is the identity as well.
\[ \lambda_\mathcal{X}^{-1}(x)=I\otimes x.\]
\[ ( \cap\_\mathcal{X}\otimes1\_\mathcal{X})(I\otimes x)=\bigvee\_{y\in\mathcal{X}}(y\otimes y^\mathrm{op})\otimes x .\]
\[ \alpha_\mathcal{X,X^\mathrm{op},X}(\bigvee\_{y\in\mathcal{X}}(y\otimes y^\mathrm{op})\otimes x)=\bigvee\_{y\in\mathcal{X}}y\otimes(y^\mathrm{op}\otimes x). \]
\[ (1\_\mathcal{X}\otimes\cup\_\mathcal{X})(\bigvee\_{y\in\mathcal{X}}y\otimes(y^\mathrm{op}\otimes x))=(x\otimes I)\vee(\bigvee\_{y\neq x}y\otimes0)=(x\otimes I)\vee 0=x\otimes I.\]
\[ \rho_\mathcal{X}(x\otimes I)=x.\]
So, the first composite is the identity.
Let \\(x\in\mathcal{X^\mathrm{op}}\\).
\[ \rho_\mathcal{X^\mathrm{op}}^{-1}(x)=x\otimes I.\]
\[ (1\_\mathcal{X}\otimes\cap\_\mathcal{X})(x\otimes I)=\bigvee\_{y\in\mathcal{X}}x\otimes(y\otimes y^\mathrm{op}).\]
\[ \alpha_\mathcal{X^\mathrm{op},X,X^\mathrm{op}}^{-1}(\bigvee\_{y\in\mathcal{X}}x\otimes(y\otimes y^\mathrm{op}))=\bigvee\_{y\in\mathcal{X}}(x\otimes y)\otimes y^\mathrm{op}.\]
\[ (\cup\_\mathcal{X}\otimes1\_\mathcal{X^\mathrm{op}})(\bigvee\_{y\in\mathcal{X}}(x\otimes y)\otimes y^\mathrm{op})=(I\otimes x)\vee(\bigvee\_{y\neq x}0\otimes y^\mathrm{op})=(I\otimes x)\vee 0=I\otimes x .\]
\[ \lambda_\mathcal{X^\mathrm{op}}(I\otimes x)=x.\]
So, the second composite is the identity as well.
Version 2.1.8p2
