Mercurial > hg > Members > atton > similar_monad
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 = {!!}