Mercurial > hg > Members > atton > similar_monad

changeset 32:71906644d206

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 Sat, 18 Oct 2014 13:52:18 +0900
parents 33b386de3f56
children 0bc402f970b3
files agda/similar.agda
diffstat 1 files changed, 6 insertions(+), 23 deletions(-) [+]
line wrap: on
line diff
--- a/agda/similar.agda	Sat Oct 18 13:38:29 2014 +0900
+++ b/agda/similar.agda	Sat Oct 18 13:52:18 2014 +0900
@@ -27,31 +27,14 @@
 
 --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)
-  ≡⟨ cong mu {!!} ⟩
-    mu (mu s)
-  ≡⟨⟩
-    ((mu ∙ mu) s)
+monad-law-1 (similar lx (similar llx (similar lllx x _ _) _ (similar _ _ _ _)) 
+                     ly (similar   _ (similar _ _ _ _)  lly (similar _ _  llly y))) = begin
+    similar (lx ++ (llx ++ lllx)) x (ly ++ (lly ++ llly)) y
+  ≡⟨ {!!} ⟩
+    similar (lx ++ llx ++ lllx) x (ly ++ lly ++ llly) y
   ∎
--}
-
-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)
-  ∎
-
-
-
-
 
 {-
 --monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡id