# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1412663531 -32400
# Node ID c2f40b6d4027b0e5fb0c960c1227d44146a0ac9e
# Parent  e0ba1bf564ddc2508712d4bc5d84de2483d6aa09
Expand monad-law-1

diff -r e0ba1bf564dd -r c2f40b6d4027 agda/similar.agda
--- 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)
+  ∎
+