Mercurial > hg > Members > atton > delta_monad

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

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix association-law for DeltaM in (S n)
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 12:24:26 +0900
parents d56596e4e784
children d57c88171f38
comparison
equal deleted 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 {-
317 begin
318 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩
319 deltaM-mu (deltaM (mono (fmap fm deltaM-mu x))) ≡⟨ refl ⟩
320 deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M A (S O)} {monadM = mm} (deltaM (mono (fmap fm deltaM-mu x))))))) ≡⟨ refl ⟩
321 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))) ≡⟨ refl ⟩
322 deltaM (mono (mu mm (fmap fm (headDeltaM {A = A} {monadM = mm}) (fmap fm
323 (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))))) x))))
324 ≡⟨ cong (\de -> deltaM (mono (mu mm de)))
325 (sym (covariant fm (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))))) headDeltaM x)) ⟩
326 deltaM (mono (mu mm (fmap fm ((headDeltaM {A = A} {monadM = mm}) ∙
327 (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d))))))) x)))
328 ≡⟨ refl ⟩
329 deltaM (mono (mu mm (fmap fm (\d -> (headDeltaM {A = A} {monadM = mm} (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d))))))) x)))
330 ≡⟨ refl ⟩
331 deltaM (mono (mu mm (fmap fm (\d -> (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))) x)))
332 ≡⟨ refl ⟩
333 deltaM (mono (mu mm (fmap fm ((mu mm) ∙ (((fmap fm headDeltaM)) ∙ ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm})))) x)))
334 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (covariant fm ((fmap fm headDeltaM) ∙ (headDeltaM)) (mu mm) x )⟩
335 deltaM (mono (mu mm (((fmap fm (mu mm)) ∙ (fmap fm ((fmap fm headDeltaM) ∙ (headDeltaM {l} {DeltaM M A (S O)} {monadM = mm})))) x)))
336 ≡⟨ refl ⟩
337 deltaM (mono (mu mm (fmap fm (mu mm) ((fmap fm ((fmap fm headDeltaM) ∙ (headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}))) x))))
338 ≡⟨ cong (\de -> deltaM (mono (mu mm (fmap fm (mu mm) de)))) (covariant fm headDeltaM (fmap fm headDeltaM) x) ⟩
339 deltaM (mono (mu mm (fmap fm (mu mm) (((fmap fm (fmap fm headDeltaM)) ∙ (fmap fm (headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}))) x))))
340 ≡⟨ refl ⟩
341 deltaM (mono (mu mm (fmap fm (mu mm) (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x)))))
342 ≡⟨ cong (\de -> deltaM (mono de)) (association-law mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))) ⟩
343 deltaM (mono (mu mm (mu mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x)))))
344 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (mu-is-nt mm headDeltaM (fmap fm headDeltaM x)) ⟩
345 deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))) ≡⟨ refl ⟩
346 deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M A (S O)} {monadM = mm} (deltaM (mono (mu mm (fmap fm headDeltaM x)))))))) ≡⟨ refl ⟩
347 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM x)))) ≡⟨ refl ⟩
348 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M (DeltaM M A (S O)) (S O)} {monadM = mm} (deltaM (mono x))))))) ≡⟨ refl ⟩
349 deltaM-mu (deltaM-mu (deltaM (mono x))) ∎
350 -}
351 deltaM-association-law {l} {A} {S n} M fm mm (deltaM (delta x d)) = begin
352 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d)))
353 ≡⟨ refl ⟩
354 deltaM-mu (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d)))
355 ≡⟨ refl ⟩
356 deltaM (delta (mu mm (fmap fm (headDeltaM {A = A} {monadM = mm}) (headDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d))))))
357 (unDeltaM {A = A} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d))))))))
358
359 ≡⟨ refl ⟩
360 deltaM (delta (mu mm (fmap fm (headDeltaM {A = A} {monadM = mm}) (fmap fm deltaM-mu x)))
361 (unDeltaM {A = A} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d))))))
362 ≡⟨ cong (\de -> deltaM (delta (mu mm de) (unDeltaM {A = A} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d)))))))
363 (sym (covariant fm deltaM-mu headDeltaM x)) ⟩
364 deltaM (delta (mu mm (fmap fm ((headDeltaM {A = A} {monadM = mm}) ∙ deltaM-mu) x))
365 (unDeltaM {A = A} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d))))))
366 ≡⟨ cong (\de -> deltaM (delta (mu mm de)
367 (unDeltaM {A = A} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d)))))))
368 (fmap-headDeltaM-with-deltaM-mu {A = A} {monadM = mm} x) ⟩
369 deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
370 (unDeltaM {A = A} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d))))))
371 ≡⟨ refl ⟩
372 deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
373 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-fmap deltaM-mu (deltaM d))))))
374 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
375 (unDeltaM {monadM = mm} (deltaM-mu de))))
376 (sym (deltaM-covariant fm tailDeltaM deltaM-mu (deltaM d))) ⟩
377 deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
378 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap (tailDeltaM ∙ deltaM-mu) (deltaM d)))))
379 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
380 (unDeltaM {monadM = mm} (deltaM-mu de))))
381 (fmap-tailDeltaM-with-deltaM-mu (deltaM d)) ⟩
382 deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
383 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
384 ≡⟨ cong (\de -> deltaM (delta (mu mm de)
385 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
386 (covariant fm headDeltaM ((mu mm) ∙ (fmap fm headDeltaM)) x) ⟩
387 deltaM (delta (mu mm (((fmap fm ((mu mm) ∙ (fmap fm headDeltaM))) ∙ (fmap fm headDeltaM)) x))
388 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
389 ≡⟨ refl ⟩
390 deltaM (delta (mu mm (((fmap fm ((mu mm) ∙ (fmap fm headDeltaM))) (fmap fm headDeltaM x))))
391 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
392 ≡⟨ cong (\de -> deltaM (delta (mu mm de)
393 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
394 (covariant fm (fmap fm headDeltaM) (mu mm) (fmap fm headDeltaM x)) ⟩
395
396 deltaM (delta (mu mm ((((fmap fm (mu mm)) ∙ (fmap fm (fmap fm headDeltaM))) (fmap fm headDeltaM x))))
397 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
398 ≡⟨ refl ⟩
399 deltaM (delta (mu mm (fmap fm (mu mm) (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))))
400 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
401 ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
402 (association-law mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))) ⟩
403 deltaM (delta (mu mm (mu mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))))
404 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
405 ≡⟨ cong (\de -> deltaM (delta (mu mm de) (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
406 (mu-is-nt mm headDeltaM (fmap fm headDeltaM x)) ⟩
407 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
408 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
409 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))) (unDeltaM {monadM = mm} (deltaM-mu de))))
410 (deltaM-covariant fm (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) tailDeltaM (deltaM d)) ⟩
411 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
412 (unDeltaM {monadM = mm} (deltaM-mu (((deltaM-fmap (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ (deltaM-fmap tailDeltaM)) (deltaM d))))))
413 ≡⟨ refl ⟩
414 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
415 (unDeltaM {monadM = mm} (deltaM-mu (((deltaM-fmap (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) (deltaM-fmap tailDeltaM (deltaM d))))))))
416 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))) (unDeltaM {monadM = mm} (deltaM-mu de))))
417 (deltaM-covariant fm deltaM-mu (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d))) ⟩
418 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
419 (unDeltaM {monadM = mm} (deltaM-mu (((deltaM-fmap deltaM-mu) ∙ (deltaM-fmap (deltaM-fmap tailDeltaM))) (deltaM-fmap tailDeltaM (deltaM d))))))
420 ≡⟨ refl ⟩
421 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
422 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap deltaM-mu (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))))))
423 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))) (unDeltaM {monadM = mm} de)))
424 (deltaM-association-law M fm mm (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))) ⟩
425 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
426 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-mu (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))))))
427
428 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
429 (unDeltaM {monadM = mm} (deltaM-mu de))))
430 (sym (deltaM-mu-is-nt tailDeltaM (deltaM-fmap tailDeltaM (deltaM d)))) ⟩
431 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
432 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
433 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
434 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM de)))))
435 (sym (deconstruct-id (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))) ⟩
436 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
437 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM
438 (deltaM (unDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))))
439
440
441 ≡⟨ refl ⟩
442 deltaM (delta (mu mm (fmap fm headDeltaM (headDeltaM {monadM = mm} ((deltaM (delta (mu mm (fmap fm headDeltaM x))
443 (unDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))))))
444 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM ((deltaM (delta (mu mm (fmap fm headDeltaM x))
445 (unDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))))))))
446
447
448 ≡⟨ refl ⟩
449 deltaM-mu (deltaM (delta (mu mm (fmap fm headDeltaM x))
450 (unDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
451 ≡⟨ refl ⟩
452 deltaM-mu (deltaM (delta (mu mm (fmap fm headDeltaM (headDeltaM {monadM = mm} (deltaM (delta x d)))))
453 (unDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d))))))))
454 ≡⟨ refl ⟩
455 deltaM-mu (deltaM-mu (deltaM (delta x d)))
456 ∎
457 {-
458 deltaM-association-law {l} {A} {S n} M fm mm (deltaM (delta x d)) = begin
459 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩
460 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-mu) (delta x d))) ≡⟨ refl ⟩
461 deltaM-mu (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d))) ≡⟨ refl ⟩
462 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))))
463 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d)))) ≡⟨ refl ⟩
464 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))))
465 (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d))))
466 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x))))) de)
467 (sym (deconstruct-id (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d)))))) ⟩
468
469 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))))
470 (deltaM (deconstruct {A = A} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d))))))
471 ≡⟨ refl ⟩
472 deltaM (deltaAppend (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x))))
473 (deconstruct {A = A} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d))))))
474 ≡⟨ refl ⟩
475 deltaM (delta (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))
476 (deconstruct {A = A} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d))))))
477 ≡⟨ {!!} ⟩
478 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))))
479 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d)))))
480 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))))
481 (deltaM-mu (deltaM-fmap tailDeltaM de)))
482 (sym (deconstruct-id (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))) ⟩
483 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))))
484 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d)))))))
485
486 ≡⟨ refl ⟩
487 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))))
488 (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM ( (deltaM (delta (mu mm (fmap fm headDeltaM x))
489 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))))))
490 ≡⟨ refl ⟩
491 appendDeltaM (deltaM (mono (mu mm (fmap fm (headDeltaM {monadM = mm}) (headDeltaM {monadM = mm} ((deltaM (delta (mu mm (fmap fm headDeltaM x))
492 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))))))))
493 (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM ( (deltaM (delta (mu mm (fmap fm headDeltaM x))
494 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))))))
495 ≡⟨ refl ⟩
496 deltaM-mu (deltaM (delta (mu mm (fmap fm headDeltaM x))
497 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))
498 ≡⟨ refl ⟩
499 deltaM-mu (deltaM (deltaAppend (mono (mu mm (fmap fm headDeltaM x)))
500 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))
501 ≡⟨ refl ⟩
502 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x))))
503 (deltaM (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))
504 ≡⟨ cong (\de -> deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x)))) de))
505 (deconstruct-id (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d)))) ⟩
506 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x))))
507 (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))
508 ≡⟨ refl ⟩
509 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x))))
510 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))≡⟨ refl ⟩
511 deltaM-mu (deltaM-mu (deltaM (delta x d)))
512 ∎
513 -}
514
515
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 -}