Options

Exercise 62 - Chapter 4

Check these proposed units and counits do indeed obey the snake equations Eq. (4.57).

Comments

  • 1.

    In order to check the snake equations, one must first define an associator profunctor. As in the previous exercise, this will be defined in terms of a functor \(\newcommand{\Ob}[1]{\mathrm{Ob}(#1)}\newcommand{\Op}[1]{(#1)^\mathrm{op}}\newcommand{\cat}[1]{\mathcal{#1}} \alpha_{\cat{A},\cat{B},\cat{C}}:\Ob{\cat{A}\times(\cat{B}\times\cat{C})}\times\Ob{(\cat{A}\times\cat{B})\times\cat{C}}\to\cat{V}\) and by checking the consistency condition.

    Define \[\alpha_{\cat{A},\cat{B},\cat{C}}((a\times b)\times c,a'\times(b'\times c')):=\cat{A}(a,a')\otimes\cat{B}(b,b')\otimes\cat{C}(c,c')\]. Note: since \(\cat{V}\) is a quantale (and so, in particular, symmetric monoidal), the left-hand side is unambiguous (either placement of parentheses yields a value that is the same as that of the other).

    \begin{align}((&\cat{A}\times\cat{B})\times\cat{C})((a\times b)\times c,(a'\times b')\times c')\otimes\alpha_{\cat{A},\cat{B},\cat{C}}((a'\times b')\times c',a''\times(b''\times c''))\otimes(\cat{A}\times(\cat{B}\times\cat{C}))(a''\times(b''\times c''),a''\times(b'''\times c'''))\\=&(\cat{A}\times\cat{B})(a\times b,a'\times b')\otimes\cat{C}(c,c')\otimes\alpha_{\cat{A},\cat{B},\cat{C}}((a'\times b')\times c',a''\times(b''\times c''))\otimes(\cat{A}\times(\cat{B}\times\cat{C}))(a''\times(b''\times c''),a''\times(b'''\times c'''))\\=&\cat{A}(a,a')\otimes\cat{B}(b,b')\otimes\cat{C}(c,c')\otimes\alpha_{\cat{A},\cat{B},\cat{C}}((a'\times b')\times c',a''\times(b''\times c''))\otimes(\cat{A}\times(\cat{B}\times\cat{C}))(a''\times(b''\times c''),a''\times(b'''\times c'''))\\=&\cat{A}(a,a')\otimes\cat{B}(b,b')\otimes\cat{C}(c,c')\otimes\cat{A}(a',a'')\otimes\cat{B}(b',b'')\otimes\cat{C}(c',c'')\otimes(\cat{A}\times(\cat{B}\times\cat{C}))(a''\times(b''\times c''),a''\times(b'''\times c'''))\\=&\cat{A}(a,a')\otimes\cat{B}(b,b')\otimes\cat{C}(c,c')\otimes\cat{A}(a',a'')\otimes\cat{B}(b',b'')\otimes\cat{C}(c',c'')\otimes\cat{A}(a'',a''')\otimes(\cat{B}\times\cat{C})(b''\times c'',b'''\times c''')\\=&\cat{A}(a,a')\otimes\cat{B}(b,b')\otimes\cat{C}(c,c')\otimes\cat{A}(a',a'')\otimes\cat{B}(b',b'')\otimes\cat{C}(c',c'')\otimes\cat{A}(a'',a''')\otimes\cat{B}(b'',b''')\otimes\cat{C}(c'',c''')\\=&\cat{A}(a,a')\otimes\cat{A}(a',a'')\otimes\cat{A}(a'',a''')\otimes\cat{B}(b,b')\otimes\cat{B}(b',b'')\otimes\cat{B}(b'',b''')\otimes\cat{C}(c,c')\otimes\cat{C}(c',c'')\otimes\cat{C}(c'',c''')\\=&\cat{A}(a,a'')\otimes\cat{A}(a'',a''')\otimes\cat{B}(b,b'')\otimes\cat{B}(b'',b''')\otimes\cat{C}(c,c'')\otimes\cat{C}(c'',c''')\\=&\cat{A}(a,a''')\otimes\cat{B}(b,b''')\otimes\cat{C}(c,c''')\\=&\alpha_{\cat{A},\cat{B},\cat{C}}((a\times b)\times c,a'''\times(b'''\times c'''))\end{align}. So, \(\alpha_{\cat{A},\cat{B},\cat{C}}\) is a profunctor. Its inverse is equal to itself \(\alpha_{\cat{A},\cat{B},\cat{C}}^{-1}(a\times(b\times c),(a'\times b')\times c'):=\cat{A}(a,a')\otimes\cat{B}(b,b')\otimes\cat{C}(c,c')\).

    \begin{align}\alpha_{\cat{A},\cat{B},\cat{C}}^{-1}\circ\alpha_{\cat{A},\cat{B},\cat{C}}((a\times b)\times c,(a''\times b'')\times c'')=&\bigvee_{a'''\in\cat{A},b'''\in\cat{B},c'''\in\cat{C}}\cat{A}(a,a''')\otimes\cat{B}(b,b''')\otimes\cat{C}(c,c''')\otimes\cat{A}(a''',a'')\otimes\cat{B}(b''',b'')\otimes\cat{C}(c''',c'')\\=&\bigvee_{a'''\in\cat{A},b'''\in\cat{B},c'''\in\cat{C}}\cat{A}(a,a''')\otimes\cat{A}(a''',a'')\otimes\cat{B}(b,b''')\otimes\cat{B}(b''',b'')\otimes\cat{C}(c,c''')\otimes\cat{C}(c''',c'')\\=&\cat{A}(a,a'')\otimes\cat{B}(b,b'')\otimes\cat{C}(c,c'')\\=&(\cat{A}\times\cat{B})(a\times b,a''\times b'')\otimes\cat{C}(c,c'')\\=&U_{(\cat{A}\times\cat{B})\times\cat{C}}((a\times b)\times c,(a''\times b'')\times c'')\end{align},

    and \begin{align}\alpha_{\cat{A},\cat{B},\cat{C}}\circ\alpha_{\cat{A},\cat{B},\cat{C}}^{-1}(a\times(b\times c),a''\times(b''\times c''))=&\bigvee_{a'''\in\cat{A},b'''\in\cat{B},c'''\in\cat{C}}\cat{A}(a,a''')\otimes\cat{B}(b,b''')\otimes\cat{C}(c,c''')\otimes\cat{A}(a''',a'')\otimes\cat{B}(b''',b'')\otimes\cat{C}(c''',c'')\\=&\bigvee_{a'''\in\cat{A},b'''\in\cat{B},c'''\in\cat{C}}\cat{A}(a,a''')\otimes\cat{A}(a''',a'')\otimes\cat{B}(b,b''')\otimes\cat{B}(b''',b'')\otimes\cat{C}(c,c''')\otimes\cat{C}(c''',c'')\\=&\cat{A}(a,a'')\otimes\cat{B}(b,b'')\otimes\cat{C}(c,c'')\\=&\cat{A}(a,a'')\otimes(\cat{B}\times\cat{C})(b\times c,b\times c'')\\=&U_{\cat{A}\times(\cat{B}\times\cat{C})}(a\times(b\times c),a''\times(b''\times c''))\end{align}. So, these profunctors are mutually isomorphic.

    Comment Source:In order to check the snake equations, one must first define an associator profunctor. As in the [previous exercise](https://forum.azimuthproject.org/discussion/2324/exercise-61-chapter-4), this will be defined in terms of a functor \\(\newcommand{\Ob}[1]{\mathrm{Ob}(#1)}\newcommand{\Op}[1]{(#1)^\mathrm{op}}\newcommand{\cat}[1]{\mathcal{#1}} \alpha\_{\cat{A},\cat{B},\cat{C}}:\Ob{\cat{A}\times(\cat{B}\times\cat{C})}\times\Ob{(\cat{A}\times\cat{B})\times\cat{C}}\to\cat{V}\\) and by checking the consistency condition. Define \\[\alpha\_{\cat{A},\cat{B},\cat{C}}((a\times b)\times c,a'\times(b'\times c')):=\cat{A}(a,a')\otimes\cat{B}(b,b')\otimes\cat{C}(c,c')\\]. Note: since \\(\cat{V}\\) is a quantale (and so, in particular, symmetric monoidal), the left-hand side is unambiguous (either placement of parentheses yields a value that is the same as that of the other). \begin{align}((&\cat{A}\times\cat{B})\times\cat{C})((a\times b)\times c,(a'\times b')\times c')\otimes\alpha\_{\cat{A},\cat{B},\cat{C}}((a'\times b')\times c',a''\times(b''\times c''))\otimes(\cat{A}\times(\cat{B}\times\cat{C}))(a''\times(b''\times c''),a''\times(b'''\times c'''))\\\\=&(\cat{A}\times\cat{B})(a\times b,a'\times b')\otimes\cat{C}(c,c')\otimes\alpha\_{\cat{A},\cat{B},\cat{C}}((a'\times b')\times c',a''\times(b''\times c''))\otimes(\cat{A}\times(\cat{B}\times\cat{C}))(a''\times(b''\times c''),a''\times(b'''\times c'''))\\\\=&\cat{A}(a,a')\otimes\cat{B}(b,b')\otimes\cat{C}(c,c')\otimes\alpha\_{\cat{A},\cat{B},\cat{C}}((a'\times b')\times c',a''\times(b''\times c''))\otimes(\cat{A}\times(\cat{B}\times\cat{C}))(a''\times(b''\times c''),a''\times(b'''\times c'''))\\\\=&\cat{A}(a,a')\otimes\cat{B}(b,b')\otimes\cat{C}(c,c')\otimes\cat{A}(a',a'')\otimes\cat{B}(b',b'')\otimes\cat{C}(c',c'')\otimes(\cat{A}\times(\cat{B}\times\cat{C}))(a''\times(b''\times c''),a''\times(b'''\times c'''))\\\\=&\cat{A}(a,a')\otimes\cat{B}(b,b')\otimes\cat{C}(c,c')\otimes\cat{A}(a',a'')\otimes\cat{B}(b',b'')\otimes\cat{C}(c',c'')\otimes\cat{A}(a'',a''')\otimes(\cat{B}\times\cat{C})(b''\times c'',b'''\times c''')\\\\=&\cat{A}(a,a')\otimes\cat{B}(b,b')\otimes\cat{C}(c,c')\otimes\cat{A}(a',a'')\otimes\cat{B}(b',b'')\otimes\cat{C}(c',c'')\otimes\cat{A}(a'',a''')\otimes\cat{B}(b'',b''')\otimes\cat{C}(c'',c''')\\\\=&\cat{A}(a,a')\otimes\cat{A}(a',a'')\otimes\cat{A}(a'',a''')\otimes\cat{B}(b,b')\otimes\cat{B}(b',b'')\otimes\cat{B}(b'',b''')\otimes\cat{C}(c,c')\otimes\cat{C}(c',c'')\otimes\cat{C}(c'',c''')\\\\=&\cat{A}(a,a'')\otimes\cat{A}(a'',a''')\otimes\cat{B}(b,b'')\otimes\cat{B}(b'',b''')\otimes\cat{C}(c,c'')\otimes\cat{C}(c'',c''')\\\\=&\cat{A}(a,a''')\otimes\cat{B}(b,b''')\otimes\cat{C}(c,c''')\\\\=&\alpha\_{\cat{A},\cat{B},\cat{C}}((a\times b)\times c,a'''\times(b'''\times c'''))\end{align}. So, \\(\alpha\_{\cat{A},\cat{B},\cat{C}}\\) is a profunctor. Its inverse is equal to itself \\(\alpha\_{\cat{A},\cat{B},\cat{C}}^{-1}(a\times(b\times c),(a'\times b')\times c'):=\cat{A}(a,a')\otimes\cat{B}(b,b')\otimes\cat{C}(c,c')\\). \begin{align}\alpha\_{\cat{A},\cat{B},\cat{C}}^{-1}\circ\alpha\_{\cat{A},\cat{B},\cat{C}}((a\times b)\times c,(a''\times b'')\times c'')=&\bigvee_{a'''\in\cat{A},b'''\in\cat{B},c'''\in\cat{C}}\cat{A}(a,a''')\otimes\cat{B}(b,b''')\otimes\cat{C}(c,c''')\otimes\cat{A}(a''',a'')\otimes\cat{B}(b''',b'')\otimes\cat{C}(c''',c'')\\\\=&\bigvee_{a'''\in\cat{A},b'''\in\cat{B},c'''\in\cat{C}}\cat{A}(a,a''')\otimes\cat{A}(a''',a'')\otimes\cat{B}(b,b''')\otimes\cat{B}(b''',b'')\otimes\cat{C}(c,c''')\otimes\cat{C}(c''',c'')\\\\=&\cat{A}(a,a'')\otimes\cat{B}(b,b'')\otimes\cat{C}(c,c'')\\\\=&(\cat{A}\times\cat{B})(a\times b,a''\times b'')\otimes\cat{C}(c,c'')\\\\=&U\_{(\cat{A}\times\cat{B})\times\cat{C}}((a\times b)\times c,(a''\times b'')\times c'')\end{align}, and \begin{align}\alpha\_{\cat{A},\cat{B},\cat{C}}\circ\alpha\_{\cat{A},\cat{B},\cat{C}}^{-1}(a\times(b\times c),a''\times(b''\times c''))=&\bigvee_{a'''\in\cat{A},b'''\in\cat{B},c'''\in\cat{C}}\cat{A}(a,a''')\otimes\cat{B}(b,b''')\otimes\cat{C}(c,c''')\otimes\cat{A}(a''',a'')\otimes\cat{B}(b''',b'')\otimes\cat{C}(c''',c'')\\\\=&\bigvee_{a'''\in\cat{A},b'''\in\cat{B},c'''\in\cat{C}}\cat{A}(a,a''')\otimes\cat{A}(a''',a'')\otimes\cat{B}(b,b''')\otimes\cat{B}(b''',b'')\otimes\cat{C}(c,c''')\otimes\cat{C}(c''',c'')\\\\=&\cat{A}(a,a'')\otimes\cat{B}(b,b'')\otimes\cat{C}(c,c'')\\\\=&\cat{A}(a,a'')\otimes(\cat{B}\times\cat{C})(b\times c,b\times c'')\\\\=&U\_{\cat{A}\times(\cat{B}\times\cat{C})}(a\times(b\times c),a''\times(b''\times c''))\end{align}. So, these profunctors are mutually isomorphic.
  • 2.

    Note that since \(\newcommand{\op}[]{^\mathrm{op}}\cat{X}\op\neq\cat{X}\), both snake equations must be checked.

    The first: \begin{align}\lambda_\cat{X}\circ(\epsilon_\cat{X}\times U_\cat{X})\circ\alpha_{\cat{X,X\op,X}}^{-1}\circ(U_\cat{X}\times\eta_\cat{X})\circ\rho_\cat{X}^{-1}(x,y)=&\bigvee_{(z_1,1)\in\cat{X}\times\textbf{1}}\rho_\cat{X}^{-1}(x,(z_1,1))\otimes\lambda_\cat{X}\circ(\epsilon_\cat{X}\times U_\cat{X})\circ\alpha_{\cat{X,X\op,X}}^{-1}\circ(U_\cat{X}\times\eta_\cat{X})((z_1,1),y)\\=&\bigvee_{(z_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z_1)\otimes\lambda_\cat{X}\circ(\epsilon_\cat{X}\times U_\cat{X})\circ\alpha_{\cat{X,X\op,X}}^{-1}\circ(U_\cat{X}\times\eta_\cat{X})((z_1,1),y)\\=&\bigvee_{(z_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z_1)\otimes\bigvee_{z_2\times(z_3\times z_4)\in\cat{X}\times(\cat{X}\op\times\cat{X})}(U_\cat{X}\times\eta_\cat{X})((z_1,1),z_2\times(z_3\times z_4))\otimes\lambda_\cat{X}\circ(\epsilon_\cat{X}\times U_\cat{X})\circ\alpha_{\cat{X,X\op,X}}^{-1}(z_2\times(z_3\times z_4),y)\\=&\bigvee_{(z_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z_1)\otimes\bigvee_{z_2\times(z_3\times z_4)\in\cat{X}\times(\cat{X}\op\times\cat{X})}U_\cat{X}(z_1,z_2)\otimes\eta_\cat{X}(1,z_3,z_4)\otimes\lambda_\cat{X}\circ(\epsilon_\cat{X}\times U_\cat{X})\circ\alpha_{\cat{X,X\op,X}}^{-1}(z_2\times(z_3\times z_4),y)\\=&\bigvee_{(z_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z_1)\otimes\bigvee_{z_2\times(z_3\times z_4)\in\cat{X}\times(\cat{X}\op\times\cat{X})}\cat{X}(z_1,z_2)\otimes\cat{X}(z_3,z_4)\otimes\lambda_\cat{X}\circ(\epsilon_\cat{X}\times U_\cat{X})\circ\alpha_{\cat{X,X\op,X}}^{-1}(z_2\times(z_3\times z_4),y)\\=&\bigvee_{(z_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z_1)\otimes\bigvee_{z_2\times(z_3\times z_4)\in\cat{X}\times(\cat{X}\op\times\cat{X})}\cat{X}(z_1,z_2)\otimes\cat{X}(z_3,z_4)\otimes\bigvee_{(z_5\times z_6)\times z_7\in(\cat{X}\times\cat{X}\op)\times\cat{X}}\alpha_{\cat{X,X\op,X}}^{-1}(z_2\times(z_3\times z_4),(z_5\times z_6)\times z_7)\otimes\lambda_\cat{X}\circ(\epsilon_\cat{X}\times U_\cat{X})((z_5\times z_6)\times z_7,y)\\=&\bigvee_{(z_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z_1)\otimes\bigvee_{z_2\times(z_3\times z_4)\in\cat{X}\times(\cat{X}\op\times\cat{X})}\cat{X}(z_1,z_2)\otimes\cat{X}(z_3,z_4)\otimes\bigvee_{(z_5\times z_6)\times z_7\in(\cat{X}\times\cat{X}\op)\times\cat{X}}\cat{X}(z_2,z_5)\otimes\cat{X}\op(z_3,z_6)\otimes\cat{X}(z_4,z_7)\otimes\lambda_\cat{X}\circ(\epsilon_\cat{X}\times U_\cat{X})((z_5\times z_6)\times z_7,y)\\=&\bigvee_{(z_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z_1)\otimes\bigvee_{z_2\times(z_3\times z_4)\in\cat{X}\times(\cat{X}\op\times\cat{X})}\cat{X}(z_1,z_2)\otimes\cat{X}(z_3,z_4)\otimes\bigvee_{(z_5\times z_6)\times z_7\in(\cat{X}\times\cat{X}\op)\times\cat{X}}\cat{X}(z_2,z_5)\otimes\cat{X}\op(z_3,z_6)\otimes\cat{X}(z_4,z_7)\otimes\bigvee_{(1,z_8)\in\textbf{1}\times\cat{X}}(\epsilon_\cat{X}\times U_\cat{X})((z_5\times z_6)\times z_7,(1,z_8))\lambda_\cat{X}((1,z_8),y)\\=&\bigvee_{(z_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z_1)\otimes\bigvee_{z_2\times(z_3\times z_4)\in\cat{X}\times(\cat{X}\op\times\cat{X})}\cat{X}(z_1,z_2)\otimes\cat{X}(z_3,z_4)\otimes\bigvee_{(z_5\times z_6)\times z_7\in(\cat{X}\times\cat{X}\op)\times\cat{X}}\cat{X}(z_2,z_5)\otimes\cat{X}\op(z_3,z_6)\otimes\cat{X}(z_4,z_7)\otimes\bigvee_{(1,z_8)\in\textbf{1}\times\cat{X}}\epsilon_\cat{X}(z_5,z_6,1)\otimes U_\cat{X}(z_7,z_8)\otimes\lambda_\cat{X}((1,z_8),y)\\=&\bigvee_{(z_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z_1)\otimes\bigvee_{z_2\times(z_3\times z_4)\in\cat{X}\times(\cat{X}\op\times\cat{X})}\cat{X}(z_1,z_2)\otimes\cat{X}(z_3,z_4)\otimes\bigvee_{(z_5\times z_6)\times z_7\in(\cat{X}\times\cat{X}\op)\times\cat{X}}\cat{X}(z_2,z_5)\otimes\cat{X}\op(z_3,z_6)\otimes\cat{X}(z_4,z_7)\otimes\bigvee_{(1,z_8)\in\textbf{1}\times\cat{X}}\cat{X}(z_5,z_6)\otimes\cat{X}(z_7,z_8)\otimes\cat{X}(z_8,y)\\=&\bigvee_{z_1,\ldots{},z_8\in\cat{X}}\cat{X}(x,z_1)\otimes\cat{X}(z_1,z_2)\otimes\cat{X}(z_3,z_4)\otimes\cat{X}(z_2,z_5)\otimes\cat{X}\op(z_3,z_6)\otimes\cat{X}(z_4,z_7)\otimes\cat{X}(z_5,z_6)\otimes\cat{X}(z_7,z_8)\otimes\cat{X}(z_8,y)\\=&\bigvee_{z_1,\ldots{},z_8\in\cat{X}}\cat{X}(x,z_1)\otimes\cat{X}(z_1,z_2)\otimes\cat{X}(z_2,z_5)\otimes\cat{X}(z_5,z_6)\otimes\cat{X}\op(z_3,z_6)\otimes\cat{X}(z_3,z_4)\otimes\cat{X}(z_4,z_7)\otimes\cat{X}(z_7,z_8)\otimes\cat{X}(z_8,y)\\=&\bigvee_{z_3,z_6\in\cat{X}}\cat{X}(x,z_6)\otimes\cat{X}\op(z_3,z_6)\otimes\cat{X}(z_3,y)\\=&\bigvee_{z_3,z_6\in\cat{X}}\cat{X}(x,z_6)\otimes\cat{X}(z_6,z_3)\otimes\cat{X}(z_3,y)\\=&\cat{X}(x,y)\\=&U_\cat{X}(x,y)\end{align}. So, the first snake equation holds.

    Comment Source:Note that since \\(\newcommand{\op}[]{^\mathrm{op}}\cat{X}\op\neq\cat{X}\\), both snake equations must be checked. The first: \begin{align}\lambda\_\cat{X}\circ(\epsilon\_\cat{X}\times U\_\cat{X})\circ\alpha\_{\cat{X,X\op,X}}^{-1}\circ(U\_\cat{X}\times\eta\_\cat{X})\circ\rho\_\cat{X}^{-1}(x,y)=&\bigvee\_{(z\_1,1)\in\cat{X}\times\textbf{1}}\rho\_\cat{X}^{-1}(x,(z\_1,1))\otimes\lambda\_\cat{X}\circ(\epsilon\_\cat{X}\times U\_\cat{X})\circ\alpha\_{\cat{X,X\op,X}}^{-1}\circ(U\_\cat{X}\times\eta\_\cat{X})((z\_1,1),y)\\\\=&\bigvee\_{(z\_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z\_1)\otimes\lambda\_\cat{X}\circ(\epsilon\_\cat{X}\times U\_\cat{X})\circ\alpha\_{\cat{X,X\op,X}}^{-1}\circ(U\_\cat{X}\times\eta\_\cat{X})((z\_1,1),y)\\\\=&\bigvee\_{(z\_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z\_1)\otimes\bigvee\_{z\_2\times(z\_3\times z\_4)\in\cat{X}\times(\cat{X}\op\times\cat{X})}(U\_\cat{X}\times\eta\_\cat{X})((z\_1,1),z\_2\times(z\_3\times z\_4))\otimes\lambda\_\cat{X}\circ(\epsilon\_\cat{X}\times U\_\cat{X})\circ\alpha\_{\cat{X,X\op,X}}^{-1}(z\_2\times(z\_3\times z\_4),y)\\\\=&\bigvee\_{(z\_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z\_1)\otimes\bigvee\_{z\_2\times(z\_3\times z\_4)\in\cat{X}\times(\cat{X}\op\times\cat{X})}U\_\cat{X}(z\_1,z\_2)\otimes\eta\_\cat{X}(1,z\_3,z\_4)\otimes\lambda\_\cat{X}\circ(\epsilon\_\cat{X}\times U\_\cat{X})\circ\alpha\_{\cat{X,X\op,X}}^{-1}(z\_2\times(z\_3\times z\_4),y)\\\\=&\bigvee\_{(z\_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z\_1)\otimes\bigvee\_{z\_2\times(z\_3\times z\_4)\in\cat{X}\times(\cat{X}\op\times\cat{X})}\cat{X}(z\_1,z\_2)\otimes\cat{X}(z\_3,z\_4)\otimes\lambda\_\cat{X}\circ(\epsilon\_\cat{X}\times U\_\cat{X})\circ\alpha\_{\cat{X,X\op,X}}^{-1}(z\_2\times(z\_3\times z\_4),y)\\\\=&\bigvee\_{(z\_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z\_1)\otimes\bigvee\_{z\_2\times(z\_3\times z\_4)\in\cat{X}\times(\cat{X}\op\times\cat{X})}\cat{X}(z\_1,z\_2)\otimes\cat{X}(z\_3,z\_4)\otimes\bigvee\_{(z\_5\times z\_6)\times z\_7\in(\cat{X}\times\cat{X}\op)\times\cat{X}}\alpha\_{\cat{X,X\op,X}}^{-1}(z\_2\times(z\_3\times z\_4),(z\_5\times z\_6)\times z\_7)\otimes\lambda\_\cat{X}\circ(\epsilon\_\cat{X}\times U\_\cat{X})((z\_5\times z\_6)\times z\_7,y)\\\\=&\bigvee\_{(z\_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z\_1)\otimes\bigvee\_{z\_2\times(z\_3\times z\_4)\in\cat{X}\times(\cat{X}\op\times\cat{X})}\cat{X}(z\_1,z\_2)\otimes\cat{X}(z\_3,z\_4)\otimes\bigvee\_{(z\_5\times z\_6)\times z\_7\in(\cat{X}\times\cat{X}\op)\times\cat{X}}\cat{X}(z\_2,z\_5)\otimes\cat{X}\op(z\_3,z\_6)\otimes\cat{X}(z\_4,z\_7)\otimes\lambda\_\cat{X}\circ(\epsilon\_\cat{X}\times U\_\cat{X})((z\_5\times z\_6)\times z\_7,y)\\\\=&\bigvee\_{(z\_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z\_1)\otimes\bigvee\_{z\_2\times(z\_3\times z\_4)\in\cat{X}\times(\cat{X}\op\times\cat{X})}\cat{X}(z\_1,z\_2)\otimes\cat{X}(z\_3,z\_4)\otimes\bigvee\_{(z\_5\times z\_6)\times z\_7\in(\cat{X}\times\cat{X}\op)\times\cat{X}}\cat{X}(z\_2,z\_5)\otimes\cat{X}\op(z\_3,z\_6)\otimes\cat{X}(z\_4,z\_7)\otimes\bigvee\_{(1,z\_8)\in\textbf{1}\times\cat{X}}(\epsilon\_\cat{X}\times U\_\cat{X})((z\_5\times z\_6)\times z\_7,(1,z\_8))\lambda\_\cat{X}((1,z\_8),y)\\\\=&\bigvee\_{(z\_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z\_1)\otimes\bigvee\_{z\_2\times(z\_3\times z\_4)\in\cat{X}\times(\cat{X}\op\times\cat{X})}\cat{X}(z\_1,z\_2)\otimes\cat{X}(z\_3,z\_4)\otimes\bigvee\_{(z\_5\times z\_6)\times z\_7\in(\cat{X}\times\cat{X}\op)\times\cat{X}}\cat{X}(z\_2,z\_5)\otimes\cat{X}\op(z\_3,z\_6)\otimes\cat{X}(z\_4,z\_7)\otimes\bigvee\_{(1,z\_8)\in\textbf{1}\times\cat{X}}\epsilon\_\cat{X}(z\_5,z\_6,1)\otimes U\_\cat{X}(z\_7,z\_8)\otimes\lambda\_\cat{X}((1,z\_8),y)\\\\=&\bigvee\_{(z\_1,1)\in\cat{X}\times\textbf{1}}\cat{X}(x,z\_1)\otimes\bigvee\_{z\_2\times(z\_3\times z\_4)\in\cat{X}\times(\cat{X}\op\times\cat{X})}\cat{X}(z\_1,z\_2)\otimes\cat{X}(z\_3,z\_4)\otimes\bigvee\_{(z\_5\times z\_6)\times z\_7\in(\cat{X}\times\cat{X}\op)\times\cat{X}}\cat{X}(z\_2,z\_5)\otimes\cat{X}\op(z\_3,z\_6)\otimes\cat{X}(z\_4,z\_7)\otimes\bigvee\_{(1,z\_8)\in\textbf{1}\times\cat{X}}\cat{X}(z\_5,z\_6)\otimes\cat{X}(z\_7,z\_8)\otimes\cat{X}(z\_8,y)\\\\=&\bigvee\_{z\_1,\ldots{},z\_8\in\cat{X}}\cat{X}(x,z\_1)\otimes\cat{X}(z\_1,z\_2)\otimes\cat{X}(z\_3,z\_4)\otimes\cat{X}(z\_2,z\_5)\otimes\cat{X}\op(z\_3,z\_6)\otimes\cat{X}(z\_4,z\_7)\otimes\cat{X}(z\_5,z\_6)\otimes\cat{X}(z\_7,z\_8)\otimes\cat{X}(z\_8,y)\\\\=&\bigvee\_{z\_1,\ldots{},z\_8\in\cat{X}}\cat{X}(x,z\_1)\otimes\cat{X}(z\_1,z\_2)\otimes\cat{X}(z\_2,z\_5)\otimes\cat{X}(z\_5,z\_6)\otimes\cat{X}\op(z\_3,z\_6)\otimes\cat{X}(z\_3,z\_4)\otimes\cat{X}(z\_4,z\_7)\otimes\cat{X}(z\_7,z\_8)\otimes\cat{X}(z\_8,y)\\\\=&\bigvee\_{z\_3,z\_6\in\cat{X}}\cat{X}(x,z\_6)\otimes\cat{X}\op(z\_3,z\_6)\otimes\cat{X}(z\_3,y)\\\\=&\bigvee\_{z\_3,z\_6\in\cat{X}}\cat{X}(x,z\_6)\otimes\cat{X}(z\_6,z\_3)\otimes\cat{X}(z\_3,y)\\\\=&\cat{X}(x,y)\\\\=&U\_\cat{X}(x,y)\end{align}. So, the first snake equation holds.
  • 3.
    edited September 22

    Now for the second snake equation (following the above calculation and making the necessary changes): \begin{align}\rho_{\cat{X}\op}\circ(U_{\cat{X}\op}\times\epsilon_\cat{X})\circ\alpha_{\cat{X\op,X,X\op}}\circ(\eta_\cat{X}\times U_{\cat{X}\op})\circ\lambda_{\cat{X}\op}^{-1}(x,y)=&\bigvee_{(1,z_1)\in\textbf{1}\times\cat{X}\op}\lambda_{\cat{X}\op}^{-1}(x,(1,z_1))\otimes\rho_{\cat{X}\op}\circ(U_{\cat{X}\op}\times\epsilon_\cat{X})\circ\alpha_{\cat{X\op,X,X\op}}\circ(\eta_\cat{X}\times U_{\cat{X}\op})((1,z_1),y)\\=&\bigvee_{(1,z_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z_1)\otimes\rho_{\cat{X}\op}\circ(U_{\cat{X}\op}\times\epsilon_\cat{X})\circ\alpha_{\cat{X\op,X,X\op}}\circ(\eta_\cat{X}\times U_{\cat{X}\op})((1,z_1),y)\\=&\bigvee_{(1,z_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z_1)\otimes\bigvee_{(z_2\times z_3)\times z_4\in(\cat{X}\op\times\cat{X})\times\cat{X}\op)}(\eta_\cat{X}\times U_{\cat{X}\op})((1,z_1),(z_2\times z_3)\times z_4)\otimes\rho_{\cat{X}\op}\circ(U_{\cat{X}\op}\times\epsilon_\cat{X})\circ\alpha_{\cat{X\op,X,X\op}}((z_2\times z_3)\times z_4,y)\\=&\bigvee_{(1,z_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z_1)\otimes\bigvee_{(z_2\times z_3)\times z_4\in(\cat{X}\op\times\cat{X})\times\cat{X}\op}\eta_\cat{X}(1,z_2,z_3)\otimes U_{\cat{X}\op}(z_1,z_4)\otimes\rho_{\cat{X}\op}\circ(U_{\cat{X}\op}\times\epsilon_\cat{X})\circ\alpha_{\cat{X\op,X,X\op}}((z_2\times z_3)\times z_4,y)\\=&\bigvee_{(1,z_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z_1)\otimes\bigvee_{(z_2\times z_3)\times z_4\in(\cat{X}\op\times\cat{X})\times\cat{X}\op}\cat{X}(z_2,z_3)\otimes\cat{X}\op(z_1,z_4)\otimes\rho_{\cat{X}\op}\circ(U_{\cat{X}\op}\times\epsilon_\cat{X})\circ\alpha_{\cat{X\op,X,X\op}}((z_2\times z_3)\times z_4,y)\\=&\bigvee_{(1,z_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z_1)\otimes\bigvee_{(z_2\times z_3)\times z_4\in(\cat{X}\op\times\cat{X})\times\cat{X}\op}\cat{X}(z_2,z_3)\otimes\cat{X}\op(z_1,z_4)\otimes\bigvee_{z_5\times(z_6\times z_7)\in\cat{X}\op\times(\cat{X}\times\cat{X}\op)}\alpha_{\cat{X\op,X,X\op}}((z_2\times z_3)\times z_4,z_5\times(z_6\times z_7))\otimes\rho_{\cat{X}\op}\circ(U_{\cat{X}\op}\times\epsilon_\cat{X})(z_5\times(z_6\times z_7),y)\\=&\bigvee_{(1,z_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z_1)\otimes\bigvee_{(z_2\times z_3)\times z_4\in(\cat{X}\op\times\cat{X})\times\cat{X}\op}\cat{X}(z_2,z_3)\otimes\cat{X}\op(z_1,z_4)\otimes\bigvee_{z_5\times(z_6\times z_7)\in\cat{X}\op\times(\cat{X}\times\cat{X}\op)}\cat{X}\op(z_2,z_5)\otimes\cat{X}(z_3,z_6)\otimes\cat{X}\op(z_4,z_7)\otimes\rho_{\cat{X}\op}\circ(U_{\cat{X}\op}\times\epsilon_\cat{X})(z_5\times(z_6\times z_7),y)\\=&\bigvee_{(1,z_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z_1)\otimes\bigvee_{(z_2\times z_3)\times z_4\in(\cat{X}\op\times\cat{X})\times\cat{X}\op}\cat{X}(z_2,z_3)\otimes\cat{X}\op(z_1,z_4)\otimes\bigvee_{z_5\times(z_6\times z_7)\in\cat{X}\op\times(\cat{X}\times\cat{X}\op)}\cat{X}\op(z_2,z_5)\otimes\cat{X}(z_3,z_6)\otimes\cat{X}\op(z_4,z_7)\otimes\bigvee_{(z_8,1)\in\cat{X}\op\times\textbf{1}}(U_{\cat{X}\op}\times\epsilon_\cat{X})(z_5\times(z_6\times z_7),(z_8,1))\otimes\rho_{\cat{X}\op}((z_8,1),y)\\=&\bigvee_{(1,z_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z_1)\otimes\bigvee_{(z_2\times z_3)\times z_4\in(\cat{X}\op\times\cat{X})\times\cat{X}\op}\cat{X}(z_2,z_3)\otimes\cat{X}\op(z_1,z_4)\otimes\bigvee_{z_5\times(z_6\times z_7)\in\cat{X}\op\times(\cat{X}\times\cat{X}\op)}\cat{X}\op(z_2,z_5)\otimes\cat{X}(z_3,z_6)\otimes\cat{X}\op(z_4,z_7)\otimes\bigvee_{(z_8,1)\in\cat{X}\op\times\textbf{1}}U_{\cat{X}\op}(z_5,z_8)\otimes\epsilon_\cat{X}(z_6,z_7,1)\otimes\rho_{\cat{X}\op}((z_8,1),y)\\=&\bigvee_{(1,z_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z_1)\otimes\bigvee_{(z_2\times z_3)\times z_4\in(\cat{X}\op\times\cat{X})\times\cat{X}\op}\cat{X}(z_2,z_3)\otimes\cat{X}\op(z_1,z_4)\otimes\bigvee_{z_5\times(z_6\times z_7)\in\cat{X}\op\times(\cat{X}\times\cat{X}\op)}\cat{X}\op(z_2,z_5)\otimes\cat{X}(z_3,z_6)\otimes\cat{X}\op(z_4,z_7)\otimes\bigvee_{(z_8,1)\in\cat{X}\op\times\textbf{1}}\cat{X}\op(z_5,z_8)\otimes\cat{X}(z_6,z_7)\otimes\cat{X}\op(z_8,y)\\=&\bigvee_{z_1,\ldots{},z_8\in\cat{X}}\cat{X}\op(x,z_1)\otimes\cat{X}(z_2,z_3)\otimes\cat{X}\op(z_1,z_4)\otimes\cat{X}\op(z_2,z_5)\otimes\cat{X}(z_3,z_6)\otimes\cat{X}\op(z_4,z_7)\otimes\cat{X}\op(z_5,z_8)\otimes\cat{X}(z_6,z_7)\otimes\cat{X}\op(z_8,y)\\=&\bigvee_{z_1,\ldots{},z_8\in\cat{X}}\cat{X}\op(x,z_1)\otimes\cat{X}\op(z_1,z_4)\otimes\cat{X}\op(z_4,z_7)\otimes\cat{X}(z_2,z_3)\otimes\cat{X}(z_3,z_6)\otimes\cat{X}(z_6,z_7)\otimes\cat{X}\op(z_2,z_5)\otimes\cat{X}\op(z_5,z_8)\otimes\cat{X}\op(z_8,y)\\=&\bigvee_{z_2,z_7\in\cat{X}}\cat{X}\op(x,z_7)\otimes\cat{X}(z_2,z_7)\otimes\cat{X}\op(z_2,y)\\=&\bigvee_{z_2,z_7\in\cat{X}}\cat{X}\op(x,z_7)\otimes\cat{X}\op(z_7,z_2)\otimes\cat{X}\op(z_2,y)\\=&\cat{X}\op(x,y)\\=&U_{\cat{X}\op}(x,y)\end{align}. So, the second snake equation holds.

    Comment Source:Now for the second snake equation (following the above calculation and making the necessary changes): \begin{align}\rho\_{\cat{X}\op}\circ(U\_{\cat{X}\op}\times\epsilon\_\cat{X})\circ\alpha\_{\cat{X\op,X,X\op}}\circ(\eta\_\cat{X}\times U\_{\cat{X}\op})\circ\lambda\_{\cat{X}\op}^{-1}(x,y)=&\bigvee\_{(1,z\_1)\in\textbf{1}\times\cat{X}\op}\lambda\_{\cat{X}\op}^{-1}(x,(1,z\_1))\otimes\rho\_{\cat{X}\op}\circ(U\_{\cat{X}\op}\times\epsilon\_\cat{X})\circ\alpha\_{\cat{X\op,X,X\op}}\circ(\eta\_\cat{X}\times U\_{\cat{X}\op})((1,z\_1),y)\\\\=&\bigvee\_{(1,z\_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z\_1)\otimes\rho\_{\cat{X}\op}\circ(U\_{\cat{X}\op}\times\epsilon\_\cat{X})\circ\alpha\_{\cat{X\op,X,X\op}}\circ(\eta\_\cat{X}\times U\_{\cat{X}\op})((1,z\_1),y)\\\\=&\bigvee\_{(1,z\_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z\_1)\otimes\bigvee\_{(z\_2\times z\_3)\times z\_4\in(\cat{X}\op\times\cat{X})\times\cat{X}\op)}(\eta\_\cat{X}\times U\_{\cat{X}\op})((1,z\_1),(z\_2\times z\_3)\times z\_4)\otimes\rho\_{\cat{X}\op}\circ(U\_{\cat{X}\op}\times\epsilon\_\cat{X})\circ\alpha\_{\cat{X\op,X,X\op}}((z\_2\times z\_3)\times z\_4,y)\\\\=&\bigvee\_{(1,z\_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z\_1)\otimes\bigvee\_{(z\_2\times z\_3)\times z\_4\in(\cat{X}\op\times\cat{X})\times\cat{X}\op}\eta\_\cat{X}(1,z\_2,z\_3)\otimes U\_{\cat{X}\op}(z\_1,z\_4)\otimes\rho\_{\cat{X}\op}\circ(U\_{\cat{X}\op}\times\epsilon\_\cat{X})\circ\alpha\_{\cat{X\op,X,X\op}}((z\_2\times z\_3)\times z\_4,y)\\\\=&\bigvee\_{(1,z\_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z\_1)\otimes\bigvee\_{(z\_2\times z\_3)\times z\_4\in(\cat{X}\op\times\cat{X})\times\cat{X}\op}\cat{X}(z\_2,z\_3)\otimes\cat{X}\op(z\_1,z\_4)\otimes\rho\_{\cat{X}\op}\circ(U\_{\cat{X}\op}\times\epsilon\_\cat{X})\circ\alpha\_{\cat{X\op,X,X\op}}((z\_2\times z\_3)\times z\_4,y)\\\\=&\bigvee\_{(1,z\_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z\_1)\otimes\bigvee\_{(z\_2\times z\_3)\times z\_4\in(\cat{X}\op\times\cat{X})\times\cat{X}\op}\cat{X}(z\_2,z\_3)\otimes\cat{X}\op(z\_1,z\_4)\otimes\bigvee\_{z\_5\times(z\_6\times z\_7)\in\cat{X}\op\times(\cat{X}\times\cat{X}\op)}\alpha\_{\cat{X\op,X,X\op}}((z\_2\times z\_3)\times z\_4,z\_5\times(z\_6\times z\_7))\otimes\rho\_{\cat{X}\op}\circ(U\_{\cat{X}\op}\times\epsilon\_\cat{X})(z\_5\times(z\_6\times z\_7),y)\\\\=&\bigvee\_{(1,z\_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z\_1)\otimes\bigvee\_{(z\_2\times z\_3)\times z\_4\in(\cat{X}\op\times\cat{X})\times\cat{X}\op}\cat{X}(z\_2,z\_3)\otimes\cat{X}\op(z\_1,z\_4)\otimes\bigvee\_{z\_5\times(z\_6\times z\_7)\in\cat{X}\op\times(\cat{X}\times\cat{X}\op)}\cat{X}\op(z\_2,z\_5)\otimes\cat{X}(z\_3,z\_6)\otimes\cat{X}\op(z\_4,z\_7)\otimes\rho\_{\cat{X}\op}\circ(U\_{\cat{X}\op}\times\epsilon\_\cat{X})(z\_5\times(z\_6\times z\_7),y)\\\\=&\bigvee\_{(1,z\_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z\_1)\otimes\bigvee\_{(z\_2\times z\_3)\times z\_4\in(\cat{X}\op\times\cat{X})\times\cat{X}\op}\cat{X}(z\_2,z\_3)\otimes\cat{X}\op(z\_1,z\_4)\otimes\bigvee\_{z\_5\times(z\_6\times z\_7)\in\cat{X}\op\times(\cat{X}\times\cat{X}\op)}\cat{X}\op(z\_2,z\_5)\otimes\cat{X}(z\_3,z\_6)\otimes\cat{X}\op(z\_4,z\_7)\otimes\bigvee\_{(z\_8,1)\in\cat{X}\op\times\textbf{1}}(U\_{\cat{X}\op}\times\epsilon\_\cat{X})(z\_5\times(z\_6\times z\_7),(z\_8,1))\otimes\rho\_{\cat{X}\op}((z\_8,1),y)\\\\=&\bigvee\_{(1,z\_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z\_1)\otimes\bigvee\_{(z\_2\times z\_3)\times z\_4\in(\cat{X}\op\times\cat{X})\times\cat{X}\op}\cat{X}(z\_2,z\_3)\otimes\cat{X}\op(z\_1,z\_4)\otimes\bigvee\_{z\_5\times(z\_6\times z\_7)\in\cat{X}\op\times(\cat{X}\times\cat{X}\op)}\cat{X}\op(z\_2,z\_5)\otimes\cat{X}(z\_3,z\_6)\otimes\cat{X}\op(z\_4,z\_7)\otimes\bigvee\_{(z\_8,1)\in\cat{X}\op\times\textbf{1}}U\_{\cat{X}\op}(z\_5,z\_8)\otimes\epsilon\_\cat{X}(z\_6,z\_7,1)\otimes\rho\_{\cat{X}\op}((z\_8,1),y)\\\\=&\bigvee\_{(1,z\_1)\in\textbf{1}\times\cat{X}\op}\cat{X}\op(x,z\_1)\otimes\bigvee\_{(z\_2\times z\_3)\times z\_4\in(\cat{X}\op\times\cat{X})\times\cat{X}\op}\cat{X}(z\_2,z\_3)\otimes\cat{X}\op(z\_1,z\_4)\otimes\bigvee\_{z\_5\times(z\_6\times z\_7)\in\cat{X}\op\times(\cat{X}\times\cat{X}\op)}\cat{X}\op(z\_2,z\_5)\otimes\cat{X}(z\_3,z\_6)\otimes\cat{X}\op(z\_4,z\_7)\otimes\bigvee\_{(z\_8,1)\in\cat{X}\op\times\textbf{1}}\cat{X}\op(z\_5,z\_8)\otimes\cat{X}(z\_6,z\_7)\otimes\cat{X}\op(z\_8,y)\\\\=&\bigvee\_{z\_1,\ldots{},z\_8\in\cat{X}}\cat{X}\op(x,z\_1)\otimes\cat{X}(z\_2,z\_3)\otimes\cat{X}\op(z\_1,z\_4)\otimes\cat{X}\op(z\_2,z\_5)\otimes\cat{X}(z\_3,z\_6)\otimes\cat{X}\op(z\_4,z\_7)\otimes\cat{X}\op(z\_5,z\_8)\otimes\cat{X}(z\_6,z\_7)\otimes\cat{X}\op(z\_8,y)\\\\=&\bigvee\_{z\_1,\ldots{},z\_8\in\cat{X}}\cat{X}\op(x,z\_1)\otimes\cat{X}\op(z\_1,z\_4)\otimes\cat{X}\op(z\_4,z\_7)\otimes\cat{X}(z\_2,z\_3)\otimes\cat{X}(z\_3,z\_6)\otimes\cat{X}(z\_6,z\_7)\otimes\cat{X}\op(z\_2,z\_5)\otimes\cat{X}\op(z\_5,z\_8)\otimes\cat{X}\op(z\_8,y)\\\\=&\bigvee\_{z\_2,z\_7\in\cat{X}}\cat{X}\op(x,z\_7)\otimes\cat{X}(z\_2,z\_7)\otimes\cat{X}\op(z\_2,y)\\\\=&\bigvee\_{z\_2,z\_7\in\cat{X}}\cat{X}\op(x,z\_7)\otimes\cat{X}\op(z\_7,z\_2)\otimes\cat{X}\op(z\_2,y)\\\\=&\cat{X}\op(x,y)\\\\=&U\_{\cat{X}\op}(x,y)\end{align}. So, the second snake equation holds.
Sign In or Register to comment.