# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1413702052 -32400
# Node ID b9b26b470cc22ad6a5a716efad1eb0aeff3be797
# Parent  6ce83b2c9e596e4224498a999f150b1f1b3e1f53
Add Comments

diff -r 6ce83b2c9e59 -r b9b26b470cc2 agda/similar.agda
--- a/agda/similar.agda	Sun Oct 19 15:53:55 2014 +0900
+++ b/agda/similar.agda	Sun Oct 19 16:00:52 2014 +0900
@@ -48,9 +48,9 @@
 
 
 
--- Monad-laws
+-- Monad-laws (Category)
 
---monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu
+-- monad-law-1 : join . fmap join = join . join
 monad-law-1 : {l : Level} {A : Set l} -> (s : Similar (Similar (Similar A))) -> ((mu ∙ (fmap mu)) s) ≡ ((mu ∙ mu) s)
 monad-law-1 (similar lx (similar llx (similar lllx x _ _) _ (similar _ _ _ _)) 
                      ly (similar   _ (similar _ _ _ _)  lly (similar _ _  llly y))) = begin
@@ -62,7 +62,8 @@
   ∎
 
 
---monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡ id
+-- monad-law-2 : join . fmap return = join . return = id
+-- monad-law-2-1 join . fmap return = join . return
 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
@@ -73,14 +74,15 @@
     similar lx x ly y
   ∎
 
+-- monad-law-2-2 :  join . return = id
 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 : return . f = fmap f . return
 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 : join . fmap (fmap f) = fmap f . join
 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