\chapter{DeltaM が Monad 則を満たす証明}
\label{section:proof_deltaM}
DeltaM に対する Monad 則の証明も Agda によって行なう。
プログラム内部のDeltaのバージョン数は全て同じであるとし、1以上とする。

内部に持つ型引数を持つ型M は Functor と Monad であるとする。
基本的に同じ法則を用いて証明していくことになる。
例えば $ \eta $ が natural transformation である証明には、 M の $ \eta $ が natural transformation である証明を用いる。
また、同じ値に対して同じ振舞いをする関数を fmap しても同じであるという fmap-equiv という等式を導入している。
これは高階関数に対する等式が定義できなかったためである。

DeltaM に対する Monad 則の証明がリスト\ref{src:deltaM_is_monad}である。
なお、Functor則に対する証明も行なったが省略する。


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