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

Split functor-proofs into delta.functor
author Yasutaka Higa Mon, 19 Jan 2015 11:00:34 +0900 fc5cd8c50312 526186c4f298
comparison
equal inserted replaced
86:5c083ddd73ed 87:6789c65a75bc
1 open import list 1 open import list
2 open import basic 2 open import basic
3 open import nat 3 open import nat
4 open import laws
4 5
5 open import Level 6 open import Level
6 open import Relation.Binary.PropositionalEquality 7 open import Relation.Binary.PropositionalEquality
7 open ≡-Reasoning 8 open ≡-Reasoning
8 9
9 module delta where 10 module delta where
10 11
11 12
12 data Delta {l : Level} (A : Set l) : (Set (suc l)) where 13 data Delta {l : Level} (A : Set l) : (Set l) where
13 mono : A -> Delta A 14 mono : A -> Delta A
14 delta : A -> Delta A -> Delta A 15 delta : A -> Delta A -> Delta A
15 16
16 deltaAppend : {l : Level} {A : Set l} -> Delta A -> Delta A -> Delta A 17 deltaAppend : {l : Level} {A : Set l} -> Delta A -> Delta A -> Delta A
17 deltaAppend (mono x) d = delta x d 18 deltaAppend (mono x) d = delta x d
128 fmap f (n-tail (S n) (delta x d)) ∎ 129 fmap f (n-tail (S n) (delta x d)) ∎
129 130
130 131
131 132
132 133
133 -- Functor-laws 134
134 135 {-
135 -- Functor-law-1 : T(id) = id'
136 functor-law-1 : {l : Level} {A : Set l} -> (d : Delta A) -> (fmap id) d ≡ id d
137 functor-law-1 (mono x) = refl
138 functor-law-1 (delta x d) = cong (delta x) (functor-law-1 d)
139
140 -- Functor-law-2 : T(f . g) = T(f) . T(g)
141 functor-law-2 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
142 (f : B -> C) -> (g : A -> B) -> (d : Delta A) ->
143 (fmap (f ∙ g)) d ≡ ((fmap f) ∙ (fmap g)) d
144 functor-law-2 f g (mono x) = refl
145 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d)
146
147