Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/monad.agda @ 118:53cb21845dea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove association-law for DeltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 02 Feb 2015 11:54:23 +0900
parents 6f86b55bf8b4
children 48b44bd85056
comparison
equal deleted inserted replaced
117:6f86b55bf8b4 118:53cb21845dea
15 open Functor 15 open Functor
16 open NaturalTransformation 16 open NaturalTransformation
17 open Monad 17 open Monad
18 18
19 19
20 -- proof utils
21 deconstruct : {l : Level} {A : Set l} {n : Nat}
22 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm}
23 (d : DeltaM M {fm} {mm} A (S n)) -> Delta (M A) (S n)
24 deconstruct (deltaM d) = d
25
26
27
28 -- sub proofs 20 -- sub proofs
29 21
30 deconstruct-id : {l : Level} {A : Set l} {n : Nat} 22 deconstruct-id : {l : Level} {A : Set l} {n : Nat}
31 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm} 23 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm}
32 (d : DeltaM M {fm} {mm} A (S n)) -> deltaM (deconstruct d) ≡ d 24 (d : DeltaM M {fm} {mm} A (S n)) -> deltaM (unDeltaM d) ≡ d
33 deconstruct-id {n = O} (deltaM x) = refl 25 deconstruct-id {n = O} (deltaM x) = refl
34 deconstruct-id {n = S n} (deltaM x) = refl 26 deconstruct-id {n = S n} (deltaM x) = refl
35 27
36 28
37 headDeltaM-with-appendDeltaM : {l : Level} {A : Set l} {n m : Nat} 29 headDeltaM-with-appendDeltaM : {l : Level} {A : Set l} {n m : Nat}
38 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm} 30 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm}
55 (d : DeltaM M {functorM} {monadM} A (S n)) -> 47 (d : DeltaM M {functorM} {monadM} A (S n)) ->
56 deltaM-fmap ((tailDeltaM {n = n} {monadM = monadM} ) ∙ deltaM-eta) d ≡ deltaM-fmap (deltaM-eta) d 48 deltaM-fmap ((tailDeltaM {n = n} {monadM = monadM} ) ∙ deltaM-eta) d ≡ deltaM-fmap (deltaM-eta) d
57 fmap-tailDeltaM-with-deltaM-eta {n = O} d = refl 49 fmap-tailDeltaM-with-deltaM-eta {n = O} d = refl
58 fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl 50 fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl
59 51
60
61 fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat} 52 fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat}
62 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm} 53 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM}
63 (x : M (DeltaM M {fm} {mm} (DeltaM M A (S n)) (S n))) -> 54 (x : M (DeltaM M (DeltaM M {functorM} {monadM} A (S n)) (S n))) ->
64 fmap fm (headDeltaM ∙ deltaM-mu) x ≡ fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x 55 fmap functorM (headDeltaM ∙ deltaM-mu) x ≡ fmap functorM (((mu monadM) ∙ (fmap functorM headDeltaM)) ∙ headDeltaM) x
65 fmap-headDeltaM-with-deltaM-mu {l} {A} {O} {M} {fm} {mm} x = refl 56 fmap-headDeltaM-with-deltaM-mu {n = O} x = refl
66 fmap-headDeltaM-with-deltaM-mu {l} {A} {S n} {M} {fm} {mm} x = begin 57 fmap-headDeltaM-with-deltaM-mu {n = S n} x = refl
67 fmap fm (headDeltaM ∙ deltaM-mu) x ≡⟨ refl ⟩ 58
68 fmap fm (headDeltaM ∙ (\d -> appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d))))) 59
69 (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM d))))) x ≡⟨ refl ⟩ 60 fmap-tailDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat}
70 fmap fm (\d -> headDeltaM (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d))))) 61 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM}
71 (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM d))))) x 62 (d : DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} (DeltaM M A (S (S n))) (S (S n))) (S n)) ->
72 ≡⟨ refl ⟩ 63 deltaM-fmap (tailDeltaM ∙ deltaM-mu) d ≡ deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) d
73 fmap fm (\d -> headDeltaM (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d))))) 64 fmap-tailDeltaM-with-deltaM-mu {n = O} (deltaM (mono x)) = refl
74 (deltaM (deconstruct {A = A} {mm = mm} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM d))))))) x 65 fmap-tailDeltaM-with-deltaM-mu {n = S n} (deltaM d) = refl
75 ≡⟨ {!!} ⟩ 66
76 fmap fm (\d -> headDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d)))))) x ≡⟨ refl ⟩ 67
77 fmap fm (\d -> (mu mm (fmap fm headDeltaM (headDeltaM d)))) x ≡⟨ {!!} ⟩
78 fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x
79 ∎
80 68
81 69
82 70
83 -- main proofs 71 -- main proofs
84 72
103 ≡⟨ refl ⟩ 91 ≡⟨ refl ⟩
104 deltaM-fmap f (deltaM-eta {n = S n} x) 92 deltaM-fmap f (deltaM-eta {n = S n} x)
105 ∎ 93 ∎
106 -} 94 -}
107 95
96 postulate deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat}
97 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
98 (f : A -> B) ->
99 (d : DeltaM T {F} {M} (DeltaM T A (S n)) (S n)) ->
100 deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d)
101
108 postulate deltaM-right-unity-law : {l : Level} {A : Set l} 102 postulate deltaM-right-unity-law : {l : Level} {A : Set l}
109 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} {n : Nat} 103 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} {n : Nat}
110 (d : DeltaM M {functorM} {monadM} A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d 104 (d : DeltaM M {functorM} {monadM} A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d
111 {- 105 {-
112 deltaM-right-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin 106 deltaM-right-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin
263 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 ⟩ 257 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 ⟩
264 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM x)))) ≡⟨ refl ⟩ 258 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM x)))) ≡⟨ refl ⟩
265 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 ⟩ 259 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 ⟩
266 deltaM-mu (deltaM-mu (deltaM (mono x))) ∎ 260 deltaM-mu (deltaM-mu (deltaM (mono x))) ∎
267 -} 261 -}
268 deltaM-association-law {l} {A} {S n} M fm mm (deltaM (delta x d)) = {!!} 262 deltaM-association-law {l} {A} {S n} M fm mm (deltaM (delta x d)) = begin
263 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d)))
264 ≡⟨ refl ⟩
265 deltaM-mu (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d)))
266 ≡⟨ refl ⟩
267 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))))))
268 (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))))))))
269
270 ≡⟨ refl ⟩
271 deltaM (delta (mu mm (fmap fm (headDeltaM {A = A} {monadM = mm}) (fmap fm deltaM-mu x)))
272 (unDeltaM {A = A} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d))))))
273 ≡⟨ 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)))))))
274 (sym (covariant fm deltaM-mu headDeltaM x)) ⟩
275 deltaM (delta (mu mm (fmap fm ((headDeltaM {A = A} {monadM = mm}) ∙ deltaM-mu) x))
276 (unDeltaM {A = A} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d))))))
277 ≡⟨ cong (\de -> deltaM (delta (mu mm de)
278 (unDeltaM {A = A} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d)))))))
279 (fmap-headDeltaM-with-deltaM-mu {A = A} {monadM = mm} x) ⟩
280 deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
281 (unDeltaM {A = A} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d))))))
282 ≡⟨ refl ⟩
283 deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
284 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-fmap deltaM-mu (deltaM d))))))
285 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
286 (unDeltaM {monadM = mm} (deltaM-mu de))))
287 (sym (deltaM-covariant fm tailDeltaM deltaM-mu (deltaM d))) ⟩
288 deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
289 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap (tailDeltaM ∙ deltaM-mu) (deltaM d)))))
290 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
291 (unDeltaM {monadM = mm} (deltaM-mu de))))
292 (fmap-tailDeltaM-with-deltaM-mu (deltaM d)) ⟩
293 deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
294 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
295 ≡⟨ cong (\de -> deltaM (delta (mu mm de)
296 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
297 (covariant fm headDeltaM ((mu mm) ∙ (fmap fm headDeltaM)) x) ⟩
298 deltaM (delta (mu mm (((fmap fm ((mu mm) ∙ (fmap fm headDeltaM))) ∙ (fmap fm headDeltaM)) x))
299 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
300 ≡⟨ refl ⟩
301 deltaM (delta (mu mm (((fmap fm ((mu mm) ∙ (fmap fm headDeltaM))) (fmap fm headDeltaM x))))
302 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
303 ≡⟨ cong (\de -> deltaM (delta (mu mm de)
304 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
305 (covariant fm (fmap fm headDeltaM) (mu mm) (fmap fm headDeltaM x)) ⟩
306
307 deltaM (delta (mu mm ((((fmap fm (mu mm)) ∙ (fmap fm (fmap fm headDeltaM))) (fmap fm headDeltaM x))))
308 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
309 ≡⟨ refl ⟩
310 deltaM (delta (mu mm (fmap fm (mu mm) (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))))
311 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
312 ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
313 (association-law mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))) ⟩
314 deltaM (delta (mu mm (mu mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))))
315 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
316 ≡⟨ cong (\de -> deltaM (delta (mu mm de) (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
317 (mu-is-nt mm headDeltaM (fmap fm headDeltaM x)) ⟩
318 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
319 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
320 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))) (unDeltaM {monadM = mm} (deltaM-mu de))))
321 (deltaM-covariant fm (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) tailDeltaM (deltaM d)) ⟩
322 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
323 (unDeltaM {monadM = mm} (deltaM-mu (((deltaM-fmap (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ (deltaM-fmap tailDeltaM)) (deltaM d))))))
324 ≡⟨ refl ⟩
325 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
326 (unDeltaM {monadM = mm} (deltaM-mu (((deltaM-fmap (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) (deltaM-fmap tailDeltaM (deltaM d))))))))
327 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))) (unDeltaM {monadM = mm} (deltaM-mu de))))
328 (deltaM-covariant fm deltaM-mu (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d))) ⟩
329 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
330 (unDeltaM {monadM = mm} (deltaM-mu (((deltaM-fmap deltaM-mu) ∙ (deltaM-fmap (deltaM-fmap tailDeltaM))) (deltaM-fmap tailDeltaM (deltaM d))))))
331 ≡⟨ refl ⟩
332 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
333 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap deltaM-mu (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))))))
334 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))) (unDeltaM {monadM = mm} de)))
335 (deltaM-association-law M fm mm (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))) ⟩
336 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
337 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-mu (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))))))
338
339 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
340 (unDeltaM {monadM = mm} (deltaM-mu de))))
341 (sym (deltaM-mu-is-nt tailDeltaM (deltaM-fmap tailDeltaM (deltaM d)))) ⟩
342 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
343 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
344 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
345 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM de)))))
346 (sym (deconstruct-id (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))) ⟩
347 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
348 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM
349 (deltaM (unDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))))
350
351
352 ≡⟨ refl ⟩
353 deltaM (delta (mu mm (fmap fm headDeltaM (headDeltaM {monadM = mm} ((deltaM (delta (mu mm (fmap fm headDeltaM x))
354 (unDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))))))
355 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM ((deltaM (delta (mu mm (fmap fm headDeltaM x))
356 (unDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))))))))
357
358
359 ≡⟨ refl ⟩
360 deltaM-mu (deltaM (delta (mu mm (fmap fm headDeltaM x))
361 (unDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
362 ≡⟨ refl ⟩
363 deltaM-mu (deltaM (delta (mu mm (fmap fm headDeltaM (headDeltaM {monadM = mm} (deltaM (delta x d)))))
364 (unDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d))))))))
365 ≡⟨ refl ⟩
366 deltaM-mu (deltaM-mu (deltaM (delta x d)))
367 ∎
269 {- 368 {-
270 deltaM-association-law {l} {A} {S n} M fm mm (deltaM (delta x d)) = begin 369 deltaM-association-law {l} {A} {S n} M fm mm (deltaM (delta x d)) = begin
271 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩ 370 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩
272 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-mu) (delta x d))) ≡⟨ refl ⟩ 371 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-mu) (delta x d))) ≡⟨ refl ⟩
273 deltaM-mu (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d))) ≡⟨ refl ⟩ 372 deltaM-mu (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d))) ≡⟨ refl ⟩
338 bind = deltaM-bind; 437 bind = deltaM-bind;
339 association-law = (deltaM-association-law M functorM monadM) ; 438 association-law = (deltaM-association-law M functorM monadM) ;
340 left-unity-law = deltaM-left-unity-law; 439 left-unity-law = deltaM-left-unity-law;
341 right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ; 440 right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ;
342 eta-is-nt = deltaM-eta-is-nt; 441 eta-is-nt = deltaM-eta-is-nt;
343 mu-is-nt = {!!}} 442 mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x)))}
344 443
345 444