--- a/proof_delta.tex	Sun Feb 15 12:16:55 2015 +0900
+++ b/proof_delta.tex	Sun Feb 15 12:35:58 2015 +0900
@@ -3,6 +3,7 @@
 第\ref{chapter:agda}章では Agda における証明手法について述べた。
 第\ref{chapter:proof_delta}章では Agda を用いて Delta Monad が Monad であることを証明していく。
 証明のゴールは Delta Monad が Funcor 則と Monad 則を満たすことの証明である。
+なお、証明は全ての Delta が同じバージョンを持つという制約下において成り立った。
 
 % {{{ Agda における Delta Monad の表現
 
@@ -200,6 +201,8 @@
 
 % }}}
 
+% {{{ Delta が Monad 則を満たす証明
+
 \section{Delta が Monad 則を満たす証明}
 \label{section:delta_is_monad}
 \ref{section:monad_laws_in_agda}節において Agda における Monad則の定義を行なった。
@@ -302,6 +305,19 @@
 
         図\ref{fig:monad_laws}で示した左側の可換図に相当する。
 
+        $ \mu $ を用いて TTT から T にする際に、右側2つのTに対して先に $ \mu $ を用いるか、左側2つから先に用いるかの可換性である。
+        よって \verb/Delta (Delta (Delta A))/から \verb/Delta A/ とする演算の等式となる。
+
+        バージョンが1である場合はやはり同じ項に簡約される。
+        しかしバージョンが1以上である場合は複雑な式変形を行なう。
+
+        パターンマッチにより最も外側の Delta は分解されるため、バージョンが1下がる。
+        しかし内側の Delta 2つはバージョンが異なるため、外側2つの Delta のバージョンが異なってしまい $ \mu $ が適用できない。
+        よって \verb/delta-fmap-mu-to-tail/ として部分的な等式を証明してから可換性を証明する。
+        \verb/delta-fmap-mu-to-tail/ では Delta のバージョンが \verb/Delta (Delta (Delta A (S (S m))) (S (S m))) (S n)/ となっていることに注目してもらいたい。
+
+        \verb/delta-fmap-mu-to-tail/ に加え、 $ \mu $ が natural transformation であることを利用して再帰的に定義することで証明ができる。
+
 \begin{table}[html]
     \lstinputlisting[basicstyle={\scriptsize},
                      numberstyle={\tiny},
@@ -312,3 +328,13 @@
 
 \end{enumerate}
 
+
+Delta Monad の定義と、5つの証明を用いて Moand の record が構築できることを確認する(リスト\ref{src:delta_is_monad})。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:delta_is_monad, caption= Agda における Delta が Monad 則を満たす証明] {src/delta_is_monad.agda.replaced}
+\end{table}
+
+全ての Delta が同じバージョンを持つ時、 $ triple(T, \eta, \mu) $ は Monad則を満たすことを示せた。
+
+% }}}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/delta_is_monad.agda	Sun Feb 15 12:35:58 2015 +0900
@@ -0,0 +1,10 @@
+delta-is-monad : {l : Level} {n : Nat} ->
+        Monad {l} (\A -> Delta A (S n))  delta-is-functor
+delta-is-monad = record
+              { eta             = delta-eta;
+                mu              = delta-mu;
+                eta-is-nt       = delta-eta-is-nt;
+                mu-is-nt        = delta-mu-is-nt;
+                association-law = delta-association-law;
+                left-unity-law  = delta-left-unity-law ;
+                right-unity-law = \x -> (sym (delta-right-unity-law x)) }