Mercurial > hg > Members > atton > similar_monad
changeset 36:169ec60fcd36
Proof Monad-law-4
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 18 Oct 2014 14:22:34 +0900 |
| parents | c5cdbedc68ad |
| children | 743c05b98dad |
| files | agda/similar.agda |
| diffstat | 1 files changed, 7 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- 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