# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1421645527 -32400
# Node ID 4d615910c87a02e5be830c52e426603591973c8e
# Parent  f41682b539927d3b86ef0fd7ba4aabff872e2df2
Prove preserve-id for deltaM

diff -r f41682b53992 -r 4d615910c87a agda/deltaM/functor.agda
--- a/agda/deltaM/functor.agda	Mon Jan 19 12:29:29 2015 +0900
+++ b/agda/deltaM/functor.agda	Mon Jan 19 14:32:07 2015 +0900
@@ -24,8 +24,20 @@
   deltaM (mono (id x))                                       ≡⟨ cong (\x -> deltaM (mono x)) refl ⟩
   deltaM (mono x)                                            ∎
 deltaM-preserve-id functorM (deltaM (delta x d)) = begin
-  deltaM-fmap id (deltaM (delta x d))                           ≡⟨ refl ⟩ 
-  deltaM (fmap delta-is-functor (fmap functorM id) (delta x d)) ≡⟨ {!!} ⟩
+  deltaM-fmap id (deltaM (delta x d))                           
+  ≡⟨ refl ⟩ 
+  deltaM (fmap delta-is-functor (fmap functorM id) (delta x d))
+  ≡⟨ refl ⟩
+  deltaM (delta (fmap functorM id x) (fmap delta-is-functor (fmap functorM id) d))
+  ≡⟨ cong (\x -> deltaM (delta x (fmap delta-is-functor (fmap functorM id) d))) (preserve-id functorM x) ⟩
+  deltaM (delta x (fmap delta-is-functor (fmap functorM id) d))
+  ≡⟨ refl ⟩
+  appendDeltaM (deltaM (mono x)) (deltaM (fmap delta-is-functor (fmap functorM id) d))
+  ≡⟨ refl ⟩
+  appendDeltaM (deltaM (mono x)) (deltaM-fmap id (deltaM d))
+  ≡⟨ cong (\d -> appendDeltaM (deltaM (mono x)) d) (deltaM-preserve-id functorM (deltaM d)) ⟩
+  appendDeltaM (deltaM (mono x)) (deltaM d)
+  ≡⟨ refl ⟩
   deltaM (delta x d)
   ∎