Mercurial > hg > Members > atton > delta_monad
changeset 91:f41682b53992
Prove deltaM-preserve-id by mono
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 19 Jan 2015 12:29:29 +0900 |
| parents | 55d11ce7e223 |
| children | 4d615910c87a |
| files | agda/deltaM/functor.agda |
| diffstat | 1 files changed, 37 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/agda/deltaM/functor.agda Mon Jan 19 12:29:29 2015 +0900 @@ -0,0 +1,37 @@ +open import Level +open import Relation.Binary.PropositionalEquality +open ≡-Reasoning + +open import basic +open import delta +open import delta.functor +open import deltaM +open import laws +open Functor + +module deltaM.functor where + + +deltaM-preserve-id : {l : Level} {A : Set l} + {M : {l' : Level} -> Set l' -> Set l'} + (functorM : {l' : Level} -> Functor {l'} M) + {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} + -> (d : DeltaM M {functorM} {monadM} A) -> (deltaM-fmap id) d ≡ id d +deltaM-preserve-id functorM (deltaM (mono x)) = begin + deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩ + deltaM (fmap delta-is-functor (fmap functorM id) (mono x)) ≡⟨ refl ⟩ + deltaM (mono (fmap functorM id x)) ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id functorM x) ⟩ + deltaM (mono (id x)) ≡⟨ cong (\x -> deltaM (mono x)) refl ⟩ + deltaM (mono x) ∎ +deltaM-preserve-id functorM (deltaM (delta x d)) = begin + deltaM-fmap id (deltaM (delta x d)) ≡⟨ refl ⟩ + deltaM (fmap delta-is-functor (fmap functorM id) (delta x d)) ≡⟨ {!!} ⟩ + deltaM (delta x d) + ∎ + +{- +deltaM-covariant : {l : Level} {A B C : Set l} -> + (f : B -> C) -> (g : A -> B) -> (d : Delta A) -> + (delta-fmap (f ∙ g)) d ≡ (delta-fmap f) (delta-fmap g d) +deltaM-covariant = {!!} +-} \ No newline at end of file