--- a/agda.tex	Fri Feb 13 11:31:46 2015 +0900
+++ b/agda.tex	Fri Feb 13 11:48:40 2015 +0900
@@ -341,7 +341,7 @@
 例えば、直積型の定義はリスト\ref{src:product}のようなものがある。
 
 \begin{table}[html]
-    \lstinputlisting[label=src:product, caption=Agdaにおける直積型の例] {src/product.agda}
+    \lstinputlisting[label=src:product, caption=Agdaにおける直積型の例] {src/product.agda.replaced}
 \end{table}
 
 関数の定義時に \verb/_/ とした部分には項を入れることで関数が適用される。

--- 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 を返すようにする。

--- a/replace_agda.rb	Fri Feb 13 11:31:46 2015 +0900
+++ b/replace_agda.rb	Fri Feb 13 11:48:40 2015 +0900
@@ -1,10 +1,11 @@
 #!/usr/bin/env ruby
 
 replace_table = {
-  '∙' => 'circ',
-  '⟨' => 'langle',
-  '⟩' => 'rangle',
-  '∎' => 'blacksquare'
+  '∙'  => 'circ',
+  '×' => 'times',
+  '⟨'  => 'langle',
+  '⟩'  => 'rangle',
+  '∎'  => 'blacksquare'
 }
 footer = '.replaced'
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/delta.agda	Fri Feb 13 11:48:40 2015 +0900
@@ -0,0 +1,3 @@
+data Delta {l : Level} (A : Set l) : (Nat -> (Set l)) where
+  mono    : A -> Delta A (S O)
+  delta   : {n : Nat} -> A -> Delta A (S n) -> Delta A (S (S n))