逆演算について

足し算と引き算のような関係は積コモナドにより定式化ができます。整数Z上の足し算+と引き算-を考えます。

\[ (+) : \mathbb{Z} × \mathbb{Z}→ \mathbb{Z} \\ (-) : \mathbb{Z} × \mathbb{Z}→ \mathbb{Z}\]
積コモナド(_×Z)を考えます。余単位元εと余拡張^†は次のようになります。
・余単位元ε
任意の集合Xに対してε_X : X × Z → X は
\[ ε_X : X × \mathbb{Z} → X \\ ε_X(x, n) = x \]
これは射影に相当します。

・余拡張^†
任意の関数f : X → Y × Z に対してf^† : X × Z → Y × Z は
\[ f^† : X × \mathbb{Z} → Y × \mathbb{Z} \\ f^† (x, n) = (f(x, n), n) \]

足し算+と引き算-は次のように合成すると余単位元になるという関係にあります。
これは、積コモナドが与える余クライスリ圏上で合成すると恒等射になるという関係を表します。
\[ (+) \circ (-)^† = ε_\mathbb{Z} = (-) \circ (+)^†\]

各式に２つの整数の組(m, n)を与えると次のようになります。
\[ (m - n) + n = m = (m + n) - n\]

確認しましょう。

・左辺
\[\begin{eqnarray*} (+) \circ (-)^† (m, n) &=& (+) ((-)^{†}(m, n)) \\&=& (+) ((-)(m, n), n) \\ &=& (+) (m - n, n) \\&=& (m - n) + n \end{eqnarray*} \]
・中辺
\[\begin{eqnarray*}ε_\mathbb{Z} (m, n) &=& m \end{eqnarray*} \]

・右辺
\[\begin{eqnarray*} (-) \circ (+)^† (m, n) &=& (-) ((+)^{†}(m, n)) \\&=& (-) ((+)(m, n), n) \\ &=& (-) (m + n, n) \\&=& (m + n) - n \end{eqnarray*} \]