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

diff -r b7c4e6276bcf -r c5cdbedc68ad agda/basic.agda
--- a/agda/basic.agda	Sat Oct 18 14:13:00 2014 +0900
+++ b/agda/basic.agda	Sat Oct 18 14:15:13 2014 +0900
@@ -2,7 +2,7 @@
 
 module basic where
 
-id : {l : Level} {A : Set} -> A -> A
+id : {l : Level} {A : Set l} -> A -> A
 id x = x
 
 _∙_ : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} -> (B -> C) -> (A -> B) -> (A -> C)
diff -r b7c4e6276bcf -r c5cdbedc68ad agda/similar.agda
--- a/agda/similar.agda	Sat Oct 18 14:13:00 2014 +0900
+++ b/agda/similar.agda	Sat Oct 18 14:15:13 2014 +0900
@@ -49,10 +49,10 @@
     similar lx x ly y
   ∎
 
+monad-law-2-2 : {l : Level} {A : Set l } -> (s : Similar A) -> (mu ∙ return) s ≡ id s
+monad-law-2-2 (similar lx x ly y) = refl
+
 {-
-monad-law-2-2 : mu ∙ return ≡ id
-monad-law-2-2 = {!!}
-
 monad-law-3 : ∀{f} -> return ∙ f ≡ fmap f ∙ return
 monad-law-3 = {!!}