Mercurial > hg > Members > atton > delta_monad
annotate agda/laws.agda @ 87:6789c65a75bc
Split functor-proofs into delta.functor
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 19 Jan 2015 11:00:34 +0900 |
parents | 5c083ddd73ed |
children | 55d11ce7e223 |
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 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 record Functor {l : Level} (F : Set l -> Set l) : (Set (suc l)) where |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 field |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 fmap : ∀{A B} -> (A -> B) -> (F A) -> (F B) |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 field |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 preserve-id : ∀{A} (x : F A) → fmap id x ≡ id x |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 covariant : ∀{A B C} (f : A -> B) -> (g : B -> C) -> (x : F A) |
87
6789c65a75bc
Split functor-proofs into delta.functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
86
diff
changeset
|
13 -> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x |
86
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 open Functor |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 record NaturalTransformation {l ll : Level} (F G : Set l -> Set l) |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 (functorF : Functor F) |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 (functorG : Functor G) : Set (suc (l ⊔ ll)) where |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 field |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 natural-transformation : {A : Set l} -> F A -> G A |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 field |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 commute : ∀ {A B} -> (f : A -> B) -> (x : F A) -> |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 natural-transformation (fmap functorF f x) ≡ fmap functorG f (natural-transformation x) |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 open NaturalTransformation |
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 -- simple Monad definition. without NaturalTransformation (mu, eta) and monad-law with f. |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 record Monad {l : Level} {A : Set l} |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 (M : {ll : Level} -> Set ll -> Set ll) |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 (functorM : Functor M) |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 : Set (suc l) where |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 field |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 mu : {A : Set l} -> M (M A) -> M A |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 eta : {A : Set l} -> A -> M A |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 field |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 association-law : (x : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 left-unity-law : (x : M A) -> (mu ∙ (fmap functorM eta)) x ≡ id x |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 right-unity-law : (x : M A) -> id x ≡ (mu ∙ eta) x |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 |
5c083ddd73ed
Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 open Monad |