Mercurial > hg > Members > atton > delta_monad
annotate agda/laws.agda @ 126:5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 03 Feb 2015 11:45:33 +0900 |
parents | 673e1ca0d1a9 |
children | d205ff1e406f |
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) |
126
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
121
diff
changeset
|
10 field -- laws |
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 |
126
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
121
diff
changeset
|
14 field -- proof assistant |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
121
diff
changeset
|
15 fmap-equiv : {A B : Set l} {f g : A -> B} -> ((x : A) -> f x ≡ g x) -> (fx : F A) -> fmap f fx ≡ fmap g fx |
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 |
121
673e1ca0d1a9
Refactor monad definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
18 record NaturalTransformation {l : Level} (F G : Set l -> Set l) |
97
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 |
121
673e1ca0d1a9
Refactor monad definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
32 -- Categorical Monad definition. without haskell-laws (bind) |
673e1ca0d1a9
Refactor monad definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
33 record Monad {l : Level} (T : Set l -> Set l) (F : Functor T) : Set (suc l) where |
94
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
34 field -- category |
121
673e1ca0d1a9
Refactor monad definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
35 mu : {A : Set l} -> T (T A) -> T A |
673e1ca0d1a9
Refactor monad definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
36 eta : {A : Set l} -> A -> T A |
673e1ca0d1a9
Refactor monad definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
37 field -- natural transformations |
673e1ca0d1a9
Refactor monad definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
38 eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap F f (eta x) |
673e1ca0d1a9
Refactor monad definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
39 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) |
94
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
40 field -- category laws |
121
673e1ca0d1a9
Refactor monad definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
41 association-law : {A : Set l} -> (x : (T (T (T A)))) -> (mu ∙ (fmap F mu)) x ≡ (mu ∙ mu) x |
673e1ca0d1a9
Refactor monad definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
42 left-unity-law : {A : Set l} -> (x : T A) -> (mu ∙ (fmap F eta)) x ≡ id x |
673e1ca0d1a9
Refactor monad definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
43 right-unity-law : {A : Set l} -> (x : T 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
|
44 |
86
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 |
121
673e1ca0d1a9
Refactor monad definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
46 open Monad |