Mercurial > hg > Members > atton > delta_monad

annotate agda/laws.agda @ 90:55d11ce7e223

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Unify levels on data type. only use suc to proofs
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 19 Jan 2015 12:11:38 +0900
parents 6789c65a75bc
children bcd4fe52a504
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
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
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
90
55d11ce7e223 Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
18 record NaturalTransformation {l : Level} (F G : Set l -> Set l)
86
5c083ddd73ed Add record definitions. functor, natural-transformation, monad.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 (functorF : Functor F)
90
55d11ce7e223 Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
20 (functorG : Functor G) : Set (suc l) where
86
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