Mercurial > hg > Members > atton > delta_monad
diff agda/deltaM/monad.agda @ 126:5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 03 Feb 2015 11:45:33 +0900 |
| parents | 6dcc68ef8f96 |
| children | d56596e4e784 |
line wrap: on
line diff
--- a/agda/deltaM/monad.agda Mon Feb 02 14:09:30 2015 +0900 +++ b/agda/deltaM/monad.agda Tue Feb 03 11:45:33 2015 +0900 @@ -25,6 +25,19 @@ deconstruct-id {n = O} (deltaM x) = refl deconstruct-id {n = S n} (deltaM x) = refl +headDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat} + {T : Set l -> Set l} {F : Functor T} {M : Monad T F} + (f : A -> B) -> (x : (DeltaM M A (S n))) -> + ((fmap F f) ∙ headDeltaM) x ≡ (headDeltaM ∙ (deltaM-fmap f)) x +headDeltaM-with-f {n = O} f (deltaM (mono x)) = refl +headDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl + +tailDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat} + {T : Set l -> Set l} {F : Functor T} {M : Monad T F} + (f : A -> B) -> (d : (DeltaM M A (S (S n)))) -> + (tailDeltaM ∙ (deltaM-fmap f)) d ≡ ((deltaM-fmap f) ∙ tailDeltaM) d +tailDeltaM-with-f {n = O} f (deltaM (delta x d)) = refl +tailDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} @@ -91,12 +104,26 @@ -postulate deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} +deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} {T : Set l -> Set l} {F : Functor T} {M : Monad T F} (f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) -> deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d) +deltaM-mu-is-nt {l} {A} {B} {O} {T} {F} {M} f (deltaM (mono x)) = {- deltaM-mu-is-nt {l} {A} {B} {O} {T} {F} {M} f (deltaM (mono x)) = begin + deltaM-fmap f (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ + deltaM-fmap f (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono x))))))) ≡⟨ refl ⟩ + deltaM-fmap f (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x)))) ≡⟨ refl ⟩ + deltaM (mono (fmap F f (mu M (fmap F (headDeltaM {M = M}) x)))) ≡⟨ {!!} ⟩ + deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x)))) ≡⟨ refl ⟩ + deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x))))))) ≡⟨ refl ⟩ + deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x))) ≡⟨ refl ⟩ + deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x))) ≡⟨ refl ⟩ + deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (mono x))) + ∎ +-} + + begin deltaM-fmap f (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ deltaM-fmap f (deltaM (mono (mu M (fmap F headDeltaM x)))) @@ -104,26 +131,83 @@ deltaM (mono (fmap F f (mu M (fmap F headDeltaM x)))) ≡⟨ cong (\de -> deltaM (mono de)) (sym (mu-is-nt M f (fmap F headDeltaM x))) ⟩ deltaM (mono (mu M (fmap F (fmap F f) (fmap F headDeltaM x)))) - ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F headDeltaM (fmap F f) x)) ⟩ + ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F headDeltaM (fmap F f) x)) ⟩ deltaM (mono (mu M (fmap F ((fmap F f) ∙ headDeltaM) x))) - ≡⟨ {!!} ⟩ - deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))) - ≡⟨ {!!} ⟩ + ≡⟨ cong (\de -> deltaM (mono (mu M de))) (fmap-equiv F (headDeltaM-with-f f) x) ⟩ deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))) ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F (deltaM-fmap f) (headDeltaM) x) ⟩ - deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x)))) + deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x)))) ≡⟨ refl ⟩ - deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x))))))) - ≡⟨ refl ⟩ + deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x))))))) + ≡⟨ refl ⟩ deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x))) ≡⟨ refl ⟩ deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (mono x))) ∎ -deltaM-mu-is-nt {n = S n} f (deltaM (delta x d)) = {!!} --} +deltaM-mu-is-nt {l} {A} {B} {S n} {T} {F} {M} f (deltaM (delta x d)) = begin + deltaM-fmap f (deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩ + deltaM-fmap f (deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta x d))))) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d)))))))) + ≡⟨ refl ⟩ + deltaM-fmap f (deltaM (delta (mu M (fmap F (headDeltaM {M = M}) x)) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) + ≡⟨ refl ⟩ + deltaM (delta (fmap F f (mu M (fmap F (headDeltaM {M = M}) x))) + (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) + ≡⟨ cong (\de -> deltaM (delta de + (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))) + (sym (mu-is-nt M f (fmap F headDeltaM x))) ⟩ + deltaM (delta (mu M (fmap F (fmap F f) (fmap F (headDeltaM {M = M}) x))) + (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) + ≡⟨ cong (\de -> deltaM (delta (mu M de) (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))) + (sym (covariant F headDeltaM (fmap F f) x)) ⟩ + deltaM (delta (mu M (fmap F ((fmap F f) ∙ (headDeltaM {M = M})) x)) + (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) + ≡⟨ cong (\de -> deltaM (delta (mu M de) (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))) + (fmap-equiv F (headDeltaM-with-f f) x) ⟩ + deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) + (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) + ≡⟨ refl ⟩ + deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) + (unDeltaM {M = M} (deltaM-fmap f (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) + ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM de))) + (deltaM-mu-is-nt {l} {A} {B} {n} {T} {F} {M} f (deltaM-fmap tailDeltaM (deltaM d))) ⟩ + deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (deltaM-fmap {n = n} f) (deltaM-fmap {n = n} (tailDeltaM {n = n}) (deltaM d)))))) + ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de)))) + (sym (deltaM-covariant (deltaM-fmap f) tailDeltaM (deltaM d))) ⟩ + deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap {n = n} ((deltaM-fmap {n = n} f) ∙ (tailDeltaM {n = n})) (deltaM d))))) + + ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de)))) + (sym (deltaM-fmap-equiv (tailDeltaM-with-f f) (deltaM d))) ⟩ + deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM ∙ (deltaM-fmap f)) (deltaM d))))) + ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de)))) + (deltaM-covariant tailDeltaM (deltaM-fmap f) (deltaM d)) ⟩ + deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-fmap (deltaM-fmap f) (deltaM d)))))) + ≡⟨ refl ⟩ + deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d)))))) + ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d))))))) + (covariant F (deltaM-fmap f) headDeltaM x) ⟩ + deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x))) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d)))))) + ≡⟨ refl ⟩ + deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d)))))) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d)))))))) + ≡⟨ refl ⟩ + deltaM-mu (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d))) + ≡⟨ refl ⟩ + deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (delta x d))) + ∎ + + +{- deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat} {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> (d : DeltaM M A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d @@ -154,10 +238,10 @@ ≡⟨ refl ⟩ deltaM (delta (mu M (eta M x)) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))) - ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))) + ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))) (sym (right-unity-law M x)) ⟩ deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))) - ≡⟨ refl ⟩ + ≡⟨ refl ⟩ deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-fmap (fmap F tailDeltaM) (delta-eta (eta M (deltaM (delta x d))))))))) ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM de))))) (sym (delta-eta-is-nt (fmap F tailDeltaM) (eta M (deltaM (delta x d))))) ⟩ @@ -177,7 +261,7 @@ -{- + postulate deltaM-left-unity-law : {l : Level} {A : Set l}