# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1424066711 -32400
# Node ID 398b42a1ac19b85a9c3ca0b15b232582e82f53f9
# Parent  43213dcf8d24642d48d259af19d2cafac2f76a9c
Fix layouts

diff -r 43213dcf8d24 -r 398b42a1ac19 proof_delta.tex
--- a/proof_delta.tex	Mon Feb 16 13:47:50 2015 +0900
+++ b/proof_delta.tex	Mon Feb 16 15:05:11 2015 +0900
@@ -235,7 +235,6 @@
 
 Delta Monad に対応する $ triple (T, \eta, \mu ) $ が定義できた。
 これから Monad 則を満たすことを証明していく。
-% TODO: layout
 
 \begin{enumerate}
     \item  $ \eta $ が natural transformation であること
@@ -246,11 +245,9 @@
         特に n が O である時は同じ項に簡約されるために refl で証明することができ、n が O 以上であれば再帰的に証明することができる。
 
 
-\begin{table}[html]
-    \lstinputlisting[label=src:delta_eta_is_nt_in_agda,
-                    caption= Agda における Delta の $ \eta$ が natural transformation である証明]
-                    {src/delta_eta_is_nt.agda.replaced}
-\end{table}
+        \lstinputlisting[label=src:delta_eta_is_nt_in_agda,
+                        caption= Agda における Delta の $ \eta$ が natural transformation である証明]
+                        {src/delta_eta_is_nt.agda.replaced}
     \item $ \mu $ が natural transformation であること
 
         次に $ \mu $ が natural transformation であることを示す(リスト\ref{src:delta_mu_is_nt_in_agda})。
@@ -270,6 +267,8 @@
                      {src/delta_mu_is_nt.agda.replaced}
 \end{table}
 
+\newpage
+
     \item T に対する演算の単位元が存在する
 
         図\ref{fig:monad_laws}で示した右側の可換図に相当する。
@@ -277,13 +276,11 @@
 
         右側単位元の証明をリスト\ref{src:delta_right_unity_law}に示す。
 
-\begin{table}[html]
     \lstinputlisting[basicstyle={\scriptsize},
                      numberstyle={\tiny},
                      label=src:delta_right_unity_law,
                      caption= Agda における Delta に対する演算に右側単位元が存在する証明]
                      {src/delta_right_unity_law.agda.replaced}
-\end{table}
 
         バージョンが1である時は同じ項となるため refl となる。
         バージョンが1以上である時は再帰的に定義することになるが、途中で $ \eta $ が natural transformation である性質を利用している。
@@ -304,6 +301,15 @@
     \item T に対する演算の可換性が存在する
 
         図\ref{fig:monad_laws}で示した左側の可換図に相当する。
+        演算の可換性の証明をリスト\ref{src:delta_association_law}に示す。
+
+\begin{table}[html]
+    \lstinputlisting[basicstyle={\scriptsize},
+                     numberstyle={\tiny},
+                     label=src:delta_association_law,
+                     caption= Agda における Delta に対する演算に可換性が存在する証明]
+                     {src/delta_association_law.agda.replaced}
+\end{table}
 
         $ \mu $ を用いて TTT から T にする際に、右側2つのTに対して先に $ \mu $ を用いるか、左側2つから先に用いるかの可換性である。
         よって \verb/Delta (Delta (Delta A))/から \verb/Delta A/ とする演算の等式となる。
@@ -318,14 +324,6 @@
 
         \verb/delta-fmap-mu-to-tail/ に加え、 $ \mu $ が natural transformation であることを利用して再帰的に定義することで証明ができる。
 
-\begin{table}[html]
-    \lstinputlisting[basicstyle={\scriptsize},
-                     numberstyle={\tiny},
-                     label=src:delta_association_law,
-                     caption= Agda における Delta に対する演算に可換性が存在する証明]
-                     {src/delta_association_law.agda.replaced}
-\end{table}
-
 \end{enumerate}