Mercurial > hg > Members > atton > delta_monad

comparison agda/laws.agda @ 144:575de2e38385

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
143:f241d521bf65 144:575de2e38385
38 field -- natural transformations 38 field -- natural transformations
39 eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap F f (eta x) 39 eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap F f (eta x)
40 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) 40 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)
41 field -- category laws 41 field -- category laws
42 association-law : {A : Set l} -> (x : (T (T (T A)))) -> (mu ∙ (fmap F mu)) x ≡ (mu ∙ mu) x 42 association-law : {A : Set l} -> (x : (T (T (T A)))) -> (mu ∙ (fmap F mu)) x ≡ (mu ∙ mu) x
43 left-unity-law : {A : Set l} -> (x : T A) -> (mu ∙ (fmap F eta)) x ≡ id x 43 right-unity-law : {A : Set l} -> (x : T A) -> (mu ∙ (fmap F eta)) x ≡ id x
44 right-unity-law : {A : Set l} -> (x : T A) -> id x ≡ (mu ∙ eta) x 44 left-unity-law : {A : Set l} -> (x : T A) -> id x ≡ (mu ∙ eta) x
45 45
46 46
47 open Monad 47 open Monad