Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/monad.agda @ 124:48b44bd85056

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix proof natural transformation for deltaM-eta
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 02 Feb 2015 13:12:49 +0900
parents 53cb21845dea
children 6dcc68ef8f96
comparison
equal deleted inserted replaced
123:ee7f5162ec1f 124:48b44bd85056
15 open Functor 15 open Functor
16 open NaturalTransformation 16 open NaturalTransformation
17 open Monad 17 open Monad
18 18
19 19
20 -- sub proofs 20 -- sub proofs
21 21
22 deconstruct-id : {l : Level} {A : Set l} {n : Nat} 22 deconstruct-id : {l : Level} {A : Set l} {n : Nat}
23 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm} 23 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
24 (d : DeltaM M {fm} {mm} 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 28
29 headDeltaM-with-appendDeltaM : {l : Level} {A : Set l} {n m : Nat} 29 headDeltaM-with-appendDeltaM : {l : Level} {A : Set l} {n m : Nat}
30 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm} 30 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
31 (d : DeltaM M {fm} {mm} A (S n)) -> (ds : DeltaM M {fm} {mm} A (S m)) -> 31 (d : DeltaM M A (S n)) -> (ds : DeltaM M A (S m)) ->
32 headDeltaM (appendDeltaM d ds) ≡ headDeltaM d 32 headDeltaM (appendDeltaM d ds) ≡ headDeltaM d
33 headDeltaM-with-appendDeltaM {l} {A} {n = O} {O} (deltaM (mono _)) (deltaM _) = refl 33 headDeltaM-with-appendDeltaM {l} {A} {O} {O} (deltaM (mono _)) (deltaM _) = refl
34 headDeltaM-with-appendDeltaM {l} {A} {n = O} {S m} (deltaM (mono _)) (deltaM _) = refl 34 headDeltaM-with-appendDeltaM {l} {A} {O} {S m} (deltaM (mono _)) (deltaM _) = refl
35 headDeltaM-with-appendDeltaM {l} {A} {n = S n} {O} (deltaM (delta _ _)) (deltaM _) = refl 35 headDeltaM-with-appendDeltaM {l} {A} {S n} {O} (deltaM (delta _ _)) (deltaM _) = refl
36 headDeltaM-with-appendDeltaM {l} {A} {n = S n} {S m} (deltaM (delta _ _)) (deltaM _) = refl 36 headDeltaM-with-appendDeltaM {l} {A} {S n} {S m} (deltaM (delta _ _)) (deltaM _) = refl
37
38
37 39
38 fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} 40 fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
39 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} 41 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
40 (x : M A) -> (fmap functorM ((headDeltaM {l} {A} {n} {M} {functorM} {monadM}) ∙ deltaM-eta) x) ≡ fmap functorM (eta monadM) x 42 (x : T A) -> (fmap F ((headDeltaM {n = n} {M = M}) ∙ deltaM-eta) x) ≡ fmap F (eta M) x
41 fmap-headDeltaM-with-deltaM-eta {l} {A} {O} {M} {fm} {mm} x = refl 43 fmap-headDeltaM-with-deltaM-eta {n = O} x = refl
42 fmap-headDeltaM-with-deltaM-eta {l} {A} {S n} {M} {fm} {mm} x = refl 44 fmap-headDeltaM-with-deltaM-eta {n = S n} x = refl
45
43 46
44 47
45 fmap-tailDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} 48 fmap-tailDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
46 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} 49 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
47 (d : DeltaM M {functorM} {monadM} A (S n)) -> 50 (d : DeltaM M A (S n)) ->
48 deltaM-fmap ((tailDeltaM {n = n} {monadM = monadM} ) ∙ deltaM-eta) d ≡ deltaM-fmap (deltaM-eta) d 51 deltaM-fmap ((tailDeltaM {n = n} {M = M} ) ∙ deltaM-eta) d ≡ deltaM-fmap (deltaM-eta) d
49 fmap-tailDeltaM-with-deltaM-eta {n = O} d = refl 52 fmap-tailDeltaM-with-deltaM-eta {n = O} d = refl
50 fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl 53 fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl
51 54
55
56
52 fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat} 57 fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat}
53 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} 58 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
54 (x : M (DeltaM M (DeltaM M {functorM} {monadM} A (S n)) (S n))) -> 59 (x : T (DeltaM M (DeltaM M A (S n)) (S n))) ->
55 fmap functorM (headDeltaM ∙ deltaM-mu) x ≡ fmap functorM (((mu monadM) ∙ (fmap functorM headDeltaM)) ∙ headDeltaM) x 60 fmap F (headDeltaM ∙ deltaM-mu) x ≡ fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x
56 fmap-headDeltaM-with-deltaM-mu {n = O} x = refl 61 fmap-headDeltaM-with-deltaM-mu {n = O} x = refl
57 fmap-headDeltaM-with-deltaM-mu {n = S n} x = refl 62 fmap-headDeltaM-with-deltaM-mu {n = S n} x = refl
58 63
59 64
60 fmap-tailDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat} 65 fmap-tailDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat}
61 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} 66 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
62 (d : DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} (DeltaM M A (S (S n))) (S (S n))) (S n)) -> 67 (d : DeltaM M (DeltaM M (DeltaM M A (S (S n))) (S (S n))) (S n)) ->
63 deltaM-fmap (tailDeltaM ∙ deltaM-mu) d ≡ deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) d 68 deltaM-fmap (tailDeltaM ∙ deltaM-mu) d ≡ deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) d
64 fmap-tailDeltaM-with-deltaM-mu {n = O} (deltaM (mono x)) = refl 69 fmap-tailDeltaM-with-deltaM-mu {n = O} (deltaM (mono x)) = refl
65 fmap-tailDeltaM-with-deltaM-mu {n = S n} (deltaM d) = refl 70 fmap-tailDeltaM-with-deltaM-mu {n = S n} (deltaM d) = refl
66 71
67 72
68 73
69 74
70 75
71 -- main proofs 76 -- main proofs
72 77
73 postulate deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat} 78 deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat}
74 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} 79 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
75 (f : A -> B) -> (x : A) -> 80 (f : A -> B) -> (x : A) ->
76 ((deltaM-eta {l} {B} {n} {M} {functorM} {monadM} )∙ f) x ≡ deltaM-fmap f (deltaM-eta x) 81 ((deltaM-eta {l} {B} {n} {T} {F} {M} )∙ f) x ≡ deltaM-fmap f (deltaM-eta x)
77 {-
78 deltaM-eta-is-nt {l} {A} {B} {O} {M} {fm} {mm} f x = begin 82 deltaM-eta-is-nt {l} {A} {B} {O} {M} {fm} {mm} f x = begin
79 deltaM-eta {n = O} (f x) ≡⟨ refl ⟩ 83 deltaM-eta {n = O} (f x) ≡⟨ refl ⟩
80 deltaM (mono (eta mm (f x))) ≡⟨ cong (\de -> deltaM (mono de)) (eta-is-nt mm f x) ⟩ 84 deltaM (mono (eta mm (f x))) ≡⟨ cong (\de -> deltaM (mono de)) (eta-is-nt mm f x) ⟩
81 deltaM (mono (fmap fm f (eta mm x))) ≡⟨ refl ⟩ 85 deltaM (mono (fmap fm f (eta mm x))) ≡⟨ refl ⟩
82 deltaM-fmap f (deltaM-eta {n = O} x) ∎ 86 deltaM-fmap f (deltaM-eta {n = O} x) ∎
83 deltaM-eta-is-nt {l} {A} {B} {S n} {M} {fm} {mm} f x = begin 87 deltaM-eta-is-nt {l} {A} {B} {S n} {M} {fm} {mm} f x = begin
84 deltaM-eta {n = S n} (f x) ≡⟨ refl ⟩ 88 deltaM-eta {n = S n} (f x)
85 deltaM (delta-eta {n = S n} (eta mm (f x))) ≡⟨ refl ⟩ 89 ≡⟨ refl ⟩
90 deltaM (delta-eta {n = S n} (eta mm (f x)))
91 ≡⟨ refl ⟩
86 deltaM (delta (eta mm (f x)) (delta-eta (eta mm (f x)))) 92 deltaM (delta (eta mm (f x)) (delta-eta (eta mm (f x))))
87 ≡⟨ cong (\de -> deltaM (delta de (delta-eta de))) (eta-is-nt mm f x) ⟩ 93 ≡⟨ cong (\de -> deltaM (delta de (delta-eta de))) (eta-is-nt mm f x) ⟩
88 deltaM (delta (fmap fm f (eta mm x)) (delta-eta (fmap fm f (eta mm x)))) 94 deltaM (delta (fmap fm f (eta mm x)) (delta-eta (fmap fm f (eta mm x))))
89 ≡⟨ cong (\de -> deltaM (delta (fmap fm f (eta mm x)) de)) (eta-is-nt delta-is-monad (fmap fm f) (eta mm x)) ⟩ 95 ≡⟨ cong (\de -> deltaM (delta (fmap fm f (eta mm x)) de)) (eta-is-nt delta-is-monad (fmap fm f) (eta mm x)) ⟩
90 deltaM (delta (fmap fm f (eta mm x)) (delta-fmap (fmap fm f) (delta-eta (eta mm x)))) 96 deltaM (delta (fmap fm f (eta mm x)) (delta-fmap (fmap fm f) (delta-eta (eta mm x))))
91 ≡⟨ refl ⟩ 97 ≡⟨ refl ⟩
92 deltaM-fmap f (deltaM-eta {n = S n} x) 98 deltaM-fmap f (deltaM-eta {n = S n} x)
93 ∎ 99 ∎
94 -} 100
101
102 {-
95 103
96 postulate deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} 104 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} 105 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
98 (f : A -> B) -> 106 (f : A -> B) ->
99 (d : DeltaM T {F} {M} (DeltaM T A (S n)) (S n)) -> 107 (d : DeltaM T {F} {M} (DeltaM T A (S n)) (S n)) ->
212 (M : Set l -> Set l) (fm : Functor M) (mm : Monad M fm) 220 (M : Set l -> Set l) (fm : Functor M) (mm : Monad M fm)
213 (d : DeltaM M {fm} {mm} (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S O)) (S O)) (S O)) -> 221 (d : DeltaM M {fm} {mm} (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S O)) (S O)) (S O)) ->
214 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d) 222 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d)
215 223
216 224
217 225
218 226
219 227
220 228
221 229
222 deltaM-association-law : {l : Level} {A : Set l} {n : Nat} 230 deltaM-association-law : {l : Level} {A : Set l} {n : Nat}
223 (M : Set l -> Set l) (fm : Functor M) (mm : Monad M fm) 231 (M : Set l -> Set l) (fm : Functor M) (mm : Monad M fm)
224 (d : DeltaM M {fm} {mm} (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S n)) (S n)) (S n)) -> 232 (d : DeltaM M {fm} {mm} (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S n)) (S n)) (S n)) ->
228 begin 236 begin
229 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ 237 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩
230 deltaM-mu (deltaM (mono (fmap fm deltaM-mu x))) ≡⟨ refl ⟩ 238 deltaM-mu (deltaM (mono (fmap fm deltaM-mu x))) ≡⟨ refl ⟩
231 deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M A (S O)} {monadM = mm} (deltaM (mono (fmap fm deltaM-mu x))))))) ≡⟨ refl ⟩ 239 deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M A (S O)} {monadM = mm} (deltaM (mono (fmap fm deltaM-mu x))))))) ≡⟨ refl ⟩
232 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))) ≡⟨ refl ⟩ 240 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))) ≡⟨ refl ⟩
233 deltaM (mono (mu mm (fmap fm (headDeltaM {A = A} {monadM = mm}) (fmap fm 241 deltaM (mono (mu mm (fmap fm (headDeltaM {A = A} {monadM = mm}) (fmap fm
234 (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))))) x)))) 242 (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))))) x))))
235 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) 243 ≡⟨ cong (\de -> deltaM (mono (mu mm de)))
236 (sym (covariant fm (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))))) headDeltaM x)) ⟩ 244 (sym (covariant fm (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))))) headDeltaM x)) ⟩
237 deltaM (mono (mu mm (fmap fm ((headDeltaM {A = A} {monadM = mm}) ∙ 245 deltaM (mono (mu mm (fmap fm ((headDeltaM {A = A} {monadM = mm}) ∙
238 (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d))))))) x))) 246 (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d))))))) x)))
239 ≡⟨ refl ⟩ 247 ≡⟨ refl ⟩
240 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))) 248 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)))
241 ≡⟨ refl ⟩ 249 ≡⟨ refl ⟩
242 deltaM (mono (mu mm (fmap fm (\d -> (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))) x))) 250 deltaM (mono (mu mm (fmap fm (\d -> (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))) x)))
243 ≡⟨ refl ⟩ 251 ≡⟨ refl ⟩
244 deltaM (mono (mu mm (fmap fm ((mu mm) ∙ (((fmap fm headDeltaM)) ∙ ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm})))) x))) 252 deltaM (mono (mu mm (fmap fm ((mu mm) ∙ (((fmap fm headDeltaM)) ∙ ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm})))) x)))
245 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (covariant fm ((fmap fm headDeltaM) ∙ (headDeltaM)) (mu mm) x )⟩ 253 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (covariant fm ((fmap fm headDeltaM) ∙ (headDeltaM)) (mu mm) x )⟩
246 deltaM (mono (mu mm (((fmap fm (mu mm)) ∙ (fmap fm ((fmap fm headDeltaM) ∙ (headDeltaM {l} {DeltaM M A (S O)} {monadM = mm})))) x))) 254 deltaM (mono (mu mm (((fmap fm (mu mm)) ∙ (fmap fm ((fmap fm headDeltaM) ∙ (headDeltaM {l} {DeltaM M A (S O)} {monadM = mm})))) x)))
247 ≡⟨ refl ⟩ 255 ≡⟨ refl ⟩
248 deltaM (mono (mu mm (fmap fm (mu mm) ((fmap fm ((fmap fm headDeltaM) ∙ (headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}))) x)))) 256 deltaM (mono (mu mm (fmap fm (mu mm) ((fmap fm ((fmap fm headDeltaM) ∙ (headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}))) x))))
249 ≡⟨ cong (\de -> deltaM (mono (mu mm (fmap fm (mu mm) de)))) (covariant fm headDeltaM (fmap fm headDeltaM) x) ⟩ 257 ≡⟨ cong (\de -> deltaM (mono (mu mm (fmap fm (mu mm) de)))) (covariant fm headDeltaM (fmap fm headDeltaM) x) ⟩
250 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)))) 258 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))))
251 ≡⟨ refl ⟩ 259 ≡⟨ refl ⟩
252 deltaM (mono (mu mm (fmap fm (mu mm) (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))))) 260 deltaM (mono (mu mm (fmap fm (mu mm) (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x)))))
253 ≡⟨ cong (\de -> deltaM (mono de)) (association-law mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))) ⟩ 261 ≡⟨ cong (\de -> deltaM (mono de)) (association-law mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))) ⟩
254 deltaM (mono (mu mm (mu mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))))) 262 deltaM (mono (mu mm (mu mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x)))))
255 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (mu-is-nt mm headDeltaM (fmap fm headDeltaM x)) ⟩ 263 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (mu-is-nt mm headDeltaM (fmap fm headDeltaM x)) ⟩
256 deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))) ≡⟨ refl ⟩ 264 deltaM (mono (mu mm (fmap fm headDeltaM (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 ⟩ 265 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 ⟩
258 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM x)))) ≡⟨ refl ⟩ 266 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM 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 ⟩ 267 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 ⟩
298 deltaM (delta (mu mm (((fmap fm ((mu mm) ∙ (fmap fm headDeltaM))) ∙ (fmap fm headDeltaM)) x)) 306 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))))) 307 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
300 ≡⟨ refl ⟩ 308 ≡⟨ refl ⟩
301 deltaM (delta (mu mm (((fmap fm ((mu mm) ∙ (fmap fm headDeltaM))) (fmap fm headDeltaM x)))) 309 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))))) 310 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
303 ≡⟨ cong (\de -> deltaM (delta (mu mm de) 311 ≡⟨ cong (\de -> deltaM (delta (mu mm de)
304 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))) 312 (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)) ⟩ 313 (covariant fm (fmap fm headDeltaM) (mu mm) (fmap fm headDeltaM x)) ⟩
306 314
307 deltaM (delta (mu mm ((((fmap fm (mu mm)) ∙ (fmap fm (fmap fm headDeltaM))) (fmap fm headDeltaM x)))) 315 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))))) 316 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
343 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))) 351 (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)))) 352 ≡⟨ 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))))) 353 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM de)))))
346 (sym (deconstruct-id (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))) ⟩ 354 (sym (deconstruct-id (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))) ⟩
347 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))) 355 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
348 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM 356 (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))))))))) 357 (deltaM (unDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))))
350 358
351 359
352 ≡⟨ refl ⟩ 360 ≡⟨ refl ⟩
353 deltaM (delta (mu mm (fmap fm headDeltaM (headDeltaM {monadM = mm} ((deltaM (delta (mu mm (fmap fm headDeltaM x)) 361 deltaM (delta (mu mm (fmap fm headDeltaM (headDeltaM {monadM = mm} ((deltaM (delta (mu mm (fmap fm headDeltaM x))
372 deltaM-mu (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d))) ≡⟨ refl ⟩ 380 deltaM-mu (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d))) ≡⟨ refl ⟩
373 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x))))) 381 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))))
374 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d)))) ≡⟨ refl ⟩ 382 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d)))) ≡⟨ refl ⟩
375 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x))))) 383 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))))
376 (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d)))) 384 (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d))))
377 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x))))) de) 385 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x))))) de)
378 (sym (deconstruct-id (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d)))))) ⟩ 386 (sym (deconstruct-id (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d)))))) ⟩
379 387
380 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x))))) 388 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))))
381 (deltaM (deconstruct {A = A} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d)))))) 389 (deltaM (deconstruct {A = A} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d))))))
382 ≡⟨ refl ⟩ 390 ≡⟨ refl ⟩
387 (deconstruct {A = A} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d)))))) 395 (deconstruct {A = A} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d))))))
388 ≡⟨ {!!} ⟩ 396 ≡⟨ {!!} ⟩
389 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))))) 397 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))))
390 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))) 398 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d)))))
391 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))))) 399 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))))
392 (deltaM-mu (deltaM-fmap tailDeltaM de))) 400 (deltaM-mu (deltaM-fmap tailDeltaM de)))
393 (sym (deconstruct-id (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))) ⟩ 401 (sym (deconstruct-id (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))) ⟩
394 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))))) 402 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))))
395 (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))))))) 403 (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)))))))
396 404
397 ≡⟨ refl ⟩ 405 ≡⟨ refl ⟩
408 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d)))))) 416 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))
409 ≡⟨ refl ⟩ 417 ≡⟨ refl ⟩
410 deltaM-mu (deltaM (deltaAppend (mono (mu mm (fmap fm headDeltaM x))) 418 deltaM-mu (deltaM (deltaAppend (mono (mu mm (fmap fm headDeltaM x)))
411 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d)))))) 419 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))
412 ≡⟨ refl ⟩ 420 ≡⟨ refl ⟩
413 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x)))) 421 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x))))
414 (deltaM (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d)))))) 422 (deltaM (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))
415 ≡⟨ cong (\de -> deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x)))) de)) 423 ≡⟨ cong (\de -> deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x)))) de))
416 (deconstruct-id (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d)))) ⟩ 424 (deconstruct-id (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d)))) ⟩
417 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x)))) 425 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x))))
418 (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d)))) 426 (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))
419 ≡⟨ refl ⟩ 427 ≡⟨ refl ⟩
420 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x)))) 428 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x))))
421 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))≡⟨ refl ⟩ 429 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))≡⟨ refl ⟩
422 deltaM-mu (deltaM-mu (deltaM (delta x d))) 430 deltaM-mu (deltaM-mu (deltaM (delta x d)))
423 ∎ 431 ∎
424 -} 432 -}
425 433
428 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} 436 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat}
429 {M : Set l -> Set l} 437 {M : Set l -> Set l}
430 (functorM : Functor M) 438 (functorM : Functor M)
431 (monadM : Monad M functorM) -> 439 (monadM : Monad M functorM) ->
432 Monad {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) (deltaM-is-functor {l} {n}) 440 Monad {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) (deltaM-is-functor {l} {n})
433 deltaM-is-monad {l} {A} {n} {M} functorM monadM = 441 deltaM-is-monad {l} {A} {n} {M} functorM monadM =
434 record { mu = deltaM-mu; 442 record { mu = deltaM-mu
435 eta = deltaM-eta; 443 ; eta = deltaM-eta
436 return = deltaM-eta; 444 ; eta-is-nt = deltaM-eta-is-nt
437 bind = deltaM-bind; 445 ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x)))
438 association-law = (deltaM-association-law M functorM monadM) ; 446 ; association-law = (deltaM-association-law M functorM monadM)
439 left-unity-law = deltaM-left-unity-law; 447 ; left-unity-law = deltaM-left-unity-law
440 right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ; 448 ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x)))
441 eta-is-nt = deltaM-eta-is-nt; 449 }
442 mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x)))} 450
443 451
444 452 -}