Mercurial > hg > Members > atton > delta_monad

comparison agda/laws.agda @ 102:9c62373bd474

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 25 Jan 2015 12:16:34 +0900
parents f26a954cd068
children a271f3ff1922
comparison
equal deleted inserted replaced
101:29c54b0197fb 102:9c62373bd474
41 bind : {A B : Set l} -> M A -> (A -> (M B)) -> M B 41 bind : {A B : Set l} -> M A -> (A -> (M B)) -> M B
42 field -- category laws 42 field -- category laws
43 association-law : (x : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x 43 association-law : (x : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x
44 left-unity-law : (x : M A) -> (mu ∙ (fmap functorM eta)) x ≡ id x 44 left-unity-law : (x : M A) -> (mu ∙ (fmap functorM eta)) x ≡ id x
45 right-unity-law : (x : M A) -> id x ≡ (mu ∙ eta) x 45 right-unity-law : (x : M A) -> id x ≡ (mu ∙ eta) x
46 field -- natural transformations
47 eta-is-nt : {B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap functorM f (eta x)
48
46 49
47 open Monad 50 open Monad