Mercurial > hg > Members > atton > delta_monad

changeset 92:4d615910c87a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove preserve-id for deltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 19 Jan 2015 14:32:07 +0900
parents f41682b53992
children 8d92ed54a94f
files agda/deltaM/functor.agda
diffstat 1 files changed, 14 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- 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)
   ∎