Mercurial > hg > Members > atton > delta_monad

comparison agda/laws.agda @ 86:5c083ddd73ed

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add record definitions. functor, natural-transformation, monad.
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 18 Jan 2015 20:59:27 +0900
parents
children 6789c65a75bc
comparison
equal deleted inserted replaced
85:a1723b3ea997 86:5c083ddd73ed
1 open import Relation.Binary.PropositionalEquality
2 open import Level
3 open import basic
4
5 module laws where
6
7 record Functor {l : Level} (F : Set l -> Set l) : (Set (suc l)) where
8 field
9 fmap : ∀{A B} -> (A -> B) -> (F A) -> (F B)
10 field
11 preserve-id : ∀{A} (x : F A) → fmap id x ≡ id x
12 covariant : ∀{A B C} (f : A -> B) -> (g : B -> C) -> (x : F A)
13 -> fmap (g ∙ f) x ≡ fmap g (fmap f x)
14 open Functor
15
16
17
18 record NaturalTransformation {l ll : Level} (F G : Set l -> Set l)
19 (functorF : Functor F)
20 (functorG : Functor G) : Set (suc (l ⊔ ll)) where
21 field
22 natural-transformation : {A : Set l} -> F A -> G A
23 field
24 commute : ∀ {A B} -> (f : A -> B) -> (x : F A) ->
25 natural-transformation (fmap functorF f x) ≡ fmap functorG f (natural-transformation x)
26 open NaturalTransformation
27
28
29
30 -- simple Monad definition. without NaturalTransformation (mu, eta) and monad-law with f.
31 record Monad {l : Level} {A : Set l}
32 (M : {ll : Level} -> Set ll -> Set ll)
33 (functorM : Functor M)
34 : Set (suc l) where
35 field
36 mu : {A : Set l} -> M (M A) -> M A
37 eta : {A : Set l} -> A -> M A
38 field
39 association-law : (x : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x
40 left-unity-law : (x : M A) -> (mu ∙ (fmap functorM eta)) x ≡ id x
41 right-unity-law : (x : M A) -> id x ≡ (mu ∙ eta) x
42
43 open Monad