Mercurial > hg > Members > atton > delta_monad
annotate agda/deltaM/monad.agda @ 146:57601209eff3 default tip
Add an example used multi types on Delta
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 24 Mar 2015 17:04:00 +0900 |
parents | 575de2e38385 |
children |
rev | line source |
---|---|
98
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Level |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Relation.Binary.PropositionalEquality |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open ≡-Reasoning |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import basic |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import delta |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import delta.functor |
111
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
8 open import delta.monad |
98
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import deltaM |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 open import deltaM.functor |
104
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
11 open import nat |
98
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 open import laws |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 module deltaM.monad where |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 open Functor |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 open NaturalTransformation |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 open Monad |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 |
124
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
20 -- sub proofs |
114
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
21 |
117
6f86b55bf8b4
Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
116
diff
changeset
|
22 deconstruct-id : {l : Level} {A : Set l} {n : Nat} |
124
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
23 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> |
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
24 (d : DeltaM M A (S n)) -> deltaM (unDeltaM d) ≡ d |
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
25 deconstruct-id {n = O} (deltaM x) = refl |
117
6f86b55bf8b4
Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
116
diff
changeset
|
26 deconstruct-id {n = S n} (deltaM x) = refl |
6f86b55bf8b4
Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
116
diff
changeset
|
27 |
126
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
28 headDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat} |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
29 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} |
130
ac45d065cbf2
Prove all Monad-laws for Delta with Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
129
diff
changeset
|
30 (f : A -> B) -> (x : (DeltaM M A (S n))) -> |
126
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
31 ((fmap F f) ∙ headDeltaM) x ≡ (headDeltaM ∙ (deltaM-fmap f)) x |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
32 headDeltaM-with-f {n = O} f (deltaM (mono x)) = refl |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
33 headDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
34 |
131 | 35 |
126
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
36 tailDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat} |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
37 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
38 (f : A -> B) -> (d : (DeltaM M A (S (S n)))) -> |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
39 (tailDeltaM ∙ (deltaM-fmap f)) d ≡ ((deltaM-fmap f) ∙ tailDeltaM) d |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
40 tailDeltaM-with-f {n = O} f (deltaM (delta x d)) = refl |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
41 tailDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl |
117
6f86b55bf8b4
Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
116
diff
changeset
|
42 |
124
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
43 |
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
44 |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
45 fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat} |
124
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
46 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> |
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
47 (x : T (DeltaM M (DeltaM M A (S n)) (S n))) -> |
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
48 fmap F (headDeltaM ∙ deltaM-mu) x ≡ fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
49 fmap-headDeltaM-with-deltaM-mu {n = O} x = refl |
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
50 fmap-headDeltaM-with-deltaM-mu {n = S n} x = refl |
114
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
51 |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
52 |
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
53 fmap-tailDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat} |
124
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
54 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> |
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
55 (d : DeltaM M (DeltaM M (DeltaM M A (S (S n))) (S (S n))) (S n)) -> |
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
56 deltaM-fmap (tailDeltaM ∙ deltaM-mu) d ≡ deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) d |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
57 fmap-tailDeltaM-with-deltaM-mu {n = O} (deltaM (mono x)) = refl |
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
58 fmap-tailDeltaM-with-deltaM-mu {n = S n} (deltaM d) = refl |
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
59 |
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
60 |
117
6f86b55bf8b4
Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
116
diff
changeset
|
61 |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
62 |
130
ac45d065cbf2
Prove all Monad-laws for Delta with Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
129
diff
changeset
|
63 |
114
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
64 -- main proofs |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
65 |
124
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
66 deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat} |
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
67 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> |
114
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
68 (f : A -> B) -> (x : A) -> |
124
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
69 ((deltaM-eta {l} {B} {n} {T} {F} {M} )∙ f) x ≡ deltaM-fmap f (deltaM-eta x) |
114
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
70 deltaM-eta-is-nt {l} {A} {B} {O} {M} {fm} {mm} f x = begin |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
71 deltaM-eta {n = O} (f x) ≡⟨ refl ⟩ |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
72 deltaM (mono (eta mm (f x))) ≡⟨ cong (\de -> deltaM (mono de)) (eta-is-nt mm f x) ⟩ |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
73 deltaM (mono (fmap fm f (eta mm x))) ≡⟨ refl ⟩ |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
74 deltaM-fmap f (deltaM-eta {n = O} x) ∎ |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
75 deltaM-eta-is-nt {l} {A} {B} {S n} {M} {fm} {mm} f x = begin |
124
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
76 deltaM-eta {n = S n} (f x) |
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
77 ≡⟨ refl ⟩ |
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
78 deltaM (delta-eta {n = S n} (eta mm (f x))) |
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
79 ≡⟨ refl ⟩ |
114
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
80 deltaM (delta (eta mm (f x)) (delta-eta (eta mm (f x)))) |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
81 ≡⟨ cong (\de -> deltaM (delta de (delta-eta de))) (eta-is-nt mm f x) ⟩ |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
82 deltaM (delta (fmap fm f (eta mm x)) (delta-eta (fmap fm f (eta mm x)))) |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
83 ≡⟨ cong (\de -> deltaM (delta (fmap fm f (eta mm x)) de)) (eta-is-nt delta-is-monad (fmap fm f) (eta mm x)) ⟩ |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
84 deltaM (delta (fmap fm f (eta mm x)) (delta-fmap (fmap fm f) (delta-eta (eta mm x)))) |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
85 ≡⟨ refl ⟩ |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
86 deltaM-fmap f (deltaM-eta {n = S n} x) |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
87 ∎ |
124
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
88 |
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
89 |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
90 |
102
9c62373bd474
Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
98
diff
changeset
|
91 |
126
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
92 deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
93 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
94 (f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) -> |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
95 deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d) |
127
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
96 deltaM-mu-is-nt {l} {A} {B} {O} {T} {F} {M} f (deltaM (mono x)) = begin |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
97 deltaM-fmap f (deltaM-mu (deltaM (mono x))) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
98 ≡⟨ refl ⟩ |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
99 deltaM-fmap f (deltaM (mono (mu M (fmap F headDeltaM x)))) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
100 ≡⟨ refl ⟩ |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
101 deltaM (mono (fmap F f (mu M (fmap F headDeltaM x)))) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
102 ≡⟨ cong (\de -> deltaM (mono de)) (sym (mu-is-nt M f (fmap F headDeltaM x))) ⟩ |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
103 deltaM (mono (mu M (fmap F (fmap F f) (fmap F headDeltaM x)))) |
126
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
104 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F headDeltaM (fmap F f) x)) ⟩ |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
105 deltaM (mono (mu M (fmap F ((fmap F f) ∙ headDeltaM) x))) |
126
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
106 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (fmap-equiv F (headDeltaM-with-f f) x) ⟩ |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
107 deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
108 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F (deltaM-fmap f) (headDeltaM) x) ⟩ |
126
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
109 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x)))) |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
110 ≡⟨ refl ⟩ |
126
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
111 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x))))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
112 ≡⟨ refl ⟩ |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
113 deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x))) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
114 ≡⟨ refl ⟩ |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
115 deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (mono x))) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
116 ∎ |
126
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
117 deltaM-mu-is-nt {l} {A} {B} {S n} {T} {F} {M} f (deltaM (delta x d)) = begin |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
118 deltaM-fmap f (deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩ |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
119 deltaM-fmap f (deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta x d))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
120 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d)))))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
121 ≡⟨ refl ⟩ |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
122 deltaM-fmap f (deltaM (delta (mu M (fmap F (headDeltaM {M = M}) x)) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
123 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
124 ≡⟨ refl ⟩ |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
125 deltaM (delta (fmap F f (mu M (fmap F (headDeltaM {M = M}) x))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
126 (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
127 ≡⟨ cong (\de -> deltaM (delta de |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
128 (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
129 (sym (mu-is-nt M f (fmap F headDeltaM x))) ⟩ |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
130 deltaM (delta (mu M (fmap F (fmap F f) (fmap F (headDeltaM {M = M}) x))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
131 (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
132 ≡⟨ cong (\de -> deltaM (delta (mu M de) (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
133 (sym (covariant F headDeltaM (fmap F f) x)) ⟩ |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
134 deltaM (delta (mu M (fmap F ((fmap F f) ∙ (headDeltaM {M = M})) x)) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
135 (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
136 ≡⟨ cong (\de -> deltaM (delta (mu M de) (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
137 (fmap-equiv F (headDeltaM-with-f f) x) ⟩ |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
138 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
139 (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
140 ≡⟨ refl ⟩ |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
141 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
142 (unDeltaM {M = M} (deltaM-fmap f (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) |
130
ac45d065cbf2
Prove all Monad-laws for Delta with Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
129
diff
changeset
|
143 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM de))) |
126
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
144 (deltaM-mu-is-nt {l} {A} {B} {n} {T} {F} {M} f (deltaM-fmap tailDeltaM (deltaM d))) ⟩ |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
145 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
146 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (deltaM-fmap {n = n} f) (deltaM-fmap {n = n} (tailDeltaM {n = n}) (deltaM d)))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
147 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de)))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
148 (sym (deltaM-covariant (deltaM-fmap f) tailDeltaM (deltaM d))) ⟩ |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
149 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
150 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap {n = n} ((deltaM-fmap {n = n} f) ∙ (tailDeltaM {n = n})) (deltaM d))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
151 |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
152 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de)))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
153 (sym (deltaM-fmap-equiv (tailDeltaM-with-f f) (deltaM d))) ⟩ |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
154 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
155 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM ∙ (deltaM-fmap f)) (deltaM d))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
156 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de)))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
157 (deltaM-covariant tailDeltaM (deltaM-fmap f) (deltaM d)) ⟩ |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
158 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
159 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-fmap (deltaM-fmap f) (deltaM d)))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
160 ≡⟨ refl ⟩ |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
161 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
162 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d)))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
163 ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d))))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
164 (covariant F (deltaM-fmap f) headDeltaM x) ⟩ |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
165 deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
166 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d)))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
167 ≡⟨ refl ⟩ |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
168 deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d)))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
169 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d)))))))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
170 ≡⟨ refl ⟩ |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
171 deltaM-mu (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
172 ≡⟨ refl ⟩ |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
173 deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (delta x d))) |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
174 ∎ |
129
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
175 |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
176 |
126
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
177 |
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
178 |
127
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
179 |
144
575de2e38385
Fix names left/right unity law
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
131
diff
changeset
|
180 deltaM-left-unity-law : {l : Level} {A : Set l} {n : Nat} |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
181 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
182 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d |
144
575de2e38385
Fix names left/right unity law
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
131
diff
changeset
|
183 deltaM-left-unity-law {l} {A} {O} {M} {fm} {mm} (deltaM (mono x)) = begin |
111
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
184 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
185 deltaM-mu (deltaM (mono (eta mm (deltaM (mono x))))) ≡⟨ refl ⟩ |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
186 deltaM (mono (mu mm (fmap fm (headDeltaM {M = mm})(eta mm (deltaM (mono x)))))) |
111
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
187 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (eta-is-nt mm headDeltaM (deltaM (mono x)) )) ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
188 deltaM (mono (mu mm (eta mm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) (deltaM (mono x)))))) ≡⟨ refl ⟩ |
144
575de2e38385
Fix names left/right unity law
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
131
diff
changeset
|
189 deltaM (mono (mu mm (eta mm x))) ≡⟨ cong (\de -> deltaM (mono de)) (sym (left-unity-law mm x)) ⟩ |
111
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
190 deltaM (mono x) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
191 ∎ |
144
575de2e38385
Fix names left/right unity law
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
131
diff
changeset
|
192 deltaM-left-unity-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin |
111
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
193 deltaM-mu (deltaM-eta (deltaM (delta x d))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
194 ≡⟨ refl ⟩ |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
195 deltaM-mu (deltaM (delta (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d)))))) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
196 ≡⟨ refl ⟩ |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
197 deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta {l} {T (DeltaM M A (S (S n)))} {n} (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d))))))))) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
198 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d))))))))))) |
104
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
199 ≡⟨ refl ⟩ |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
200 deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (eta M (deltaM (delta x d))))) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
201 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
202 ≡⟨ cong (\de -> deltaM (delta (mu M de) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
203 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
204 (sym (eta-is-nt M headDeltaM (deltaM (delta x d)))) ⟩ |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
205 deltaM (delta (mu M (eta M (headDeltaM {M = M} (deltaM (delta x d))))) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
206 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))) |
111
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
207 ≡⟨ refl ⟩ |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
208 deltaM (delta (mu M (eta M x)) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
209 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))) |
126
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
210 ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))) |
144
575de2e38385
Fix names left/right unity law
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
131
diff
changeset
|
211 (sym (left-unity-law M x)) ⟩ |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
212 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))) |
126
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
213 ≡⟨ refl ⟩ |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
214 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-fmap (fmap F tailDeltaM) (delta-eta (eta M (deltaM (delta x d))))))))) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
215 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM de))))) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
216 (sym (delta-eta-is-nt (fmap F tailDeltaM) (eta M (deltaM (delta x d))))) ⟩ |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
217 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (fmap F tailDeltaM (eta M (deltaM (delta x d))))))))) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
218 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta de)))))) |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
219 (sym (eta-is-nt M tailDeltaM (deltaM (delta x d)))) ⟩ |
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
220 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (eta M (tailDeltaM (deltaM (delta x d))))))))) |
103
a271f3ff1922
Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
102
diff
changeset
|
221 ≡⟨ refl ⟩ |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
222 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (eta M (deltaM d))))))) |
111
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
223 ≡⟨ refl ⟩ |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
224 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-eta (deltaM d))))) |
144
575de2e38385
Fix names left/right unity law
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
131
diff
changeset
|
225 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-left-unity-law (deltaM d)) ⟩ |
125
6dcc68ef8f96
Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
124
diff
changeset
|
226 deltaM (delta x (unDeltaM {M = M} (deltaM d))) |
111
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
227 ≡⟨ refl ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
228 deltaM (delta x d) |
102
9c62373bd474
Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
98
diff
changeset
|
229 ∎ |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
230 |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
231 |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
232 |
126
5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
125
diff
changeset
|
233 |
104
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
234 |
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
235 |
144
575de2e38385
Fix names left/right unity law
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
131
diff
changeset
|
236 deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat} |
127
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
237 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
238 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d |
144
575de2e38385
Fix names left/right unity law
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
131
diff
changeset
|
239 deltaM-right-unity-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = begin |
127
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
240 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
241 deltaM-mu (deltaM (mono (fmap F deltaM-eta x))) ≡⟨ refl ⟩ |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
242 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-eta x))))))) ≡⟨ refl ⟩ |
130
ac45d065cbf2
Prove all Monad-laws for Delta with Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
129
diff
changeset
|
243 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-eta x)))) |
127
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
244 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-eta headDeltaM x)) ⟩ |
130
ac45d065cbf2
Prove all Monad-laws for Delta with Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
129
diff
changeset
|
245 deltaM (mono (mu M (fmap F ((headDeltaM {n = O} {M = M}) ∙ deltaM-eta) x))) |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
246 ≡⟨ refl ⟩ |
127
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
247 deltaM (mono (mu M (fmap F (eta M) x))) |
144
575de2e38385
Fix names left/right unity law
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
131
diff
changeset
|
248 ≡⟨ cong (\de -> deltaM (mono de)) (right-unity-law M x) ⟩ |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
249 deltaM (mono x) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
250 ∎ |
144
575de2e38385
Fix names left/right unity law
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
131
diff
changeset
|
251 deltaM-right-unity-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
252 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (delta x d))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
253 ≡⟨ refl ⟩ |
127
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
254 deltaM-mu (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d))) |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
255 ≡⟨ refl ⟩ |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
256 deltaM (delta (mu M (fmap F (headDeltaM {n = S n} {M = M}) (headDeltaM {n = S n} {M = M} (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d)))))) |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
257 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d)))))))) |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
258 ≡⟨ refl ⟩ |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
259 deltaM (delta (mu M (fmap F (headDeltaM {n = S n} {M = M}) (fmap F deltaM-eta x))) |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
260 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d)))))) |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
261 ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))) |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
262 (sym (covariant F deltaM-eta headDeltaM x)) ⟩ |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
263 deltaM (delta (mu M (fmap F ((headDeltaM {n = S n} {M = M}) ∙ deltaM-eta) x)) |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
264 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d)))))) |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
265 ≡⟨ refl ⟩ |
127
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
266 deltaM (delta (mu M (fmap F (eta M) x)) |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
267 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d)))))) |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
268 ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))) |
144
575de2e38385
Fix names left/right unity law
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
131
diff
changeset
|
269 (right-unity-law M x) ⟩ |
127
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
270 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d)))))) |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
271 ≡⟨ refl ⟩ |
127
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
272 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM {n = n})(deltaM-fmap (deltaM-eta {n = S n})(deltaM d)))))) |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
273 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu de)))) (sym (deltaM-covariant tailDeltaM deltaM-eta (deltaM d))) ⟩ |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
274 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((tailDeltaM {n = n}) ∙ (deltaM-eta {n = S n})) (deltaM d))))) |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
275 ≡⟨ refl ⟩ |
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
276 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap deltaM-eta (deltaM d))))) |
144
575de2e38385
Fix names left/right unity law
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
131
diff
changeset
|
277 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-right-unity-law (deltaM d)) ⟩ |
127
d56596e4e784
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
126
diff
changeset
|
278 deltaM (delta x (unDeltaM {M = M} (deltaM d))) |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
279 ≡⟨ refl ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
280 deltaM (delta x d) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
281 ∎ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
282 |
115
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
283 deltaM-association-law : {l : Level} {A : Set l} {n : Nat} |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
284 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
285 (d : DeltaM M (DeltaM M (DeltaM M A (S n)) (S n)) (S n)) -> |
115
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
286 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d) |
129
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
287 deltaM-association-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = begin |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
288 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
289 ≡⟨ refl ⟩ |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
290 deltaM-mu (deltaM (mono (fmap F deltaM-mu x))) |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
291 ≡⟨ refl ⟩ |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
292 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-mu x))))))) |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
293 ≡⟨ refl ⟩ |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
294 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-mu x)))) |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
295 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-mu headDeltaM x)) ⟩ |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
296 deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ deltaM-mu) x))) |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
297 ≡⟨ refl ⟩ |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
298 deltaM (mono (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))) |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
299 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F headDeltaM ((mu M) ∙ (fmap F headDeltaM)) x) ⟩ |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
300 deltaM (mono (mu M ((((fmap F (((mu M) ∙ (fmap F headDeltaM)))) ∙ (fmap F headDeltaM)) x)))) |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
301 ≡⟨ refl ⟩ |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
302 deltaM (mono (mu M ((((fmap F (((mu M) ∙ (fmap F headDeltaM)))) (fmap F headDeltaM x)))))) |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
303 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F (fmap F headDeltaM) (mu M) (fmap F headDeltaM x)) ⟩ |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
304 deltaM (mono (mu M (((fmap F (mu M)) ∙ (fmap F (fmap F headDeltaM))) (fmap F headDeltaM x)))) |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
305 ≡⟨ refl ⟩ |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
306 deltaM (mono (mu M (fmap F (mu M) ((fmap F (fmap F headDeltaM) (fmap F headDeltaM x)))))) |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
307 ≡⟨ cong (\de -> deltaM (mono de)) (association-law M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))) ⟩ |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
308 deltaM (mono (mu M (mu M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))))) |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
309 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (mu-is-nt M headDeltaM (fmap F headDeltaM x)) ⟩ |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
310 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (mu M (fmap F (headDeltaM {M = M}) x))))) |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
311 ≡⟨ refl ⟩ |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
312 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x)))))))) |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
313 ≡⟨ refl ⟩ |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
314 deltaM-mu (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x)))) |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
315 ≡⟨ refl ⟩ |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
316 deltaM-mu (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono x))))))) |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
317 ≡⟨ refl ⟩ |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
318 deltaM-mu (deltaM-mu (deltaM (mono x))) |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
319 |
d57c88171f38
Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
320 ∎ |
130
ac45d065cbf2
Prove all Monad-laws for Delta with Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
129
diff
changeset
|
321 |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
322 deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
323 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d))) |
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
324 ≡⟨ refl ⟩ |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
325 deltaM-mu (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d))) |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
326 ≡⟨ refl ⟩ |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
327 deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d)))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
328 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d)))))))) |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
329 |
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
330 ≡⟨ refl ⟩ |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
331 deltaM (delta (mu M (fmap F (headDeltaM {A = A} {M = M}) (fmap F deltaM-mu x))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
332 (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d)))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
333 ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d))))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
334 (sym (covariant F deltaM-mu headDeltaM x)) ⟩ |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
335 deltaM (delta (mu M (fmap F ((headDeltaM {A = A} {M = M}) ∙ deltaM-mu) x)) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
336 (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d)))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
337 ≡⟨ cong (\de -> deltaM (delta (mu M de) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
338 (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d))))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
339 (fmap-headDeltaM-with-deltaM-mu {A = A} {M = M} x) ⟩ |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
340 deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x)) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
341 (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d)))))) |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
342 ≡⟨ refl ⟩ |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
343 deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x)) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
344 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-fmap deltaM-mu (deltaM d)))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
345 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x)) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
346 (unDeltaM {M = M} (deltaM-mu de)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
347 (sym (deltaM-covariant tailDeltaM deltaM-mu (deltaM d))) ⟩ |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
348 deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x)) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
349 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM ∙ deltaM-mu) (deltaM d))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
350 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x)) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
351 (unDeltaM {M = M} (deltaM-mu de)))) |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
352 (fmap-tailDeltaM-with-deltaM-mu (deltaM d)) ⟩ |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
353 deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x)) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
354 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
355 ≡⟨ cong (\de -> deltaM (delta (mu M de) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
356 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
357 (covariant F headDeltaM ((mu M) ∙ (fmap F headDeltaM)) x) ⟩ |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
358 deltaM (delta (mu M (((fmap F ((mu M) ∙ (fmap F headDeltaM))) ∙ (fmap F headDeltaM)) x)) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
359 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))) |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
360 ≡⟨ refl ⟩ |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
361 deltaM (delta (mu M (((fmap F ((mu M) ∙ (fmap F headDeltaM))) (fmap F headDeltaM x)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
362 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
363 ≡⟨ cong (\de -> deltaM (delta (mu M de) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
364 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
365 (covariant F (fmap F headDeltaM) (mu M) (fmap F headDeltaM x)) ⟩ |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
366 |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
367 deltaM (delta (mu M ((((fmap F (mu M)) ∙ (fmap F (fmap F headDeltaM))) (fmap F headDeltaM x)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
368 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))) |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
369 ≡⟨ refl ⟩ |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
370 deltaM (delta (mu M (fmap F (mu M) (fmap F (fmap F headDeltaM) (fmap F headDeltaM x)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
371 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
372 ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
373 (association-law M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))) ⟩ |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
374 deltaM (delta (mu M (mu M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
375 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
376 ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
377 (mu-is-nt M headDeltaM (fmap F headDeltaM x)) ⟩ |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
378 deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
379 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
380 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) (unDeltaM {M = M} (deltaM-mu de)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
381 (deltaM-covariant (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) tailDeltaM (deltaM d)) ⟩ |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
382 deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
383 (unDeltaM {M = M} (deltaM-mu (((deltaM-fmap (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ (deltaM-fmap tailDeltaM)) (deltaM d)))))) |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
384 ≡⟨ refl ⟩ |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
385 deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
386 (unDeltaM {M = M} (deltaM-mu (((deltaM-fmap (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) (deltaM-fmap tailDeltaM (deltaM d)))))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
387 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) (unDeltaM {M = M} (deltaM-mu de)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
388 (deltaM-covariant deltaM-mu (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d))) ⟩ |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
389 deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
390 (unDeltaM {M = M} (deltaM-mu (((deltaM-fmap deltaM-mu) ∙ (deltaM-fmap (deltaM-fmap tailDeltaM))) (deltaM-fmap tailDeltaM (deltaM d)))))) |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
391 ≡⟨ refl ⟩ |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
392 deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
393 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap deltaM-mu (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d))))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
394 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) (unDeltaM {M = M} de))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
395 (deltaM-association-law (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))) ⟩ |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
396 deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
397 (unDeltaM {M = M} (deltaM-mu (deltaM-mu (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d))))))) |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
398 |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
399 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
400 (unDeltaM {M = M} (deltaM-mu de)))) |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
401 (sym (deltaM-mu-is-nt tailDeltaM (deltaM-fmap tailDeltaM (deltaM d)))) ⟩ |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
402 deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
403 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
404 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
405 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM de))))) |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
406 (sym (deconstruct-id (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))) ⟩ |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
407 deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
408 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
409 (deltaM (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))))) |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
410 |
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
411 |
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
412 ≡⟨ refl ⟩ |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
413 deltaM (delta (mu M (fmap F headDeltaM (headDeltaM {M = M} ((deltaM (delta (mu M (fmap F headDeltaM x)) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
414 (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
415 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM ((deltaM (delta (mu M (fmap F headDeltaM x)) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
416 (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))))))) |
118
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
417 |
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
418 |
53cb21845dea
Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
117
diff
changeset
|
419 ≡⟨ refl ⟩ |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
420 deltaM-mu (deltaM (delta (mu M (fmap F headDeltaM x)) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
421 (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) |
117
6f86b55bf8b4
Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
116
diff
changeset
|
422 ≡⟨ refl ⟩ |
128
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
423 deltaM-mu (deltaM (delta (mu M (fmap F headDeltaM (headDeltaM {M = M} (deltaM (delta x d))))) |
d9a30f696933
Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
127
diff
changeset
|
424 (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d)))))))) |
117
6f86b55bf8b4
Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
116
diff
changeset
|
425 ≡⟨ refl ⟩ |
115
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
426 deltaM-mu (deltaM-mu (deltaM (delta x d))) |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
427 ∎ |
130
ac45d065cbf2
Prove all Monad-laws for Delta with Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
129
diff
changeset
|
428 |
115
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
429 |
130
ac45d065cbf2
Prove all Monad-laws for Delta with Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
129
diff
changeset
|
430 |
104
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
431 |
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
432 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} |
130
ac45d065cbf2
Prove all Monad-laws for Delta with Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
129
diff
changeset
|
433 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> |
ac45d065cbf2
Prove all Monad-laws for Delta with Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
129
diff
changeset
|
434 Monad {l} (\A -> DeltaM M A (S n)) (deltaM-is-functor {l} {n}) |
ac45d065cbf2
Prove all Monad-laws for Delta with Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
129
diff
changeset
|
435 deltaM-is-monad {l} {A} {n} {T} {F} {M} = |
124
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
436 record { mu = deltaM-mu |
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
437 ; eta = deltaM-eta |
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
438 ; eta-is-nt = deltaM-eta-is-nt |
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
439 ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x))) |
130
ac45d065cbf2
Prove all Monad-laws for Delta with Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
129
diff
changeset
|
440 ; association-law = deltaM-association-law |
144
575de2e38385
Fix names left/right unity law
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
131
diff
changeset
|
441 ; right-unity-law = deltaM-right-unity-law |
575de2e38385
Fix names left/right unity law
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
131
diff
changeset
|
442 ; left-unity-law = (\x -> (sym (deltaM-left-unity-law x))) |
124
48b44bd85056
Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
118
diff
changeset
|
443 } |