Mercurial > hg > Members > atton > delta_monad

comparison agda/laws.agda @ 115:e6bcc7467335

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
114:08403eb8db8b 115:e6bcc7467335
41 association-law : {A : Set l} -> (x : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x 41 association-law : {A : Set l} -> (x : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x
42 left-unity-law : {A : Set l} -> (x : M A) -> (mu ∙ (fmap functorM eta)) x ≡ id x 42 left-unity-law : {A : Set l} -> (x : M A) -> (mu ∙ (fmap functorM eta)) x ≡ id x
43 right-unity-law : {A : Set l} -> (x : M A) -> id x ≡ (mu ∙ eta) x 43 right-unity-law : {A : Set l} -> (x : M A) -> id x ≡ (mu ∙ eta) x
44 field -- natural transformations 44 field -- natural transformations
45 eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap functorM f (eta x) 45 eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap functorM f (eta x)
46 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)
46 47
47 48
48 open Monad 49 open Monad