# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1421632834 -32400
# Node ID 6789c65a75bc5041a530e6cfdb713b1e4924ca36
# Parent  5c083ddd73ed7ccb68a7746d91f917c3d4f80277
Split functor-proofs into delta.functor

diff -r 5c083ddd73ed -r 6789c65a75bc agda/delta.agda
--- a/agda/delta.agda	Sun Jan 18 20:59:27 2015 +0900
+++ b/agda/delta.agda	Mon Jan 19 11:00:34 2015 +0900
@@ -1,6 +1,7 @@
 open import list
 open import basic
 open import nat
+open import laws
 
 open import Level
 open import Relation.Binary.PropositionalEquality
@@ -9,7 +10,7 @@
 module delta where
 
 
-data Delta {l : Level} (A : Set l) : (Set (suc l)) where
+data Delta {l : Level} (A : Set l) : (Set l) where
   mono    : A -> Delta A
   delta   : A -> Delta A -> Delta A
 
@@ -130,21 +131,8 @@
 
 
 
--- Functor-laws
 
--- Functor-law-1 : T(id) = id'
-functor-law-1 :  {l : Level} {A : Set l} ->  (d : Delta A) -> (fmap id) d ≡ id d
-functor-law-1 (mono x)    = refl
-functor-law-1 (delta x d) = cong (delta x) (functor-law-1 d)
-
--- Functor-law-2 : T(f . g) = T(f) . T(g)
-functor-law-2 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
-                (f : B -> C) -> (g : A -> B) -> (d : Delta A) ->
-                (fmap (f ∙ g)) d ≡ ((fmap f) ∙ (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)
-
-
+{-
 -- Monad-laws (Category)
 
 monad-law-1-5 : {l : Level} {A : Set l} -> (m : Nat) (n : Nat) -> (ds : Delta (Delta A)) ->
@@ -481,3 +469,4 @@
 monad-law-h-3 (delta x d) k h = {!!}
 
 -}
+-}
diff -r 5c083ddd73ed -r 6789c65a75bc agda/delta/functor.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/delta/functor.agda	Mon Jan 19 11:00:34 2015 +0900
@@ -0,0 +1,28 @@
+open import delta
+open import basic
+open import laws
+
+open import Level
+open import Relation.Binary.PropositionalEquality
+
+
+module delta.functor where
+
+-- Functor-laws
+
+-- Functor-law-1 : T(id) = id'
+functor-law-1 :  {l : Level} {A : Set l} ->  (d : Delta A) -> (fmap id) d ≡ id d
+functor-law-1 (mono x)    = refl
+functor-law-1 (delta x d) = cong (delta x) (functor-law-1 d)
+
+-- Functor-law-2 : T(f . g) = T(f) . T(g)
+functor-law-2 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
+                (f : B -> C) -> (g : A -> B) -> (d : Delta A) ->
+                (fmap (f ∙ g)) d ≡ (fmap f) (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)
+
+delta-is-functor : {l : Level} -> Functor (Delta {l})
+delta-is-functor = record {  fmap = fmap ;
+                             preserve-id = functor-law-1;
+                             covariant  = \f g -> functor-law-2 g f}
diff -r 5c083ddd73ed -r 6789c65a75bc agda/laws.agda
--- a/agda/laws.agda	Sun Jan 18 20:59:27 2015 +0900
+++ b/agda/laws.agda	Mon Jan 19 11:00:34 2015 +0900
@@ -10,7 +10,7 @@
   field
     preserve-id : ∀{A} (x : F A) → fmap id x ≡ id x
     covariant   : ∀{A B C} (f : A -> B) -> (g : B -> C) -> (x : F A)
-                    -> fmap (g ∙ f) x ≡ fmap g (fmap f x)
+                    -> fmap (g ∙ f) x ≡ ((fmap g) ∙  (fmap f)) x
 open Functor