Mercurial > hg > Members > atton > delta_monad
comparison agda/deltaM/monad.agda @ 130:ac45d065cbf2
Prove all Monad-laws for Delta with Monad
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 03 Feb 2015 12:46:20 +0900 |
parents | d57c88171f38 |
children | d205ff1e406f |
comparison
equal
deleted
inserted
replaced
129:d57c88171f38 | 130:ac45d065cbf2 |
---|---|
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 headDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat} | 28 headDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat} |
29 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} | 29 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} |
30 (f : A -> B) -> (x : (DeltaM M A (S n))) -> | 30 (f : A -> B) -> (x : (DeltaM M A (S n))) -> |
31 ((fmap F f) ∙ headDeltaM) x ≡ (headDeltaM ∙ (deltaM-fmap f)) x | 31 ((fmap F f) ∙ headDeltaM) x ≡ (headDeltaM ∙ (deltaM-fmap f)) x |
32 headDeltaM-with-f {n = O} f (deltaM (mono x)) = refl | 32 headDeltaM-with-f {n = O} f (deltaM (mono x)) = refl |
33 headDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl | 33 headDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl |
34 | 34 |
35 tailDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat} | 35 tailDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat} |
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} -> |
82 (f : A -> B) -> (x : A) -> | 82 (f : A -> B) -> (x : A) -> |
152 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) | 152 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) |
153 (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) | 153 (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) |
154 ≡⟨ refl ⟩ | 154 ≡⟨ refl ⟩ |
155 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) | 155 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) |
156 (unDeltaM {M = M} (deltaM-fmap f (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) | 156 (unDeltaM {M = M} (deltaM-fmap f (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) |
157 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM de))) | 157 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM de))) |
158 (deltaM-mu-is-nt {l} {A} {B} {n} {T} {F} {M} f (deltaM-fmap tailDeltaM (deltaM d))) ⟩ | 158 (deltaM-mu-is-nt {l} {A} {B} {n} {T} {F} {M} f (deltaM-fmap tailDeltaM (deltaM d))) ⟩ |
159 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) | 159 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) |
160 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (deltaM-fmap {n = n} f) (deltaM-fmap {n = n} (tailDeltaM {n = n}) (deltaM d)))))) | 160 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (deltaM-fmap {n = n} f) (deltaM-fmap {n = n} (tailDeltaM {n = n}) (deltaM d)))))) |
161 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de)))) | 161 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de)))) |
162 (sym (deltaM-covariant (deltaM-fmap f) tailDeltaM (deltaM d))) ⟩ | 162 (sym (deltaM-covariant (deltaM-fmap f) tailDeltaM (deltaM d))) ⟩ |
252 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d | 252 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d |
253 deltaM-left-unity-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = begin | 253 deltaM-left-unity-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = begin |
254 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ | 254 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ |
255 deltaM-mu (deltaM (mono (fmap F deltaM-eta x))) ≡⟨ refl ⟩ | 255 deltaM-mu (deltaM (mono (fmap F deltaM-eta x))) ≡⟨ refl ⟩ |
256 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-eta x))))))) ≡⟨ refl ⟩ | 256 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-eta x))))))) ≡⟨ refl ⟩ |
257 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-eta x)))) | 257 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-eta x)))) |
258 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-eta headDeltaM x)) ⟩ | 258 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-eta headDeltaM x)) ⟩ |
259 deltaM (mono (mu M (fmap F ((headDeltaM {n = O} {M = M}) ∙ deltaM-eta) x))) | 259 deltaM (mono (mu M (fmap F ((headDeltaM {n = O} {M = M}) ∙ deltaM-eta) x))) |
260 ≡⟨ refl ⟩ | 260 ≡⟨ refl ⟩ |
261 deltaM (mono (mu M (fmap F (eta M) x))) | 261 deltaM (mono (mu M (fmap F (eta M) x))) |
262 ≡⟨ cong (\de -> deltaM (mono de)) (left-unity-law M x) ⟩ | 262 ≡⟨ cong (\de -> deltaM (mono de)) (left-unity-law M x) ⟩ |
263 deltaM (mono x) | 263 deltaM (mono x) |
264 ∎ | 264 ∎ |
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 -} | |
298 | |
299 postulate deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} | |
300 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} | |
301 (f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) -> | |
302 deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d) | |
303 | |
304 deltaM-association-law : {l : Level} {A : Set l} {n : Nat} | 297 deltaM-association-law : {l : Level} {A : Set l} {n : Nat} |
305 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} | 298 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} |
306 (d : DeltaM M (DeltaM M (DeltaM M A (S n)) (S n)) (S n)) -> | 299 (d : DeltaM M (DeltaM M (DeltaM M A (S n)) (S n)) (S n)) -> |
307 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d) | 300 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d) |
308 deltaM-association-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = begin | 301 deltaM-association-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = begin |
337 deltaM-mu (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono x))))))) | 330 deltaM-mu (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono x))))))) |
338 ≡⟨ refl ⟩ | 331 ≡⟨ refl ⟩ |
339 deltaM-mu (deltaM-mu (deltaM (mono x))) | 332 deltaM-mu (deltaM-mu (deltaM (mono x))) |
340 | 333 |
341 ∎ | 334 ∎ |
342 deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = {!!} | 335 |
343 {- | |
344 deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin | 336 deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin |
345 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d))) | 337 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d))) |
346 ≡⟨ refl ⟩ | 338 ≡⟨ refl ⟩ |
347 deltaM-mu (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d))) | 339 deltaM-mu (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d))) |
348 ≡⟨ refl ⟩ | 340 ≡⟨ refl ⟩ |
445 deltaM-mu (deltaM (delta (mu M (fmap F headDeltaM (headDeltaM {M = M} (deltaM (delta x d))))) | 437 deltaM-mu (deltaM (delta (mu M (fmap F headDeltaM (headDeltaM {M = M} (deltaM (delta x d))))) |
446 (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d)))))))) | 438 (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d)))))))) |
447 ≡⟨ refl ⟩ | 439 ≡⟨ refl ⟩ |
448 deltaM-mu (deltaM-mu (deltaM (delta x d))) | 440 deltaM-mu (deltaM-mu (deltaM (delta x d))) |
449 ∎ | 441 ∎ |
450 -} | 442 |
451 | 443 |
452 {- | 444 |
453 | 445 |
454 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} | 446 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} |
455 {M : Set l -> Set l} | 447 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> |
456 (functorM : Functor M) | 448 Monad {l} (\A -> DeltaM M A (S n)) (deltaM-is-functor {l} {n}) |
457 (M : Monad M functorM) -> | 449 deltaM-is-monad {l} {A} {n} {T} {F} {M} = |
458 Monad {l} (\A -> DeltaM M {functorM} {M} A (S n)) (deltaM-is-functor {l} {n}) | |
459 deltaM-is-monad {l} {A} {n} {M} functorM M = | |
460 record { mu = deltaM-mu | 450 record { mu = deltaM-mu |
461 ; eta = deltaM-eta | 451 ; eta = deltaM-eta |
462 ; eta-is-nt = deltaM-eta-is-nt | 452 ; eta-is-nt = deltaM-eta-is-nt |
463 ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x))) | 453 ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x))) |
464 ; association-law = (deltaM-association-law M functorM M) | 454 ; association-law = deltaM-association-law |
465 ; left-unity-law = deltaM-left-unity-law | 455 ; left-unity-law = deltaM-left-unity-law |
466 ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) | 456 ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) |
467 } | 457 } |
468 | 458 |
469 | 459 |
470 | 460 |
471 -} | 461 |