\chapter{Delta Monad が Monad である証明}
\label{chapter:proof_delta}
第\ref{chapter:agda}章では Agda における証明手法について述べた。
第\ref{chapter:proof_delta}章では Agda を用いて Delta Monad が Monad であることを証明していく。
証明のゴールは Delta Monad が Funcor 則と Monad 則を満たすことの証明である。

% {{{ Agda における Functor 則

\section{Agda における Functor 則}
\label{section:functor_in_agda}
Agda における Functor 則はリスト \ref{src:record_functor} のように記述した。

\begin{table}[html]
    \lstinputlisting[label=src:record_functor, caption=Agdaにおける Functor則の定義] {src/record_functor.agda.replaced}
\end{table}

Agda ではある性質を持つデータは record 構文によって記述する。
record の値は record の定義時に要請した field を全て満たすことで構築される。
よって、あるデータAが持つべき性質は field に定義し、A を用いた証明によって field を満たす。
field を満たすことにより record が構成できることで A がある性質を満たすことを証明する。

record Funcor は implicit な値 level と、型引数を持つ関数 F を持つ。
level とは型のlevelの区別に用いられるものである。
Agda では型も値として扱えるため、同じ式において型と値が混同することがある。
厳密に型と値を区別したい場合、level を定義することで区別する。
levelは任意の level と、関数 suc により定義される。
関数 suc は level を一つ上昇させる関数である。
level l を適用した型を用いる時は Set l と記述する。

record Functor が取る F は Set l を取り Set l を取る関数である。
Set l が証明の対象となるプログラムであるため、関数F はプログラムのlevel で表現する。
よって、プログラムの level l を取り、プログラムの level l の Set を返すようにする。
それに対し、 F に対する証明となる record Functor は、証明の対象とするプログラムそのものではない。
よって suc により level を一段上げる。
これは、証明の対象となるプログラムと証明そのものを混同しないためである。

record Functor の field には以下のようなものがある。

\begin{itemize}
    \item fmap

        Functor に要請される、category から category への map 関数である。
        型の定義はほとんど Haskell と同じである。
        fmap は任意の型に対して適用可能でなくてはいけないため、map する対象の型Aと map される対象の型Bは implicit である。

    \item preserve-id

        Functor則の id の保存である。
        型F A  を持つ値x に対するfmap id と id の等価性がなくてはならない。

    \item covariant

        Functor則における関数の合成の保存である。
        関数fとgを合成してから fmap により mapping しても、 f と g を個別に mapping してから合成しても等価性を持たなくてはならない。

    \item fmap-equiv

        ある型A の値x に対して等価である関数f と g を考えた時、 型F A の値 fx の対し、 fmap f としても fmap gとしても等価であることを保証する。
        これは本来はFunctor則には存在しない。
        Agda において Monad の証明に必要であったために追加した。
\end{itemize}

% }}}

\section{Delta が Functor 則を満たす証明}
\label{section:delta_is_functor}
\ref{section:functor_in_agda}節では Agda における Functor則の表現について述べた。
\ref{section:delta_is_functor}節では

\section{Agda における Monad 則}
\section{Delta が Monad 則を満たす証明}