### comparison agda/deltaM/monad.agda @ 128:d9a30f696933

Fix association-law for DeltaM in (S n)
author Yasutaka Higa Tue, 03 Feb 2015 12:24:26 +0900 d56596e4e784 d57c88171f38
comparison
equal inserted replaced
127:d56596e4e784 128:d9a30f696933
71 fmap-tailDeltaM-with-deltaM-mu {n = O} (deltaM (mono x)) = refl 71 fmap-tailDeltaM-with-deltaM-mu {n = O} (deltaM (mono x)) = refl
72 fmap-tailDeltaM-with-deltaM-mu {n = S n} (deltaM d) = refl 72 fmap-tailDeltaM-with-deltaM-mu {n = S n} (deltaM d) = refl
73 73
74 74
75 75
76 {- 76
77 77
78 -- main proofs 78 -- main proofs
79 79
80 deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat} 80 deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat}
81 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> 81 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
184 ≡⟨ refl ⟩ 184 ≡⟨ refl ⟩
185 deltaM-mu (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d))) 185 deltaM-mu (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d)))
186 ≡⟨ refl ⟩ 186 ≡⟨ refl ⟩
187 deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (delta x d))) 187 deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (delta x d)))
188 188
189 189 {-
190 190
191 191
192 192
193 193
194 deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat} 194 deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat}
241 ≡⟨ refl ⟩ 241 ≡⟨ refl ⟩
242 deltaM (delta x d) 242 deltaM (delta x d)
243 243
244 244
245 245
246 -} 246
247 247
248 248
249 249
250 deltaM-left-unity-law : {l : Level} {A : Set l} {n : Nat} 250 deltaM-left-unity-law : {l : Level} {A : Set l} {n : Nat}
251 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} 251 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
292 deltaM (delta x (unDeltaM {M = M} (deltaM d))) 292 deltaM (delta x (unDeltaM {M = M} (deltaM d)))
293 ≡⟨ refl ⟩ 293 ≡⟨ refl ⟩
294 deltaM (delta x d) 294 deltaM (delta x d)
295 295
296 296
297 297 -}
298
299
300 deltaM-association-law : {l : Level} {A : Set l} {n : Nat}
301 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
302 (d : DeltaM M (DeltaM M (DeltaM M A (S n)) (S n)) (S n)) ->
303 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d)
304 deltaM-association-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = {!!}
298 {- 305 {-
299 306 deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
300 postulate nya : {l : Level} {A : Set l} 307 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d)))
301 (M : Set l -> Set l) (fm : Functor M) (mm : Monad M fm) 308 ≡⟨ refl ⟩
302 (d : DeltaM M {fm} {mm} (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S O)) (S O)) (S O)) -> 309 deltaM-mu (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d)))
303 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d) 310 ≡⟨ refl ⟩
304 311 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))))))
305 312 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d))))))))
306 313
307 314 ≡⟨ refl ⟩
308 315 deltaM (delta (mu M (fmap F (headDeltaM {A = A} {M = M}) (fmap F deltaM-mu x)))
309 316 (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d))))))
310 317 ≡⟨ 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)))))))
311 deltaM-association-law : {l : Level} {A : Set l} {n : Nat} 318 (sym (covariant F deltaM-mu headDeltaM x)) ⟩
312 (M : Set l -> Set l) (fm : Functor M) (mm : Monad M fm) 319 deltaM (delta (mu M (fmap F ((headDeltaM {A = A} {M = M}) ∙ deltaM-mu) x))
313 (d : DeltaM M {fm} {mm} (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S n)) (S n)) (S n)) -> 320 (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d))))))
314 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d) 321 ≡⟨ cong (\de -> deltaM (delta (mu M de)
315 deltaM-association-law {l} {A} {O} M fm mm (deltaM (mono x)) = nya {l} {A} M fm mm (deltaM (mono x)) 322 (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d)))))))
323 (fmap-headDeltaM-with-deltaM-mu {A = A} {M = M} x) ⟩
324 deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
325 (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d))))))
326 ≡⟨ refl ⟩
327 deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
328 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-fmap deltaM-mu (deltaM d))))))
329 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
330 (unDeltaM {M = M} (deltaM-mu de))))
331 (sym (deltaM-covariant tailDeltaM deltaM-mu (deltaM d))) ⟩
332 deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
333 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM ∙ deltaM-mu) (deltaM d)))))
334 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
335 (unDeltaM {M = M} (deltaM-mu de))))
336 (fmap-tailDeltaM-with-deltaM-mu (deltaM d)) ⟩
337 deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
338 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
339 ≡⟨ cong (\de -> deltaM (delta (mu M de)
340 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
341 (covariant F headDeltaM ((mu M) ∙ (fmap F headDeltaM)) x) ⟩
342 deltaM (delta (mu M (((fmap F ((mu M) ∙ (fmap F headDeltaM))) ∙ (fmap F headDeltaM)) x))
343 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
344 ≡⟨ refl ⟩
345 deltaM (delta (mu M (((fmap F ((mu M) ∙ (fmap F headDeltaM))) (fmap F headDeltaM x))))
346 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
347 ≡⟨ cong (\de -> deltaM (delta (mu M de)
348 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
349 (covariant F (fmap F headDeltaM) (mu M) (fmap F headDeltaM x)) ⟩
350
351 deltaM (delta (mu M ((((fmap F (mu M)) ∙ (fmap F (fmap F headDeltaM))) (fmap F headDeltaM x))))
352 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
353 ≡⟨ refl ⟩
354 deltaM (delta (mu M (fmap F (mu M) (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))))
355 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
356 ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
357 (association-law M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))) ⟩
358 deltaM (delta (mu M (mu M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))))
359 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
360 ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
361 (mu-is-nt M headDeltaM (fmap F headDeltaM x)) ⟩
362 deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
363 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
364 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) (unDeltaM {M = M} (deltaM-mu de))))
365 (deltaM-covariant (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) tailDeltaM (deltaM d)) ⟩
366 deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
367 (unDeltaM {M = M} (deltaM-mu (((deltaM-fmap (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ (deltaM-fmap tailDeltaM)) (deltaM d))))))
368 ≡⟨ refl ⟩
369 deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
370 (unDeltaM {M = M} (deltaM-mu (((deltaM-fmap (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) (deltaM-fmap tailDeltaM (deltaM d))))))))
371 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) (unDeltaM {M = M} (deltaM-mu de))))
372 (deltaM-covariant deltaM-mu (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d))) ⟩
373 deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
374 (unDeltaM {M = M} (deltaM-mu (((deltaM-fmap deltaM-mu) ∙ (deltaM-fmap (deltaM-fmap tailDeltaM))) (deltaM-fmap tailDeltaM (deltaM d))))))
375 ≡⟨ refl ⟩
376 deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
377 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap deltaM-mu (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))))))
378 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) (unDeltaM {M = M} de)))
379 (deltaM-association-law (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))) ⟩
380 deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
381 (unDeltaM {M = M} (deltaM-mu (deltaM-mu (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))))))
382
383 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
384 (unDeltaM {M = M} (deltaM-mu de))))
385 (sym (deltaM-mu-is-nt tailDeltaM (deltaM-fmap tailDeltaM (deltaM d)))) ⟩
386 deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
387 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
388 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
389 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM de)))))
390 (sym (deconstruct-id (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))) ⟩
391 deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
392 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM
393 (deltaM (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))))
394
395
396 ≡⟨ refl ⟩
397 deltaM (delta (mu M (fmap F headDeltaM (headDeltaM {M = M} ((deltaM (delta (mu M (fmap F headDeltaM x))
398 (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))))))
399 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM ((deltaM (delta (mu M (fmap F headDeltaM x))
400 (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))))))))
401
402
403 ≡⟨ refl ⟩
404 deltaM-mu (deltaM (delta (mu M (fmap F headDeltaM x))
405 (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
406 ≡⟨ refl ⟩
407 deltaM-mu (deltaM (delta (mu M (fmap F headDeltaM (headDeltaM {M = M} (deltaM (delta x d)))))
408 (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d))))))))
409 ≡⟨ refl ⟩
410 deltaM-mu (deltaM-mu (deltaM (delta x d)))
411
412 -}
413
316 {- 414 {-
516 415
517 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} 416 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat}
518 {M : Set l -> Set l} 417 {M : Set l -> Set l}
519 (functorM : Functor M) 418 (functorM : Functor M)
520 (monadM : Monad M functorM) -> 419 (M : Monad M functorM) ->
521 Monad {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) (deltaM-is-functor {l} {n}) 420 Monad {l} (\A -> DeltaM M {functorM} {M} A (S n)) (deltaM-is-functor {l} {n})
522 deltaM-is-monad {l} {A} {n} {M} functorM monadM = 421 deltaM-is-monad {l} {A} {n} {M} functorM M =
523 record { mu = deltaM-mu 422 record { mu = deltaM-mu
524 ; eta = deltaM-eta 423 ; eta = deltaM-eta
525 ; eta-is-nt = deltaM-eta-is-nt 424 ; eta-is-nt = deltaM-eta-is-nt
526 ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x))) 425 ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x)))
527 ; association-law = (deltaM-association-law M functorM monadM) 426 ; association-law = (deltaM-association-law M functorM M)
528 ; left-unity-law = deltaM-left-unity-law 427 ; left-unity-law = deltaM-left-unity-law
529 ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) 428 ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x)))
530 } 429 }
531 430
532 431
432
533 -} 433 -}