Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/monad.agda @ 126:5902b2a24abf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove mu-is-nt for DeltaM with fmap-equiv
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 11:45:33 +0900
parents 6dcc68ef8f96
children d56596e4e784
comparison
equal deleted inserted replaced
125:6dcc68ef8f96 126:5902b2a24abf
23 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> 23 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
24 (d : DeltaM M A (S n)) -> deltaM (unDeltaM d) ≡ d 24 (d : DeltaM M A (S n)) -> deltaM (unDeltaM d) ≡ d
25 deconstruct-id {n = O} (deltaM x) = refl 25 deconstruct-id {n = O} (deltaM x) = refl
26 deconstruct-id {n = S n} (deltaM x) = refl 26 deconstruct-id {n = S n} (deltaM x) = refl
27 27
28 headDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat}
29 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
30 (f : A -> B) -> (x : (DeltaM M A (S n))) ->
31 ((fmap F f) ∙ headDeltaM) x ≡ (headDeltaM ∙ (deltaM-fmap f)) x
32 headDeltaM-with-f {n = O} f (deltaM (mono x)) = refl
33 headDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl
34
35 tailDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat}
36 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
37 (f : A -> B) -> (d : (DeltaM M A (S (S n)))) ->
38 (tailDeltaM ∙ (deltaM-fmap f)) d ≡ ((deltaM-fmap f) ∙ tailDeltaM) d
39 tailDeltaM-with-f {n = O} f (deltaM (delta x d)) = refl
40 tailDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl
28 41
29 42
30 fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} 43 fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
31 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> 44 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
32 (x : T A) -> (fmap F ((headDeltaM {n = n} {M = M}) ∙ deltaM-eta) x) ≡ fmap F (eta M) x 45 (x : T A) -> (fmap F ((headDeltaM {n = n} {M = M}) ∙ deltaM-eta) x) ≡ fmap F (eta M) x
89 ∎ 102 ∎
90 103
91 104
92 105
93 106
94 postulate deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} 107 deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat}
95 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} 108 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
96 (f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) -> 109 (f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) ->
97 deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d) 110 deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d)
111 deltaM-mu-is-nt {l} {A} {B} {O} {T} {F} {M} f (deltaM (mono x)) =
98 {- 112 {-
99 deltaM-mu-is-nt {l} {A} {B} {O} {T} {F} {M} f (deltaM (mono x)) = begin 113 deltaM-mu-is-nt {l} {A} {B} {O} {T} {F} {M} f (deltaM (mono x)) = begin
114 deltaM-fmap f (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩
115 deltaM-fmap f (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono x))))))) ≡⟨ refl ⟩
116 deltaM-fmap f (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x)))) ≡⟨ refl ⟩
117 deltaM (mono (fmap F f (mu M (fmap F (headDeltaM {M = M}) x)))) ≡⟨ {!!} ⟩
118 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x)))) ≡⟨ refl ⟩
119 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x))))))) ≡⟨ refl ⟩
120 deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x))) ≡⟨ refl ⟩
121 deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x))) ≡⟨ refl ⟩
122 deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (mono x)))
123 ∎
124 -}
125
126 begin
100 deltaM-fmap f (deltaM-mu (deltaM (mono x))) 127 deltaM-fmap f (deltaM-mu (deltaM (mono x)))
101 ≡⟨ refl ⟩ 128 ≡⟨ refl ⟩
102 deltaM-fmap f (deltaM (mono (mu M (fmap F headDeltaM x)))) 129 deltaM-fmap f (deltaM (mono (mu M (fmap F headDeltaM x))))
103 ≡⟨ refl ⟩ 130 ≡⟨ refl ⟩
104 deltaM (mono (fmap F f (mu M (fmap F headDeltaM x)))) 131 deltaM (mono (fmap F f (mu M (fmap F headDeltaM x))))
105 ≡⟨ cong (\de -> deltaM (mono de)) (sym (mu-is-nt M f (fmap F headDeltaM x))) ⟩ 132 ≡⟨ cong (\de -> deltaM (mono de)) (sym (mu-is-nt M f (fmap F headDeltaM x))) ⟩
106 deltaM (mono (mu M (fmap F (fmap F f) (fmap F headDeltaM x)))) 133 deltaM (mono (mu M (fmap F (fmap F f) (fmap F headDeltaM x))))
107 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F headDeltaM (fmap F f) x)) ⟩ 134 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F headDeltaM (fmap F f) x)) ⟩
108 deltaM (mono (mu M (fmap F ((fmap F f) ∙ headDeltaM) x))) 135 deltaM (mono (mu M (fmap F ((fmap F f) ∙ headDeltaM) x)))
109 ≡⟨ {!!} ⟩ 136 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (fmap-equiv F (headDeltaM-with-f f) x) ⟩
110 deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)))
111 ≡⟨ {!!} ⟩
112 deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))) 137 deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)))
113 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F (deltaM-fmap f) (headDeltaM) x) ⟩ 138 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F (deltaM-fmap f) (headDeltaM) x) ⟩
114 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x)))) 139 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x))))
115 ≡⟨ refl ⟩ 140 ≡⟨ refl ⟩
116 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x))))))) 141 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x)))))))
117 ≡⟨ refl ⟩ 142 ≡⟨ refl ⟩
118 deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x))) 143 deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x)))
119 ≡⟨ refl ⟩ 144 ≡⟨ refl ⟩
120 deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (mono x))) 145 deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (mono x)))
121 ∎ 146 ∎
122 deltaM-mu-is-nt {n = S n} f (deltaM (delta x d)) = {!!} 147
123 148 deltaM-mu-is-nt {l} {A} {B} {S n} {T} {F} {M} f (deltaM (delta x d)) = begin
124 -} 149 deltaM-fmap f (deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩
125 150 deltaM-fmap f (deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta x d)))))
126 151 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d))))))))
152 ≡⟨ refl ⟩
153 deltaM-fmap f (deltaM (delta (mu M (fmap F (headDeltaM {M = M}) x))
154 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
155 ≡⟨ refl ⟩
156 deltaM (delta (fmap F f (mu M (fmap F (headDeltaM {M = M}) x)))
157 (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
158 ≡⟨ cong (\de -> deltaM (delta de
159 (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
160 (sym (mu-is-nt M f (fmap F headDeltaM x))) ⟩
161 deltaM (delta (mu M (fmap F (fmap F f) (fmap F (headDeltaM {M = M}) x)))
162 (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
163 ≡⟨ cong (\de -> deltaM (delta (mu M de) (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
164 (sym (covariant F headDeltaM (fmap F f) x)) ⟩
165 deltaM (delta (mu M (fmap F ((fmap F f) ∙ (headDeltaM {M = M})) x))
166 (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
167 ≡⟨ cong (\de -> deltaM (delta (mu M de) (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
168 (fmap-equiv F (headDeltaM-with-f f) x) ⟩
169 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
170 (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
171 ≡⟨ refl ⟩
172 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
173 (unDeltaM {M = M} (deltaM-fmap f (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
174 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM de)))
175 (deltaM-mu-is-nt {l} {A} {B} {n} {T} {F} {M} f (deltaM-fmap tailDeltaM (deltaM d))) ⟩
176 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
177 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (deltaM-fmap {n = n} f) (deltaM-fmap {n = n} (tailDeltaM {n = n}) (deltaM d))))))
178 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de))))
179 (sym (deltaM-covariant (deltaM-fmap f) tailDeltaM (deltaM d))) ⟩
180 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
181 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap {n = n} ((deltaM-fmap {n = n} f) ∙ (tailDeltaM {n = n})) (deltaM d)))))
182
183 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de))))
184 (sym (deltaM-fmap-equiv (tailDeltaM-with-f f) (deltaM d))) ⟩
185 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
186 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM ∙ (deltaM-fmap f)) (deltaM d)))))
187 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de))))
188 (deltaM-covariant tailDeltaM (deltaM-fmap f) (deltaM d)) ⟩
189 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
190 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-fmap (deltaM-fmap f) (deltaM d))))))
191 ≡⟨ refl ⟩
192 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
193 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d))))))
194 ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d)))))))
195 (covariant F (deltaM-fmap f) headDeltaM x) ⟩
196 deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x)))
197 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d))))))
198 ≡⟨ refl ⟩
199 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))))))
200 (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))))))))
201 ≡⟨ refl ⟩
202 deltaM-mu (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d)))
203 ≡⟨ refl ⟩
204 deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (delta x d)))
205 ∎
206
207
208
209
210 {-
127 deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat} 211 deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat}
128 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> 212 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
129 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d 213 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d
130 deltaM-right-unity-law {l} {A} {O} {M} {fm} {mm} (deltaM (mono x)) = begin 214 deltaM-right-unity-law {l} {A} {O} {M} {fm} {mm} (deltaM (mono x)) = begin
131 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ 215 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
152 deltaM (delta (mu M (eta M (headDeltaM {M = M} (deltaM (delta x d))))) 236 deltaM (delta (mu M (eta M (headDeltaM {M = M} (deltaM (delta x d)))))
153 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))) 237 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
154 ≡⟨ refl ⟩ 238 ≡⟨ refl ⟩
155 deltaM (delta (mu M (eta M x)) 239 deltaM (delta (mu M (eta M x))
156 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))) 240 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
157 ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))) 241 ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))))
158 (sym (right-unity-law M x)) ⟩ 242 (sym (right-unity-law M x)) ⟩
159 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))) 243 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
160 ≡⟨ refl ⟩ 244 ≡⟨ refl ⟩
161 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-fmap (fmap F tailDeltaM) (delta-eta (eta M (deltaM (delta x d))))))))) 245 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-fmap (fmap F tailDeltaM) (delta-eta (eta M (deltaM (delta x d)))))))))
162 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM de))))) 246 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM de)))))
163 (sym (delta-eta-is-nt (fmap F tailDeltaM) (eta M (deltaM (delta x d))))) ⟩ 247 (sym (delta-eta-is-nt (fmap F tailDeltaM) (eta M (deltaM (delta x d))))) ⟩
164 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (fmap F tailDeltaM (eta M (deltaM (delta x d))))))))) 248 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (fmap F tailDeltaM (eta M (deltaM (delta x d)))))))))
165 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta de)))))) 249 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta de))))))
175 deltaM (delta x d) 259 deltaM (delta x d)
176 ∎ 260 ∎
177 261
178 262
179 263
180 {- 264
181 265
182 266
183 postulate deltaM-left-unity-law : {l : Level} {A : Set l} 267 postulate deltaM-left-unity-law : {l : Level} {A : Set l}
184 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} 268 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM}
185 {n : Nat} 269 {n : Nat}