Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/monad.agda @ 131:d205ff1e406f InfiniteDeltaWithMonad

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Cleanup proofs
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 12:57:13 +0900
parents ac45d065cbf2
children 575de2e38385
comparison
equal deleted inserted replaced
130:ac45d065cbf2 131:d205ff1e406f
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
35 tailDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat} 36 tailDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat}
36 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} 37 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
37 (f : A -> B) -> (d : (DeltaM M A (S (S n)))) -> 38 (f : A -> B) -> (d : (DeltaM M A (S (S n)))) ->
38 (tailDeltaM ∙ (deltaM-fmap f)) d ≡ ((deltaM-fmap f) ∙ tailDeltaM) d 39 (tailDeltaM ∙ (deltaM-fmap f)) d ≡ ((deltaM-fmap f) ∙ tailDeltaM) d
39 tailDeltaM-with-f {n = O} f (deltaM (delta x d)) = refl 40 tailDeltaM-with-f {n = O} f (deltaM (delta x d)) = refl
40 tailDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl 41 tailDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl
41
42 headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
43 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
44 (x : DeltaM M A (S n)) ->
45 ((headDeltaM {n = n} {M = M}) ∙ deltaM-eta) x ≡ eta M x
46 headDeltaM-with-deltaM-eta {n = O} (deltaM (mono x)) = refl
47 headDeltaM-with-deltaM-eta {n = S n} (deltaM (delta x d)) = refl
48
49
50 fmap-tailDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
51 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
52 (d : DeltaM M A (S n)) ->
53 deltaM-fmap ((tailDeltaM {n = n} {M = M} ) ∙ deltaM-eta) d ≡ deltaM-fmap (deltaM-eta) d
54 fmap-tailDeltaM-with-deltaM-eta {n = O} d = refl
55 fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl
56 42
57 43
58 44
59 fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat} 45 fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat}
60 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> 46 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
453 ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x))) 439 ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x)))
454 ; association-law = deltaM-association-law 440 ; association-law = deltaM-association-law
455 ; left-unity-law = deltaM-left-unity-law 441 ; left-unity-law = deltaM-left-unity-law
456 ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) 442 ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x)))
457 } 443 }
458
459
460
461