# HG changeset patch # User Yasutaka Higa # 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