Mercurial > hg > Members > atton > delta_monad
diff agda/laws.agda @ 144:575de2e38385
Fix names left/right unity law
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 25 Feb 2015 14:49:50 +0900 |
| parents | d205ff1e406f |
| children |
line wrap: on
line diff
--- a/agda/laws.agda Wed Feb 25 14:36:02 2015 +0900 +++ b/agda/laws.agda Wed Feb 25 14:49:50 2015 +0900 @@ -40,8 +40,8 @@ mu-is-nt : {A B : Set l} -> (f : A -> B) -> (x : T (T A)) -> mu (fmap F (fmap F f) x) ≡ fmap F f (mu x) field -- category laws association-law : {A : Set l} -> (x : (T (T (T A)))) -> (mu ∙ (fmap F mu)) x ≡ (mu ∙ mu) x - left-unity-law : {A : Set l} -> (x : T A) -> (mu ∙ (fmap F eta)) x ≡ id x - right-unity-law : {A : Set l} -> (x : T A) -> id x ≡ (mu ∙ eta) x + right-unity-law : {A : Set l} -> (x : T A) -> (mu ∙ (fmap F eta)) x ≡ id x + left-unity-law : {A : Set l} -> (x : T A) -> id x ≡ (mu ∙ eta) x open Monad