Mercurial > hg > Members > atton > delta_monad
diff agda/laws.agda @ 115:e6bcc7467335
Temporary commit : Proving association-law ...
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 01 Feb 2015 17:06:55 +0900 |
parents | 47f144540d51 |
children | 673e1ca0d1a9 |
line wrap: on
line diff
--- a/agda/laws.agda Fri Jan 30 22:17:46 2015 +0900 +++ b/agda/laws.agda Sun Feb 01 17:06:55 2015 +0900 @@ -43,6 +43,7 @@ right-unity-law : {A : Set l} -> (x : M A) -> id x ≡ (mu ∙ eta) x field -- natural transformations eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap functorM f (eta x) + mu-is-nt : {A B : Set l} -> (f : A -> B) -> (x : M (M A)) -> mu (fmap functorM (fmap functorM f) x) ≡ fmap functorM f (mu x) open Monad \ No newline at end of file