--- a/proof_delta.tex	Sun Feb 15 10:33:47 2015 +0900
+++ b/proof_delta.tex	Sun Feb 15 11:17:59 2015 +0900
@@ -232,6 +232,7 @@
 
 Delta Monad に対応する $ triple (T, \eta, \mu ) $ が定義できた。
 これから Monad 則を満たすことを証明していく。
+% TODO: layout
 
 \begin{enumerate}
     \item  $ \eta $ が natural transformation であること
@@ -268,6 +269,11 @@
 
     \item T に対する演算の単位元が存在する
 
+        図\ref{fig:monad_laws}で示した右側の可換図に相当する。
+        単位元に相当する演算は右側と左側の2つが存在するため、証明も2つに分割する。
+
+        右側単位元の証明をリスト\ref{src:delta_right_unity_law}に示す。
+
 \begin{table}[html]
     \lstinputlisting[basicstyle={\scriptsize},
                      numberstyle={\tiny},
@@ -276,6 +282,11 @@
                      {src/delta_right_unity_law.agda.replaced}
 \end{table}
 
+        バージョンが1である時は同じ項となるため refl となる。
+        バージョンが1以上である時は再帰的に定義することになるが、途中で $ \eta $ が natural transformation である性質を利用している。
+
+        次に左側単位元の証明をリスト\ref{src:delta_left_unity_law}に示す。
+
 \begin{table}[html]
     \lstinputlisting[basicstyle={\scriptsize},
                      numberstyle={\tiny},
@@ -284,8 +295,13 @@
                      {src/delta_left_unity_law.agda.replaced}
 \end{table}
 
+        これまでの証明と同様にバージョンが1である場合は定義から同じ項となる。
+        バージョンが1以上の場合、Functor則の関数の合成の保存を利用して証明を再帰的に行なう。
+
     \item T に対する演算の可換性が存在する
 
+        図\ref{fig:monad_laws}で示した左側の可換図に相当する。
+
 \begin{table}[html]
     \lstinputlisting[basicstyle={\scriptsize},
                      numberstyle={\tiny},
@@ -296,5 +312,3 @@
 
 \end{enumerate}
 
-
-