Mercurial > hg > Members > atton > delta_monad
annotate agda/laws.agda @ 112:0a3b6cb91a05
Prove left-unity-law for DeltaM
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 30 Jan 2015 21:57:31 +0900 |
parents | a271f3ff1922 |
children | 47f144540d51 |
rev | line source |
---|---|
86
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Relation.Binary.PropositionalEquality |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Level |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open import basic |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 module laws where |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
7 record Functor {l : Level} (F : Set l -> Set l) : Set (suc l) where |
86
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 field |
90
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
87
diff
changeset
|
9 fmap : {A B : Set l} -> (A -> B) -> (F A) -> (F B) |
86
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 field |
90
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
87
diff
changeset
|
11 preserve-id : {A : Set l} (x : F A) → fmap id x ≡ id x |
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
87
diff
changeset
|
12 covariant : {A B C : Set l} (f : A -> B) -> (g : B -> C) -> (x : F A) |
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
87
diff
changeset
|
13 -> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
14 field |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
15 fmap-equiv : {A B : Set l} {f g : A -> B} -> ((x : A) -> f x ≡ g x) -> (x : F A) -> fmap f x ≡ fmap g x |
86
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 open Functor |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 |
97
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
18 record NaturalTransformation {l : Level} (F G : {l' : Level} -> Set l' -> Set l') |
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
19 {fmapF : {A B : Set l} -> (A -> B) -> (F A) -> (F B)} |
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
20 {fmapG : {A B : Set l} -> (A -> B) -> (G A) -> (G B)} |
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
21 (natural-transformation : {A : Set l} -> F A -> G A) |
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
22 : Set (suc l) where |
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
23 field |
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
24 commute : {A B : Set l} -> (f : A -> B) -> (x : F A) -> |
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
25 natural-transformation (fmapF f x) ≡ fmapG f (natural-transformation x) |
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
26 open NaturalTransformation |
86
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 -- simple Monad definition. without NaturalTransformation (mu, eta) and monad-law with f. |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
33 record Monad {l : Level} (M : Set l -> Set l) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
34 (functorM : Functor M) |
86
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 : Set (suc l) where |
94
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
36 field -- category |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
37 mu : {A : Set l} -> M (M A) -> M A |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
38 eta : {A : Set l} -> A -> M A |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
39 field -- haskell |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
40 return : {A : Set l} -> A -> M A |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
41 bind : {A B : Set l} -> M A -> (A -> (M B)) -> M B |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
42 field -- category laws |
103
a271f3ff1922
Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
102
diff
changeset
|
43 association-law : {A : Set l} -> (x : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x |
a271f3ff1922
Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
102
diff
changeset
|
44 left-unity-law : {A : Set l} -> (x : M A) -> (mu ∙ (fmap functorM eta)) x ≡ id x |
a271f3ff1922
Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
102
diff
changeset
|
45 right-unity-law : {A : Set l} -> (x : M A) -> id x ≡ (mu ∙ eta) x |
102
9c62373bd474
Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
97
diff
changeset
|
46 field -- natural transformations |
103
a271f3ff1922
Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
102
diff
changeset
|
47 eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap functorM f (eta x) |
102
9c62373bd474
Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
97
diff
changeset
|
48 |
86
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 |
97
f26a954cd068
Update Natural Transformation definitions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
50 open Monad |