changeset 35:c5cdbedc68ad

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
files agda/basic.agda agda/similar.agda
diffstat 2 files changed, 4 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- 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)
--- 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 = {!!}