# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1413609180 -32400
# Node ID b7c4e6276bcf482621b28241a62678bfc195344b
# Parent  0bc402f970b3466910aecc0d16693d7e5d7b80d3
Proof Monad-law-2-1

diff -r 0bc402f970b3 -r b7c4e6276bcf agda/similar.agda
--- a/agda/similar.agda	Sat Oct 18 14:04:33 2014 +0900
+++ b/agda/similar.agda	Sat Oct 18 14:13:00 2014 +0900
@@ -16,7 +16,7 @@
 mu : {l : Level} {A : Set l} -> Similar (Similar A) -> Similar A
 mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y
 
-return : {A : Set} -> A -> Similar A
+return : {l : Level} {A : Set l} -> A -> Similar A
 return x = similar [] x [] x
 
 returnS : {A : Set} -> A -> Similar A
@@ -37,11 +37,19 @@
     similar (lx ++ llx ++ lllx) x (ly ++ lly ++ llly) y
   ∎
 
+
+--monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡ id
+monad-law-2-1 : {l : Level} {A : Set l} -> (s : Similar  A) ->
+  (mu ∙ fmap return) s ≡ (mu ∙ return) s
+monad-law-2-1 (similar lx x ly y) = begin
+    similar (lx ++ []) x (ly ++ []) y
+  ≡⟨ cong (\left-list -> similar left-list x (ly ++ []) y) (empty-append lx)⟩
+    similar lx x (ly ++ []) y
+  ≡⟨ cong (\right-list -> similar lx x right-list y) (empty-append ly) ⟩
+    similar lx x ly y
+  ∎
+
 {-
---monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡id
-monad-law-2-1 : mu ∙ fmap return ≡ mu ∙ return
-monad-law-2-1 = {!!}
-
 monad-law-2-2 : mu ∙ return ≡ id
 monad-law-2-2 = {!!}