Mercurial > hg > Members > atton > delta_monad

diff agda/similar.agda @ 35:c5cdbedc68ad

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proof Monad-law-2-2
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sat, 18 Oct 2014 14:15:13 +0900
parents b7c4e6276bcf
children 169ec60fcd36
line wrap: on
line diff
--- 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 = {!!}