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