\chapter{DeltaM が Monad 則を満たす証明}
\label{section:proof_deltaM}
DeltaM に対する Monad 則の証明も Agda によって行なう。

内部に持つ型 M は型引数を持ち、 Functor と Monad の制約を持つ。
ある法則を証明する時は内部の M の証明を使って証明することになる。
例えば DeltaM の$ \eta $ が natural transformation である証明には、 M の $ \eta $ が natural transformation である証明を用いる。

また、証明に辺り fmap-equiv という等式を定義している。
この等式は同じ値に対して同じ振舞いをする関数を fmap しても同じである等式である。

DeltaM に対する Monad 則の証明がリスト\ref{src:deltaM_is_monad}である。
プログラム内部のDeltaのバージョン数は全て同じであるとし、1以上とする。
なお、Functor則に対する証明も行なったが省略する。


\lstinputlisting[basicstyle={\scriptsize},
                 numberstyle={\tiny},
                 label=src:deltaM_is_monad,
                 caption= DeltaM が Monad 則を満たす証明]
                 {src/deltaM_is_monad.agda.replaced}