Mercurial > hg > Members > atton > delta_monad
annotate agda/deltaM/functor.agda @ 93:8d92ed54a94f
Prove functor-laws for deltaM
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 19 Jan 2015 15:21:29 +0900 |
parents | 4d615910c87a |
children | a271f3ff1922 |
rev | line source |
---|---|
91
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Level |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Relation.Binary.PropositionalEquality |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open ≡-Reasoning |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import basic |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import delta |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import delta.functor |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import deltaM |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import laws |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 open Functor |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 module deltaM.functor where |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 deltaM-preserve-id : {l : Level} {A : Set l} |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 {M : {l' : Level} -> Set l' -> Set l'} |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 (functorM : {l' : Level} -> Functor {l'} M) |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} |
93
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
19 -> (d : DeltaM M {functorM} {monadM} A) -> deltaM-fmap id d ≡ id d |
91
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 deltaM-preserve-id functorM (deltaM (mono x)) = begin |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩ |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 deltaM (fmap delta-is-functor (fmap functorM id) (mono x)) ≡⟨ refl ⟩ |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 deltaM (mono (fmap functorM id x)) ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id functorM x) ⟩ |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 deltaM (mono (id x)) ≡⟨ cong (\x -> deltaM (mono x)) refl ⟩ |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 deltaM (mono x) ∎ |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 deltaM-preserve-id functorM (deltaM (delta x d)) = begin |
92
4d615910c87a
Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
27 deltaM-fmap id (deltaM (delta x d)) |
4d615910c87a
Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
28 ≡⟨ refl ⟩ |
4d615910c87a
Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
29 deltaM (fmap delta-is-functor (fmap functorM id) (delta x d)) |
4d615910c87a
Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
30 ≡⟨ refl ⟩ |
4d615910c87a
Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
31 deltaM (delta (fmap functorM id x) (fmap delta-is-functor (fmap functorM id) d)) |
4d615910c87a
Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
32 ≡⟨ cong (\x -> deltaM (delta x (fmap delta-is-functor (fmap functorM id) d))) (preserve-id functorM x) ⟩ |
4d615910c87a
Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
33 deltaM (delta x (fmap delta-is-functor (fmap functorM id) d)) |
4d615910c87a
Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
34 ≡⟨ refl ⟩ |
4d615910c87a
Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
35 appendDeltaM (deltaM (mono x)) (deltaM (fmap delta-is-functor (fmap functorM id) d)) |
4d615910c87a
Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
36 ≡⟨ refl ⟩ |
4d615910c87a
Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
37 appendDeltaM (deltaM (mono x)) (deltaM-fmap id (deltaM d)) |
4d615910c87a
Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
38 ≡⟨ cong (\d -> appendDeltaM (deltaM (mono x)) d) (deltaM-preserve-id functorM (deltaM d)) ⟩ |
4d615910c87a
Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
39 appendDeltaM (deltaM (mono x)) (deltaM d) |
4d615910c87a
Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
40 ≡⟨ refl ⟩ |
91
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 deltaM (delta x d) |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 ∎ |
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 |
93
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
44 |
91
f41682b53992
Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 deltaM-covariant : {l : Level} {A B C : Set l} -> |
93
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
46 {M : {l' : Level} -> Set l' -> Set l'} |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
47 (functorM : {l' : Level} -> Functor {l'} M) |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
48 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
49 (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A) -> |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
50 (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
51 deltaM-covariant functorM f g (deltaM (mono x)) = begin |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
52 deltaM-fmap (f ∙ g) (deltaM (mono x)) ≡⟨ refl ⟩ |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
53 deltaM (delta-fmap (fmap functorM (f ∙ g)) (mono x)) ≡⟨ refl ⟩ |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
54 deltaM (mono (fmap functorM (f ∙ g) x)) ≡⟨ cong (\x -> (deltaM (mono x))) (covariant functorM g f x) ⟩ |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
55 deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x)) ≡⟨ refl ⟩ |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
56 deltaM-fmap f (deltaM-fmap g (deltaM (mono x))) ∎ |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
57 deltaM-covariant functorM f g (deltaM (delta x d)) = begin |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
58 deltaM-fmap (f ∙ g) (deltaM (delta x d)) |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
59 ≡⟨ refl ⟩ |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
60 deltaM (delta-fmap (fmap functorM (f ∙ g)) (delta x d)) |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
61 ≡⟨ refl ⟩ |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
62 deltaM (delta (fmap functorM (f ∙ g) x) (delta-fmap (fmap functorM (f ∙ g)) d)) |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
63 ≡⟨ refl ⟩ |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
64 appendDeltaM (deltaM (mono (fmap functorM (f ∙ g) x))) (deltaM (delta-fmap (fmap functorM (f ∙ g)) d)) |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
65 ≡⟨ refl ⟩ |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
66 appendDeltaM (deltaM (mono (fmap functorM (f ∙ g) x))) (deltaM-fmap (f ∙ g) (deltaM d)) |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
67 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-fmap (f ∙ g) (deltaM d))) (covariant functorM g f x) ⟩ |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
68 appendDeltaM (deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x))) (deltaM-fmap (f ∙ g) (deltaM d)) |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
69 ≡⟨ refl ⟩ |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
70 appendDeltaM (deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x))) (deltaM-fmap (f ∙ g) (deltaM d)) |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
71 ≡⟨ refl ⟩ |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
72 appendDeltaM (deltaM (delta-fmap ((fmap functorM f) ∙ (fmap functorM g)) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d)) |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
73 ≡⟨ refl ⟩ |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
74 appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d)) |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
75 ≡⟨ cong (\de -> appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) de) (deltaM-covariant functorM f g (deltaM d)) ⟩ |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
76 appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) (((deltaM-fmap f) ∙ (deltaM-fmap g)) (deltaM d)) |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
77 ≡⟨ refl ⟩ |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
78 (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d)) |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
79 ∎ |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
80 |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
81 |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
82 deltaM-is-functor : {l : Level} {M : {l' : Level} -> Set l' -> Set l'} |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
83 {functorM : {l' : Level} -> Functor {l'} M } |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
84 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
85 -> Functor {l} (DeltaM M {functorM} {monadM}) |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
86 deltaM-is-functor {_} {_} {functorM} = record { fmap = deltaM-fmap ; |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
87 preserve-id = deltaM-preserve-id functorM ; |
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
88 covariant = (\f g -> deltaM-covariant functorM g f)} |