Mercurial > hg > Members > atton > delta_monad

changeset 87:6789c65a75bc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Split functor-proofs into delta.functor
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 19 Jan 2015 11:00:34 +0900
parents 5c083ddd73ed
children 526186c4f298
files agda/delta.agda agda/delta/functor.agda agda/laws.agda
diffstat 3 files changed, 33 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- 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 = {!!}
 
 -}
+-}
--- /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}
--- 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