annotate agda/deltaM/functor.agda @ 110:cd058dd89864

Rewrite Functor-laws for DeltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 28 Jan 2015 22:36:34 +0900
parents ebd0d6e2772c
children 0a3b6cb91a05
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
9 open import nat
91
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import laws
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open Functor
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 module deltaM.functor where
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
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
16 deltaM-preserve-id : {l : Level} {A : Set l} {n : Nat}
91
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 {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
18 (functorM : {l' : Level} -> Functor {l'} M)
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 93
diff changeset
19 {monadM : {l' : Level} -> Monad {l'} M functorM}
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
20 -> (d : DeltaM M {functorM} {monadM} A (S n)) -> 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
21 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
22 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
23 deltaM (fmap delta-is-functor (fmap functorM id) (mono x)) ≡⟨ refl ⟩
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
24 deltaM (mono (fmap functorM id x)) ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id functorM x) ⟩
91
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 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
26 deltaM (mono x) ∎
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 deltaM-preserve-id functorM (deltaM (delta x d)) = begin
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
28 deltaM-fmap id (deltaM (delta x d))
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
29 ≡⟨ refl ⟩
92
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
30 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
31 ≡⟨ refl ⟩
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
32 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
33 ≡⟨ 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
34 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
35 ≡⟨ refl ⟩
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
36 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
37 ≡⟨ refl ⟩
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
38 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
39 ≡⟨ 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
40 appendDeltaM (deltaM (mono x)) (deltaM d)
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
41 ≡⟨ refl ⟩
91
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 deltaM (delta x d)
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
45
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
46 deltaM-covariant : {l : Level} {A B C : Set l} {n : Nat} ->
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
47 {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
48 (functorM : {l' : Level} -> Functor {l'} M)
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 93
diff changeset
49 {monadM : {l' : Level} -> Monad {l'} M functorM}
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
50 (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A (S n)) ->
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
51 (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
52 deltaM-covariant functorM f g (deltaM (mono x)) = begin
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
53 deltaM-fmap (f ∙ g) (deltaM (mono x)) ≡⟨ refl ⟩
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
54 deltaM (delta-fmap (fmap functorM (f ∙ g)) (mono x)) ≡⟨ refl ⟩
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
55 deltaM (mono (fmap functorM (f ∙ g) x)) ≡⟨ cong (\x -> (deltaM (mono x))) (covariant functorM g f x) ⟩
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
56 deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x)) ≡⟨ refl ⟩
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
57 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
58 deltaM-covariant functorM f g (deltaM (delta x d)) = begin
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
59 deltaM-fmap (f ∙ g) (deltaM (delta x d))
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
60 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
61 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
62 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
63 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
64 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
65 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
66 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
67 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
68 ≡⟨ 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
69 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
70 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
71 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
72 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
73 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
74 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
75 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
76 ≡⟨ 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
77 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
78 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
79 (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
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
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
83 deltaM-is-functor : {l : Level} {n : Nat}
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
84 {M : {l' : Level} -> Set l' -> Set l'}
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
85 {functorM : {l' : Level} -> Functor {l'} M }
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 93
diff changeset
86 {monadM : {l' : Level} -> Monad {l'} M functorM}
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
87 -> Functor {l} (\A -> DeltaM M {functorM} {monadM} A (S n))
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
88 deltaM-is-functor {_} {_} {_} {functorM} = record { fmap = deltaM-fmap ;
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
89 preserve-id = deltaM-preserve-id functorM ;
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
90 covariant = (\f g -> deltaM-covariant functorM g f)}