--- a/proof_delta.tex	Fri Feb 13 11:31:46 2015 +0900
+++ b/proof_delta.tex	Fri Feb 13 11:48:40 2015 +0900
@@ -4,6 +4,50 @@
 第\ref{chapter:proof_delta}章では Agda を用いて Delta Monad が Monad であることを証明していく。
 証明のゴールは Delta Monad が Funcor 則と Monad 則を満たすことの証明である。
 
+% {{{ Agda における Delta Monad の表現
+
+\section{Agda における Delta Monad の表現}
+\label{section:delta_in_agda}
+\ref{section:delta_in_agda}節では Agda において Delta Monad を再定義する。
+Agda は Haskell において実装されているため、ほとんど同様に定義できる(リスト\ref{src:delta_in_agda})。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:delta_in_agda, caption=Agdaにおける Delta Monad のデータ定義] {src/delta.agda.replaced}
+\end{table}
+
+data型 Delta は型A の値と Nat を持つ。
+
+level とは型のlevelの区別に用いられるものである。
+Agda では型も値として扱えるため、同じ式において型と値が混同することがある。
+厳密に型と値を区別したい場合、level を定義することで区別する。
+levelは任意の level と、関数 suc により定義される。
+関数 suc は level を一つ上昇させる関数である。
+level l を適用した型を用いる時は Set l と記述する。
+今回は証明する対象のプログラムは Set l の level とし、それ以外は Set (suc l) の level とする。
+
+Nat は自然数であり、プログラムのバージョンに対応する。
+自然数の定義は\ref{section:reasoning} 節にあるリスト \ref{src:nat}にならうものとする。
+
+data 型 Delta は2つのコンストラクタにより構成される。
+
+\begin{itemize}
+    \item mono
+
+        プログラムの最初の変更単位を受けとり、バージョン1とする。
+        型Aを取り、バージョンが1のDeltaを構成することでその表現とする。
+
+    \item delta
+
+        変更単位と変更単位の列を受けとり、変更単位を追加する。
+        これは変更によるバージョンアップに相当する。
+        よって任意の1以上のバージョンを持つ Delta に変更単位を加えることでバージョンを1上昇させる。
+\end{itemize}
+
+Agda においてもデータ型 Delta が定義できた。
+これからこの定義を用いて Functor則と Monad 則を証明していく。
+
+% }}}
+
 % {{{ Agda における Functor 則
 
 \section{Agda における Functor 則}
@@ -20,13 +64,6 @@
 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 を返すようにする。