Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/monad.agda @ 144:575de2e38385

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix names left/right unity law
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 25 Feb 2015 14:49:50 +0900
parents d205ff1e406f
children
comparison
equal deleted inserted replaced
143:f241d521bf65 144:575de2e38385
175 175
176 176
177 177
178 178
179 179
180 deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat} 180 deltaM-left-unity-law : {l : Level} {A : Set l} {n : Nat}
181 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> 181 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
182 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d 182 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d
183 deltaM-right-unity-law {l} {A} {O} {M} {fm} {mm} (deltaM (mono x)) = begin 183 deltaM-left-unity-law {l} {A} {O} {M} {fm} {mm} (deltaM (mono x)) = begin
184 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ 184 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
185 deltaM-mu (deltaM (mono (eta mm (deltaM (mono x))))) ≡⟨ refl ⟩ 185 deltaM-mu (deltaM (mono (eta mm (deltaM (mono x))))) ≡⟨ refl ⟩
186 deltaM (mono (mu mm (fmap fm (headDeltaM {M = mm})(eta mm (deltaM (mono x)))))) 186 deltaM (mono (mu mm (fmap fm (headDeltaM {M = mm})(eta mm (deltaM (mono x))))))
187 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (eta-is-nt mm headDeltaM (deltaM (mono x)) )) ⟩ 187 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (eta-is-nt mm headDeltaM (deltaM (mono x)) )) ⟩
188 deltaM (mono (mu mm (eta mm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) (deltaM (mono x)))))) ≡⟨ refl ⟩ 188 deltaM (mono (mu mm (eta mm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) (deltaM (mono x)))))) ≡⟨ refl ⟩
189 deltaM (mono (mu mm (eta mm x))) ≡⟨ cong (\de -> deltaM (mono de)) (sym (right-unity-law mm x)) ⟩ 189 deltaM (mono (mu mm (eta mm x))) ≡⟨ cong (\de -> deltaM (mono de)) (sym (left-unity-law mm x)) ⟩
190 deltaM (mono x) 190 deltaM (mono x)
191 ∎ 191 ∎
192 deltaM-right-unity-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin 192 deltaM-left-unity-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
193 deltaM-mu (deltaM-eta (deltaM (delta x d))) 193 deltaM-mu (deltaM-eta (deltaM (delta x d)))
194 ≡⟨ refl ⟩ 194 ≡⟨ refl ⟩
195 deltaM-mu (deltaM (delta (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d)))))) 195 deltaM-mu (deltaM (delta (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d))))))
196 ≡⟨ refl ⟩ 196 ≡⟨ refl ⟩
197 deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta {l} {T (DeltaM M A (S (S n)))} {n} (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d))))))))) 197 deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta {l} {T (DeltaM M A (S (S n)))} {n} (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d)))))))))
206 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))) 206 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
207 ≡⟨ refl ⟩ 207 ≡⟨ refl ⟩
208 deltaM (delta (mu M (eta M x)) 208 deltaM (delta (mu M (eta M x))
209 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))) 209 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
210 ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))) 210 ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))))
211 (sym (right-unity-law M x)) ⟩ 211 (sym (left-unity-law M x)) ⟩
212 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))) 212 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
213 ≡⟨ refl ⟩ 213 ≡⟨ refl ⟩
214 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-fmap (fmap F tailDeltaM) (delta-eta (eta M (deltaM (delta x d))))))))) 214 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-fmap (fmap F tailDeltaM) (delta-eta (eta M (deltaM (delta x d)))))))))
215 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM de))))) 215 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM de)))))
216 (sym (delta-eta-is-nt (fmap F tailDeltaM) (eta M (deltaM (delta x d))))) ⟩ 216 (sym (delta-eta-is-nt (fmap F tailDeltaM) (eta M (deltaM (delta x d))))) ⟩
220 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (eta M (tailDeltaM (deltaM (delta x d))))))))) 220 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (eta M (tailDeltaM (deltaM (delta x d)))))))))
221 ≡⟨ refl ⟩ 221 ≡⟨ refl ⟩
222 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (eta M (deltaM d))))))) 222 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (eta M (deltaM d)))))))
223 ≡⟨ refl ⟩ 223 ≡⟨ refl ⟩
224 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-eta (deltaM d))))) 224 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-eta (deltaM d)))))
225 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-right-unity-law (deltaM d)) ⟩ 225 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-left-unity-law (deltaM d)) ⟩
226 deltaM (delta x (unDeltaM {M = M} (deltaM d))) 226 deltaM (delta x (unDeltaM {M = M} (deltaM d)))
227 ≡⟨ refl ⟩ 227 ≡⟨ refl ⟩
228 deltaM (delta x d) 228 deltaM (delta x d)
229 ∎ 229 ∎
230 230
231 231
232 232
233 233
234 234
235 235
236 deltaM-left-unity-law : {l : Level} {A : Set l} {n : Nat} 236 deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat}
237 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} 237 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
238 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d 238 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d
239 deltaM-left-unity-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = begin 239 deltaM-right-unity-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = begin
240 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ 240 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
241 deltaM-mu (deltaM (mono (fmap F deltaM-eta x))) ≡⟨ refl ⟩ 241 deltaM-mu (deltaM (mono (fmap F deltaM-eta x))) ≡⟨ refl ⟩
242 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-eta x))))))) ≡⟨ refl ⟩ 242 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-eta x))))))) ≡⟨ refl ⟩
243 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-eta x)))) 243 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-eta x))))
244 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-eta headDeltaM x)) ⟩ 244 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-eta headDeltaM x)) ⟩
245 deltaM (mono (mu M (fmap F ((headDeltaM {n = O} {M = M}) ∙ deltaM-eta) x))) 245 deltaM (mono (mu M (fmap F ((headDeltaM {n = O} {M = M}) ∙ deltaM-eta) x)))
246 ≡⟨ refl ⟩ 246 ≡⟨ refl ⟩
247 deltaM (mono (mu M (fmap F (eta M) x))) 247 deltaM (mono (mu M (fmap F (eta M) x)))
248 ≡⟨ cong (\de -> deltaM (mono de)) (left-unity-law M x) ⟩ 248 ≡⟨ cong (\de -> deltaM (mono de)) (right-unity-law M x) ⟩
249 deltaM (mono x) 249 deltaM (mono x)
250 ∎ 250 ∎
251 deltaM-left-unity-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin 251 deltaM-right-unity-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
252 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (delta x d))) 252 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (delta x d)))
253 ≡⟨ refl ⟩ 253 ≡⟨ refl ⟩
254 deltaM-mu (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d))) 254 deltaM-mu (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d)))
255 ≡⟨ refl ⟩ 255 ≡⟨ refl ⟩
256 deltaM (delta (mu M (fmap F (headDeltaM {n = S n} {M = M}) (headDeltaM {n = S n} {M = M} (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d)))))) 256 deltaM (delta (mu M (fmap F (headDeltaM {n = S n} {M = M}) (headDeltaM {n = S n} {M = M} (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d))))))
264 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d)))))) 264 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
265 ≡⟨ refl ⟩ 265 ≡⟨ refl ⟩
266 deltaM (delta (mu M (fmap F (eta M) x)) 266 deltaM (delta (mu M (fmap F (eta M) x))
267 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d)))))) 267 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
268 ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))) 268 ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d)))))))
269 (left-unity-law M x) ⟩ 269 (right-unity-law M x) ⟩
270 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d)))))) 270 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
271 ≡⟨ refl ⟩ 271 ≡⟨ refl ⟩
272 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM {n = n})(deltaM-fmap (deltaM-eta {n = S n})(deltaM d)))))) 272 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM {n = n})(deltaM-fmap (deltaM-eta {n = S n})(deltaM d))))))
273 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu de)))) (sym (deltaM-covariant tailDeltaM deltaM-eta (deltaM d))) ⟩ 273 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu de)))) (sym (deltaM-covariant tailDeltaM deltaM-eta (deltaM d))) ⟩
274 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((tailDeltaM {n = n}) ∙ (deltaM-eta {n = S n})) (deltaM d))))) 274 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((tailDeltaM {n = n}) ∙ (deltaM-eta {n = S n})) (deltaM d)))))
275 ≡⟨ refl ⟩ 275 ≡⟨ refl ⟩
276 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap deltaM-eta (deltaM d))))) 276 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap deltaM-eta (deltaM d)))))
277 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-left-unity-law (deltaM d)) ⟩ 277 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-right-unity-law (deltaM d)) ⟩
278 deltaM (delta x (unDeltaM {M = M} (deltaM d))) 278 deltaM (delta x (unDeltaM {M = M} (deltaM d)))
279 ≡⟨ refl ⟩ 279 ≡⟨ refl ⟩
280 deltaM (delta x d) 280 deltaM (delta x d)
281 ∎ 281 ∎
282 282
436 record { mu = deltaM-mu 436 record { mu = deltaM-mu
437 ; eta = deltaM-eta 437 ; eta = deltaM-eta
438 ; eta-is-nt = deltaM-eta-is-nt 438 ; eta-is-nt = deltaM-eta-is-nt
439 ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x))) 439 ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x)))
440 ; association-law = deltaM-association-law 440 ; association-law = deltaM-association-law
441 ; left-unity-law = deltaM-left-unity-law 441 ; right-unity-law = deltaM-right-unity-law
442 ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) 442 ; left-unity-law = (\x -> (sym (deltaM-left-unity-law x)))
443 } 443 }