# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1413607938 -32400
# Node ID 71906644d20647c029b3f54a6637375b240cf587
# Parent  33b386de3f560c40003d5f28c765ffc9ab25bb96
Expand monad-law 1

diff -r 33b386de3f56 -r 71906644d206 agda/similar.agda
--- 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