Mercurial > hg > Members > atton > delta_monad
annotate agda/deltaM/functor.agda @ 112:0a3b6cb91a05
Prove left-unity-law for DeltaM
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 30 Jan 2015 21:57:31 +0900 |
parents | cd058dd89864 |
children | 47f144540d51 |
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} |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
17 {M : Set l -> Set l} |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
18 (functorM : Functor M) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
19 {monadM : Monad 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} -> |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
47 {M : Set l -> Set l} |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
48 (functorM : Functor M) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
49 {monadM : Monad 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 |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
82 postulate deltaM-fmap-equiv : {l : Level} {A B : Set l} {n : Nat} |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
83 {M : Set l -> Set l} |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
84 {functorM : Functor M} |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
85 {monadM : Monad M functorM} |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
86 {f g : A -> B} |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
87 (eq : (x : A) -> f x ≡ g x) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
88 (d : DeltaM M {functorM} {monadM} A (S n)) -> |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
89 deltaM-fmap f d ≡ deltaM-fmap g d |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
90 {- |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
91 deltaM-fmap-equiv {n = O} f g eq (deltaM (mono x)) = begin |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
92 {!!} ≡⟨ {!!} ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
93 {!!} |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
94 ∎ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
95 deltaM-fmap-equiv {n = S n} f g eq d = {!!} |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
96 -} |
93
8d92ed54a94f
Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
92
diff
changeset
|
97 |
110
cd058dd89864
Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
98 deltaM-is-functor : {l : Level} {n : Nat} |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
99 {M : Set l -> Set l} |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
100 {functorM : Functor M } |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
101 {monadM : Monad M functorM} |
110
cd058dd89864
Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
102 -> 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
|
103 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
|
104 preserve-id = deltaM-preserve-id functorM ; |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
105 covariant = (\f g -> deltaM-covariant functorM g f); |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
106 fmap-equiv = deltaM-fmap-equiv |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
110
diff
changeset
|
107 } |