diff agda/deltaM/functor.agda @ 93:8d92ed54a94f

Prove functor-laws for deltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 19 Jan 2015 15:21:29 +0900
parents 4d615910c87a
children a271f3ff1922
line wrap: on
line diff
--- a/agda/deltaM/functor.agda	Mon Jan 19 14:32:07 2015 +0900
+++ b/agda/deltaM/functor.agda	Mon Jan 19 15:21:29 2015 +0900
@@ -16,7 +16,7 @@
                       {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
+                      -> (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 ⟩
@@ -41,9 +41,48 @@
   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
+                   {M : {l' : Level} -> Set l' -> Set l'}
+                   (functorM : {l' : Level} -> Functor {l'} M)
+                   {monadM   : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
+                   (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A) ->
+                   (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d
+deltaM-covariant functorM f g (deltaM (mono x))    = begin
+  deltaM-fmap (f ∙ g) (deltaM (mono x))                     ≡⟨ refl ⟩ 
+  deltaM (delta-fmap (fmap functorM (f ∙ g)) (mono x))      ≡⟨ refl ⟩ 
+  deltaM (mono (fmap functorM (f ∙ g) x))                   ≡⟨ cong (\x -> (deltaM (mono x))) (covariant functorM g f x) ⟩ 
+  deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x)) ≡⟨ refl ⟩ 
+  deltaM-fmap f (deltaM-fmap g (deltaM (mono x)))           ∎
+deltaM-covariant functorM f g (deltaM (delta x d)) = begin
+  deltaM-fmap (f ∙ g) (deltaM (delta x d))               
+  ≡⟨ refl ⟩
+  deltaM (delta-fmap (fmap functorM (f ∙ g)) (delta x d))
+  ≡⟨ refl ⟩
+  deltaM (delta (fmap functorM (f ∙ g) x) (delta-fmap (fmap functorM (f ∙ g)) d))
+  ≡⟨ refl ⟩
+  appendDeltaM (deltaM (mono (fmap functorM (f ∙ g) x))) (deltaM (delta-fmap (fmap functorM (f ∙ g)) d))
+  ≡⟨ refl ⟩
+  appendDeltaM (deltaM (mono (fmap functorM (f ∙ g) x))) (deltaM-fmap (f ∙ g) (deltaM d))
+  ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-fmap (f ∙ g) (deltaM d))) (covariant functorM g f x)  ⟩
+  appendDeltaM (deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x))) (deltaM-fmap (f ∙ g) (deltaM d))
+  ≡⟨ refl ⟩
+  appendDeltaM (deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x))) (deltaM-fmap (f ∙ g) (deltaM d))
+  ≡⟨ refl ⟩
+  appendDeltaM (deltaM (delta-fmap ((fmap functorM f) ∙ (fmap functorM g)) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d))
+  ≡⟨ refl ⟩
+  appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d))
+  ≡⟨ cong (\de ->  appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) de) (deltaM-covariant functorM f g (deltaM d)) ⟩
+  appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) (((deltaM-fmap f) ∙ (deltaM-fmap g)) (deltaM d))
+  ≡⟨ refl ⟩
+  (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d))
+  ∎
+
+
+deltaM-is-functor : {l : Level} {M : {l' : Level} -> Set l' -> Set l'}
+                                {functorM : {l' : Level} -> Functor {l'} M }
+                                {monadM   : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
+                    -> Functor {l} (DeltaM M {functorM} {monadM}) 
+deltaM-is-functor {_} {_} {functorM} = record { fmap        = deltaM-fmap ;
+                             preserve-id  = deltaM-preserve-id functorM ;
+                             covariant    = (\f g -> deltaM-covariant functorM g f)}
\ No newline at end of file