Cleanup proofs
author Yasutaka Higa Tue, 03 Feb 2015 12:57:13 +0900 ac45d065cbf2 575de2e38385
comparison
equal 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
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 }