Mercurial > hg > Members > atton > delta_monad

changeset 30:c2f40b6d4027

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Expand monad-law-1
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 07 Oct 2014 15:32:11 +0900
parents e0ba1bf564dd
children 33b386de3f56
files agda/similar.agda
diffstat 1 files changed, 14 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/agda/similar.agda	Tue Oct 07 15:09:17 2014 +0900
+++ b/agda/similar.agda	Tue Oct 07 15:32:11 2014 +0900
@@ -27,16 +27,28 @@
 
 --monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu
 
+{-
 monad-law-1 : {l : Level} {A : Set l} -> (s : Similar (Similar (Similar A))) -> ((mu ∙ (fmap mu)) s) ≡ ((mu ∙ mu) s)
 monad-law-1 s = begin
     ((mu ∙ (fmap mu)) s)
   ≡⟨⟩
     mu (fmap mu s)
-  ≡⟨ {!!} ⟩
-     mu (mu s)
+  ≡⟨ cong mu {!!} ⟩
+    mu (mu s)
   ≡⟨⟩
     ((mu ∙ mu) s)
   ∎
+-}
+
+monad-law-1-sub : {l : Level} {A : Set l} -> (s : Similar (Similar (Similar A))) -> fmap mu s ≡ mu s
+monad-law-1-sub (similar lx (similar llx (similar lllx x _ _) _ _) ly (similar _ _ lly (similar _ _ llly y))) = begin
+    similar lx (mu (similar llx (similar lllx x _ _) _ _)) ly
+      (mu (similar _ _ lly (similar _ _ llly y)))
+  ≡⟨ {!!} ⟩
+    similar (lx ++ llx) (similar lllx x _ _) (ly ++ lly)
+      (similar _ _ llly y)
+  ∎
+