# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1422451561 -32400
# Node ID d47aea3f92466b1ad289558cf940d7cf2503cfc0
# Parent  caaf364f45ac1d0b777ccebc2f9c6b70d8442749
Delete comment outed temporary code

diff -r caaf364f45ac -r d47aea3f9246 agda/delta/monad.agda
--- a/agda/delta/monad.agda	Wed Jan 28 22:21:27 2015 +0900
+++ b/agda/delta/monad.agda	Wed Jan 28 22:26:01 2015 +0900
@@ -11,11 +11,12 @@
 
 module delta.monad where
 
-tailDelta-is-nt : {l : Level} {A B : Set l} {n : Nat} 
+tailDelta-is-nt : {l : Level} {A B : Set l} {n : Nat}
                   (f : A -> B) -> (d : Delta A (S (S n))) ->
                   (tailDelta {n = n} ∙ (delta-fmap f)) d ≡ ((delta-fmap f) ∙ tailDelta {n = n}) d
 tailDelta-is-nt f (delta x d) = refl
 
+
 tailDelta-to-tail-nt : {l : Level} {A B : Set l} (n m  : Nat)
                        (f : A -> B) (d : Delta (Delta A (S (S m))) (S n)) ->
                    delta-fmap tailDelta (delta-fmap (delta-fmap f) d) ≡ delta-fmap (delta-fmap f) (delta-fmap tailDelta d)
@@ -30,14 +31,13 @@
   ∎
 tailDelta-to-tail-nt (S n) (S m) f (delta (delta x (delta xx d)) ds) = begin
   delta (delta (f xx) (delta-fmap f d))
-    (delta-fmap tailDelta (delta-fmap (delta-fmap f) ds)) 
+    (delta-fmap tailDelta (delta-fmap (delta-fmap f) ds))
   ≡⟨ cong (\de -> delta (delta (f xx) (delta-fmap f d)) de) (tailDelta-to-tail-nt n (S m) f ds) ⟩
   delta (delta (f xx) (delta-fmap f d))
     (delta-fmap (delta-fmap f) (delta-fmap tailDelta ds))
   ∎
 
 
-
 delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat}
                   (f : A -> B) -> (x : A) -> (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x)
 delta-eta-is-nt {n = O}   f x = refl
@@ -70,7 +70,7 @@
 delta-fmap-mu-to-tail O O (mono (delta d ds)) = refl
 delta-fmap-mu-to-tail O (S n) (mono (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds))) = refl
 delta-fmap-mu-to-tail (S n) O (delta (delta (delta x (mono xx)) (mono (delta dx (mono dxx)))) ds) = begin
-  delta (mono dxx) (delta-fmap tailDelta (delta-fmap delta-mu ds)) 
+  delta (mono dxx) (delta-fmap tailDelta (delta-fmap delta-mu ds))
   ≡⟨ cong (\de -> delta (mono dxx) de) (delta-fmap-mu-to-tail n O ds) ⟩
   delta (mono dxx)
     (delta-fmap delta-mu
@@ -92,7 +92,7 @@
               ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d)
 monad-law-1 {n =       O} (mono d)                          = refl
 monad-law-1 {n = S n} (delta (delta (delta x d) dd) ds) = begin
-  delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) 
+  delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds)))
   ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-fmap-mu-to-tail n n ds) ⟩
   delta x (delta-mu (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
   ≡⟨ cong (\de -> delta x de) (monad-law-1 (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) ⟩
@@ -102,58 +102,6 @@
   ∎
 
 
-{-
-  begin
-  delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) ≡⟨ {!!} ⟩
-  delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds))))
-  ∎
--}
-{-
-monad-law-1 {n = S O} (delta (delta (delta _ _) _) (mono (delta (delta _ (mono _)) (mono (delta _ (mono _)))))) = refl
-monad-law-1 {n = S n} (delta (delta (delta x d) dd) ds) = begin
-  (delta-mu ∙ delta-fmap delta-mu) (delta (delta (delta x d) dd) ds) ≡⟨ refl ⟩
-  delta-mu (delta-fmap delta-mu (delta (delta (delta x d) dd) ds)) ≡⟨ refl ⟩
-  delta-mu (delta (delta-mu (delta (delta x d) dd)) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
-  delta-mu (delta (delta (headDelta (delta x d)) (delta-mu (delta-fmap tailDelta dd))) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
-  delta-mu (delta (delta x (delta-mu (delta-fmap tailDelta dd))) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
-  delta (headDelta (delta x (delta-mu (delta-fmap tailDelta dd)))) (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) ≡⟨ refl ⟩
-  delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds)))
-  ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (functor-law-2 tailDelta delta-mu ds)) ⟩
-  delta x (delta-mu (delta-fmap (tailDelta {n = n} ∙ delta-mu {n = (S n)}) ds))
---  ≡⟨ cong (\ff -> delta x (delta-mu (delta-fmap ff ds))) hoge ⟩
-  ≡⟨ {!!} ⟩
-  delta x (delta-mu (delta-fmap (((delta-mu {n = n}) ∙ (delta-fmap tailDelta)) ∙ tailDelta) ds))
-  ≡⟨ cong (\de -> delta x (delta-mu de)) (functor-law-2 (delta-mu ∙ (delta-fmap tailDelta)) tailDelta ds ) ⟩
-  delta x (delta-mu (delta-fmap ((delta-mu {n = n}) ∙ (delta-fmap tailDelta)) (delta-fmap tailDelta ds)))
-  ≡⟨ cong (\de -> delta x (delta-mu de)) (functor-law-2 delta-mu (delta-fmap tailDelta) (delta-fmap tailDelta ds)) ⟩
-  delta x (delta-mu (delta-fmap (delta-mu {n = n}) (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
-  ≡⟨ cong (\de -> delta x de) (monad-law-1 (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))  ⟩
-  delta x (delta-mu (delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
-  ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-mu-is-nt tailDelta (delta-fmap tailDelta ds)) ⟩
-  delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) ≡⟨ refl ⟩
-  delta (headDelta (delta x d)) (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) ≡⟨ refl ⟩
-  delta-mu (delta (delta x d) (delta-mu (delta-fmap tailDelta ds))) ≡⟨ refl ⟩
-  delta-mu (delta (headDelta (delta (delta x d) dd)) (delta-mu (delta-fmap tailDelta ds))) ≡⟨ refl ⟩
-  delta-mu (delta-mu (delta (delta (delta x d) dd) ds)) ≡⟨ refl ⟩
-  (delta-mu ∙ delta-mu) (delta (delta (delta x d) dd) ds)
-  ∎
--}
-{-
-begin
-  (delta-mu ∙ delta-fmap delta-mu) (delta d ds) ≡⟨ refl ⟩
-  delta-mu (delta-fmap delta-mu (delta d ds)) ≡⟨ refl ⟩
-  delta-mu (delta (delta-mu d) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
-  delta (headDelta (delta-mu d)) (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) ≡⟨ {!!} ⟩
-  delta (headDelta (headDelta d)) (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) ≡⟨ refl ⟩
-  delta-mu (delta (headDelta d) (delta-mu (delta-fmap tailDelta ds))) ≡⟨ refl ⟩
-  delta-mu (delta-mu (delta d ds)) ≡⟨ refl ⟩
-  (delta-mu ∙ delta-mu) (delta d ds)
-  ∎
--}
-
-
-
-
 delta-right-unity-law : {l : Level} {A : Set l} {n : Nat} (d : Delta A (S n)) -> (delta-mu ∙ delta-eta) d ≡ id d
 delta-right-unity-law (mono x)    = refl
 delta-right-unity-law (delta x d) = begin