### diff agda/delta.agda @ 87:6789c65a75bc

Split functor-proofs into delta.functor
author Yasutaka Higa Mon, 19 Jan 2015 11:00:34 +0900 fc5cd8c50312 526186c4f298
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)
-
-
+{-