Mercurial > hg > Members > atton > delta_monad

changeset 93:8d92ed54a94f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 bcd4fe52a504
files agda/delta/functor.agda agda/deltaM/functor.agda
diffstat 2 files changed, 46 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/agda/delta/functor.agda	Mon Jan 19 14:32:07 2015 +0900
+++ b/agda/delta/functor.agda	Mon Jan 19 15:21:29 2015 +0900
@@ -18,7 +18,7 @@
 -- Functor-law-2 : T(f . g) = T(f) . T(g)
 functor-law-2 : {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)
+                (delta-fmap (f ∙ g)) d ≡ ((delta-fmap f) ∙ (delta-fmap g)) d
 functor-law-2 f g (mono x)    = refl
 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d)
 
--- 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