# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1422847070 -32400
# Node ID ee7f5162ec1f6af97677c632d8499c8c869a955c
# Parent  e1900c89dea99f3a83c87264fe4ef2d02cd9b88d
Fix proof functor for DeltaM

diff -r e1900c89dea9 -r ee7f5162ec1f agda/deltaM/functor.agda
--- a/agda/deltaM/functor.agda	Mon Feb 02 12:12:14 2015 +0900
+++ b/agda/deltaM/functor.agda	Mon Feb 02 12:17:50 2015 +0900
@@ -14,67 +14,63 @@
 
 
 deltaM-preserve-id :  {l : Level} {A : Set l} {n : Nat}
-                      {M : Set l -> Set l}
-                      (functorM : Functor  M)
-                      {monadM   : Monad  M functorM}
-                      -> (d : DeltaM M {functorM} {monadM} A (S n)) -> 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
+                      {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
+                      -> (d : DeltaM M A (S n)) -> deltaM-fmap id d ≡ id d
+deltaM-preserve-id {F = F}  (deltaM (mono x))  = begin
+  deltaM-fmap id (deltaM (mono x))                    ≡⟨ refl ⟩
+  deltaM (fmap delta-is-functor (fmap F id) (mono x)) ≡⟨ refl ⟩
+  deltaM (mono (fmap F id x))                         ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id F x) ⟩
+  deltaM (mono (id x))                                ≡⟨ cong (\x -> deltaM (mono x)) refl ⟩
+  deltaM (mono x)                                     ∎
+deltaM-preserve-id {F = F} (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 (fmap delta-is-functor (fmap F id) (delta x d))
   ≡⟨ refl ⟩
-  deltaM (delta (fmap functorM id x) (fmap delta-is-functor (fmap functorM id) d))
-  ≡⟨ cong (\x -> deltaM (delta x (fmap delta-is-functor (fmap functorM id) d))) (preserve-id functorM x) ⟩
-  deltaM (delta x (fmap delta-is-functor (fmap functorM id) d))
+  deltaM (delta (fmap F id x) (fmap delta-is-functor (fmap F id) d))
+  ≡⟨ cong (\x -> deltaM (delta x (fmap delta-is-functor (fmap F id) d))) (preserve-id F x) ⟩
+  deltaM (delta x (fmap delta-is-functor (fmap F id) d))
   ≡⟨ refl ⟩
-  appendDeltaM (deltaM (mono x)) (deltaM (fmap delta-is-functor (fmap functorM id) d))
+  appendDeltaM (deltaM (mono x)) (deltaM (fmap delta-is-functor (fmap F id) d))
   ≡⟨ refl ⟩
   appendDeltaM (deltaM (mono x)) (deltaM-fmap id (deltaM d))
-  ≡⟨ cong (\d -> appendDeltaM (deltaM (mono x)) d) (deltaM-preserve-id functorM (deltaM d)) ⟩
+  ≡⟨ cong (\d -> appendDeltaM (deltaM (mono x)) d) (deltaM-preserve-id {F = F} (deltaM d)) ⟩
   appendDeltaM (deltaM (mono x)) (deltaM d)
   ≡⟨ refl ⟩
   deltaM (delta x d)
   ∎
 
 
-deltaM-covariant : {l : Level} {A B C : Set l} {n : Nat} ->
-                   {M : Set l -> Set l}
-                   (functorM : Functor M)
-                   {monadM   : Monad M functorM}
-                   (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A (S n)) ->
+deltaM-covariant : {l : Level} {A B C : Set l} {n : Nat}
+                   {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
+                   (f : B -> C) -> (g : A -> B) -> (d : DeltaM M A (S n)) ->
                    (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-covariant {F = F} f g (deltaM (mono x))    = begin
+  deltaM-fmap (f ∙ g) (deltaM (mono x))              ≡⟨ refl ⟩
+  deltaM (delta-fmap (fmap F (f ∙ g)) (mono x))      ≡⟨ refl ⟩
+  deltaM (mono (fmap F (f ∙ g) x))                   ≡⟨ cong (\x -> (deltaM (mono x))) (covariant F g f x) ⟩
+  deltaM (mono (((fmap F f) ∙ (fmap F g)) x))        ≡⟨ refl ⟩
   deltaM-fmap f (deltaM-fmap g (deltaM (mono x)))           ∎
-deltaM-covariant functorM f g (deltaM (delta x d)) = begin
+deltaM-covariant {F = F} 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))
+  deltaM (delta-fmap (fmap F (f ∙ g)) (delta x d))
   ≡⟨ refl ⟩
-  deltaM (delta (fmap functorM (f ∙ g) x) (delta-fmap (fmap functorM (f ∙ g)) d))
+  deltaM (delta (fmap F (f ∙ g) x) (delta-fmap (fmap F (f ∙ g)) d))
   ≡⟨ refl ⟩
-  appendDeltaM (deltaM (mono (fmap functorM (f ∙ g) x))) (deltaM (delta-fmap (fmap functorM (f ∙ g)) d))
+  appendDeltaM (deltaM (mono (fmap F (f ∙ g) x))) (deltaM (delta-fmap (fmap F (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))
+  appendDeltaM (deltaM (mono (fmap F (f ∙ g) x))) (deltaM-fmap (f ∙ g) (deltaM d))
+  ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-fmap (f ∙ g) (deltaM d))) (covariant F g f x)  ⟩
+  appendDeltaM (deltaM (mono (((fmap F f) ∙ (fmap F 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))
+  appendDeltaM (deltaM (mono (((fmap F f) ∙ (fmap F 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))
+  appendDeltaM (deltaM (delta-fmap ((fmap F f) ∙ (fmap F 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))
+  appendDeltaM (deltaM ((((delta-fmap (fmap F f)) ∙ (delta-fmap (fmap F g)))) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d))
+  ≡⟨ cong (\de ->  appendDeltaM (deltaM ((((delta-fmap (fmap F f)) ∙ (delta-fmap (fmap F g)))) (mono x))) de) (deltaM-covariant {F = F} f g (deltaM d)) ⟩
+  appendDeltaM (deltaM ((((delta-fmap (fmap F f)) ∙ (delta-fmap (fmap F g)))) (mono x))) (((deltaM-fmap f) ∙ (deltaM-fmap g)) (deltaM d))
   ≡⟨ refl ⟩
   (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d))
   ∎
@@ -82,11 +78,11 @@
 
 
 deltaM-is-functor : {l : Level} {n : Nat}
-                                {M : Set l -> Set l}
-                                {functorM : Functor M }
-                                {monadM   : Monad M functorM}
-                    -> Functor {l} (\A -> DeltaM M {functorM} {monadM} A (S n))
-deltaM-is-functor {_} {_} {_} {functorM} = record { fmap         = deltaM-fmap ;
-                                                    preserve-id  = deltaM-preserve-id functorM ;
-                                                    covariant    = (\f g -> deltaM-covariant functorM g f)
-                                                    }
+                    {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
+                    Functor {l} (\A -> DeltaM M A (S n))
+deltaM-is-functor {F = F} = record { fmap         = deltaM-fmap
+                                   ; preserve-id  = deltaM-preserve-id {F = F}
+                                   ; covariant    = (\f g -> deltaM-covariant {F = F} g f)
+                                   }
+
+