# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1413609754 -32400
# Node ID 169ec60fcd364e0ae4d022b763b85f072863feba
# Parent  c5cdbedc68ad69bb0cc9b38e75a3398aa9be8925
Proof Monad-law-4

diff -r c5cdbedc68ad -r 169ec60fcd36 agda/similar.agda
--- a/agda/similar.agda	Sat Oct 18 14:15:13 2014 +0900
+++ b/agda/similar.agda	Sat Oct 18 14:22:34 2014 +0900
@@ -52,10 +52,11 @@
 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-3 : ∀{f} -> return ∙ f ≡ fmap f ∙ return
-monad-law-3 = {!!}
+
+monad-law-3 : {l : Level} {A B : Set l} (f : A -> B) (x : A) -> (return ∙ f) x ≡ (fmap f ∙ return) x
+monad-law-3 f x = refl
 
-monad-law-4 : ∀{f} -> mu ∙ fmap (fmap f) ≡ fmap f ∙ mu
-monad-law-4 = {!!}
--}
+
+monad-law-4 : {l : Level} {A B : Set l} (f : A -> B) (s : Similar (Similar A)) ->
+              (mu ∙ fmap (fmap f)) s ≡ (fmap f ∙ mu) s
+monad-law-4 f (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = refl
\ No newline at end of file