# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1422934948 -32400
# Node ID d57c88171f38082150ea20b549cbff6f2b55cc72
# Parent  d9a30f696933a51617c9475e2ec050b1ea801e63
Prove assciation-law for DeltaM on (S O)

diff -r d9a30f696933 -r d57c88171f38 agda/deltaM/monad.agda
--- a/agda/deltaM/monad.agda	Tue Feb 03 12:24:26 2015 +0900
+++ b/agda/deltaM/monad.agda	Tue Feb 03 12:42:28 2015 +0900
@@ -74,7 +74,7 @@
 
 
 
-
+{-
 -- main proofs
 
 deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat}
@@ -186,7 +186,7 @@
   ≡⟨ refl ⟩
   deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (delta x d)))
   ∎
-{-
+
 
 
 
@@ -296,12 +296,50 @@
 
 -}
 
+postulate deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat}
+                  {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
+                  (f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) ->
+                  deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d)
 
 deltaM-association-law : {l : Level} {A : Set l} {n : Nat}
                          {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
                          (d : DeltaM M (DeltaM M (DeltaM M A (S n)) (S n))  (S n)) ->
                          deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d)
-deltaM-association-law {l} {A}   {O} {T} {F} {M} (deltaM (mono x)) = {!!}
+deltaM-association-law {l} {A}   {O} {T} {F} {M} (deltaM (mono x))    = begin
+  deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x)))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (fmap F deltaM-mu x)))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-mu x)))))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-mu x))))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-mu headDeltaM x)) ⟩
+  deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ deltaM-mu) x)))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x)))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F headDeltaM ((mu M) ∙ (fmap F headDeltaM)) x) ⟩
+  deltaM (mono (mu M ((((fmap F (((mu M) ∙ (fmap F headDeltaM)))) ∙ (fmap F headDeltaM)) x))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M ((((fmap F (((mu M) ∙ (fmap F headDeltaM)))) (fmap F headDeltaM x))))))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F (fmap F headDeltaM) (mu M) (fmap F headDeltaM x)) ⟩
+  deltaM (mono (mu M (((fmap F (mu M)) ∙ (fmap F (fmap F headDeltaM))) (fmap F headDeltaM x))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (mu M) ((fmap F (fmap F headDeltaM) (fmap F headDeltaM x))))))
+  ≡⟨ cong (\de -> deltaM (mono de)) (association-law M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))) ⟩
+  deltaM (mono (mu M (mu M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x)))))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (mu-is-nt M headDeltaM (fmap F headDeltaM x)) ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (mu M (fmap F (headDeltaM {M = M}) x)))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x))))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono x)))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM-mu (deltaM (mono x)))
+
+  ∎
+deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = {!!}
 {-
 deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
   deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d)))