Mercurial > hg > Members > atton > delta_monad

annotate agda/deltaM/monad.agda @ 129:d57c88171f38

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove assciation-law for DeltaM on (S O)
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 12:42:28 +0900
parents d9a30f696933
children ac45d065cbf2
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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}
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
30 (f : A -> B) -> (x : (DeltaM M A (S n))) ->
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
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
35 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
36 {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
37 (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
38 (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
39 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
40 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
41
127
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
42 headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
43 {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
44 (x : DeltaM M A (S n)) ->
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
45 ((headDeltaM {n = n} {M = M}) ∙ deltaM-eta) x ≡ eta M x
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
46 headDeltaM-with-deltaM-eta {n = O} (deltaM (mono x)) = refl
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
47 headDeltaM-with-deltaM-eta {n = S n} (deltaM (delta x d)) = refl
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
48
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
49
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
50 fmap-tailDeltaM-with-deltaM-eta : {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
51 {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
52 (d : DeltaM M A (S n)) ->
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
53 deltaM-fmap ((tailDeltaM {n = n} {M = M} ) ∙ deltaM-eta) d ≡ deltaM-fmap (deltaM-eta) d
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
54 fmap-tailDeltaM-with-deltaM-eta {n = O} d = refl
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
55 fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
56
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
57
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
58
118
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
59 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
60 {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
61 (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
62 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
63 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
64 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
65
118
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
66
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
67 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
68 {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
69 (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
70 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
71 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
72 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
73
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
74
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
75
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
76
129
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
77 {-
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
78 -- main proofs
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
79
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
80 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
81 {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
82 (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
83 ((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
84 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
85 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
86 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
87 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
88 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
89 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
90 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
91 ≡⟨ refl ⟩
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
92 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
93 ≡⟨ refl ⟩
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
94 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
95 ≡⟨ 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
96 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
97 ≡⟨ 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
98 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
99 ≡⟨ refl ⟩
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
100 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
101 ∎
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
102
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
103
125
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
104
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
105
126
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
106 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
107 {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
108 (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
109 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
110 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
111 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
112 ≡⟨ refl ⟩
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
113 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
114 ≡⟨ refl ⟩
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
115 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
116 ≡⟨ 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
117 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
118 ≡⟨ 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
119 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
120 ≡⟨ 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
121 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
122 ≡⟨ 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
123 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
124 ≡⟨ refl ⟩
126
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
125 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
126 ≡⟨ refl ⟩
125
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
127 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
128 ≡⟨ refl ⟩
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
129 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
130 ∎
126
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
131 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
132 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
133 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
134 (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
135 ≡⟨ refl ⟩
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
136 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
137 (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
138 ≡⟨ refl ⟩
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
139 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
140 (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
141 ≡⟨ 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
142 (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
143 (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
144 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
145 (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
146 ≡⟨ 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
147 (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
148 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
149 (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
150 ≡⟨ 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
151 (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
152 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
153 (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
154 ≡⟨ refl ⟩
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
155 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
156 (unDeltaM {M = M} (deltaM-fmap f (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
157 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM de)))
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
158 (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
159 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
160 (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
161 ≡⟨ 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
162 (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
163 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
164 (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
165
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
166 ≡⟨ 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
167 (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
168 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
169 (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
170 ≡⟨ 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
171 (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
172 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
173 (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
174 ≡⟨ refl ⟩
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
175 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
176 (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
177 ≡⟨ 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
178 (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
179 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
180 (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
181 ≡⟨ refl ⟩
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
182 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
183 (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
184 ≡⟨ refl ⟩
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
185 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
186 ≡⟨ refl ⟩
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
187 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
188 ∎
129
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
189
125
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
190
126
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
191
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
192
127
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
193
125
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
194 deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat}
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
195 {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
196 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
197 deltaM-right-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
198 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
199 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
200 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
201 ≡⟨ 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
202 deltaM (mono (mu mm (eta mm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) (deltaM (mono x)))))) ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
203 deltaM (mono (mu mm (eta mm x))) ≡⟨ cong (\de -> deltaM (mono de)) (sym (right-unity-law mm x)) ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
204 deltaM (mono x)
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
205 ∎
125
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
206 deltaM-right-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
207 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
208 ≡⟨ refl ⟩
125
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
209 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
210 ≡⟨ refl ⟩
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
211 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
212 (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
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 (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
215 (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
216 ≡⟨ 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
217 (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
218 (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
219 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
220 (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
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 (mu M (eta M x))
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
223 (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
224 ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))))
125
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
225 (sym (right-unity-law M x)) ⟩
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-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
227 ≡⟨ refl ⟩
125
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
228 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
229 ≡⟨ 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
230 (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
231 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
232 ≡⟨ 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
233 (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
234 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
235 ≡⟨ refl ⟩
125
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
236 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
237 ≡⟨ refl ⟩
125
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
238 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-eta (deltaM d)))))
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
239 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-right-unity-law (deltaM d)) ⟩
6dcc68ef8f96 Prove right-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
240 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
241 ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
242 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
243 ∎
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
244
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
245
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
246
126
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
247
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
248
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
249
127
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
250 deltaM-left-unity-law : {l : Level} {A : Set l} {n : Nat}
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
251 {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
252 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
253 deltaM-left-unity-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = begin
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
254 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
255 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
256 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (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
257 deltaM (mono (mu M (fmap F (headDeltaM {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
258 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (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
259 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
260 ≡⟨ refl ⟩
127
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
261 deltaM (mono (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
262 ≡⟨ cong (\de -> deltaM (mono de)) (left-unity-law M x) ⟩
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
263 deltaM (mono x)
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
264 ∎
127
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
265 deltaM-left-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
266 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
267 ≡⟨ refl ⟩
127
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
268 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
269 ≡⟨ refl ⟩
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
270 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
271 (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
272 ≡⟨ refl ⟩
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
273 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
274 (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
275 ≡⟨ 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
276 (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
277 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
278 (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
279 ≡⟨ refl ⟩
127
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
280 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
281 (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
282 ≡⟨ cong (\de -> deltaM (delta 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
283 (left-unity-law M x) ⟩
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
284 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
285 ≡⟨ refl ⟩
127
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
286 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
287 ≡⟨ 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
288 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
289 ≡⟨ refl ⟩
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
290 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap deltaM-eta (deltaM d)))))
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
291 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-left-unity-law (deltaM d)) ⟩
d56596e4e784 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
292 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
293 ≡⟨ refl ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
294 deltaM (delta x d)
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
295 ∎
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
296
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
297 -}
115
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
298
129
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
299 postulate deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat}
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
300 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
301 (f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) ->
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
302 deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d)
115
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
303
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
304 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
305 {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
306 (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
307 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
308 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
309 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
310 ≡⟨ refl ⟩
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
311 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
312 ≡⟨ refl ⟩
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
313 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
314 ≡⟨ refl ⟩
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
315 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
316 ≡⟨ 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
317 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
318 ≡⟨ refl ⟩
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
319 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
320 ≡⟨ 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
321 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
322 ≡⟨ refl ⟩
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
323 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
324 ≡⟨ 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
325 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
326 ≡⟨ refl ⟩
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
327 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
328 ≡⟨ 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
329 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
330 ≡⟨ 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
331 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
332 ≡⟨ refl ⟩
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
333 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
334 ≡⟨ refl ⟩
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
335 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
336 ≡⟨ refl ⟩
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
337 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
338 ≡⟨ refl ⟩
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
339 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
340
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
341 ∎
d57c88171f38 Prove assciation-law for DeltaM on (S O)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
342 deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = {!!}
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
343 {-
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
344 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
345 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
346 ≡⟨ refl ⟩
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
347 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
348 ≡⟨ refl ⟩
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
349 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
350 (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
351
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
352 ≡⟨ refl ⟩
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 (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
354 (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
355 ≡⟨ 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
356 (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
357 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
358 (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
359 ≡⟨ 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
360 (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
361 (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
362 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
363 (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
364 ≡⟨ refl ⟩
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
365 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
366 (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
367 ≡⟨ 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
368 (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
369 (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
370 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
371 (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
372 ≡⟨ 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
373 (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
374 (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
375 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
376 (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 ≡⟨ 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
378 (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
379 (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
380 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
381 (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
382 ≡⟨ refl ⟩
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
383 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
384 (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
385 ≡⟨ 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
386 (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
387 (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
388
128
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 (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
390 (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
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 (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
393 (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
394 ≡⟨ 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
395 (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
396 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
397 (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
398 ≡⟨ 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
399 (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
400 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
401 (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
402 ≡⟨ 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
403 (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
404 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 (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
406 ≡⟨ refl ⟩
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 (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
409 ≡⟨ 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
410 (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
411 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
412 (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
413 ≡⟨ refl ⟩
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
414 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
415 (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
416 ≡⟨ 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
417 (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
418 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
419 (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
420
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
421 ≡⟨ 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
422 (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
423 (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
424 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
425 (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
426 ≡⟨ 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
427 (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
428 (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
429 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
430 (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
431 (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
432
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
433
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
434 ≡⟨ refl ⟩
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
435 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
436 (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
437 (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
438 (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
439
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
440
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
441 ≡⟨ refl ⟩
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
442 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
443 (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
444 ≡⟨ refl ⟩
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
445 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
446 (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
447 ≡⟨ refl ⟩
115
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
448 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
449 ∎
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
450 -}
115
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
451
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
452 {-
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
453
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
454 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat}
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
455 {M : Set l -> Set l}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
456 (functorM : Functor M)
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
457 (M : Monad M functorM) ->
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
458 Monad {l} (\A -> DeltaM M {functorM} {M} A (S n)) (deltaM-is-functor {l} {n})
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
459 deltaM-is-monad {l} {A} {n} {M} functorM M =
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
460 record { mu = deltaM-mu
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
461 ; eta = deltaM-eta
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
462 ; 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
463 ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x)))
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
464 ; association-law = (deltaM-association-law M functorM M)
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
465 ; left-unity-law = deltaM-left-unity-law
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
466 ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x)))
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
467 }
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
468
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
469
128
d9a30f696933 Fix association-law for DeltaM in (S n)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
470
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
471 -}