comparison agda/delta.agda @ 87:6789c65a75bc

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 fc5cd8c50312
children 526186c4f298
comparison
equal deleted 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
148 -- Monad-laws (Category) 136 -- Monad-laws (Category)
149 137
150 monad-law-1-5 : {l : Level} {A : Set l} -> (m : Nat) (n : Nat) -> (ds : Delta (Delta A)) -> 138 monad-law-1-5 : {l : Level} {A : Set l} -> (m : Nat) (n : Nat) -> (ds : Delta (Delta A)) ->
151 n-tail n (bind ds (n-tail m)) ≡ bind (n-tail n ds) (n-tail (m + n)) 139 n-tail n (bind ds (n-tail m)) ≡ bind (n-tail n ds) (n-tail (m + n))
152 monad-law-1-5 O O ds = refl 140 monad-law-1-5 O O ds = refl
479 (m >>= (\x -> k x >>= h)) ≡ ((m >>= k) >>= h) 467 (m >>= (\x -> k x >>= h)) ≡ ((m >>= k) >>= h)
480 monad-law-h-3 (mono x) k h = refl 468 monad-law-h-3 (mono x) k h = refl
481 monad-law-h-3 (delta x d) k h = {!!} 469 monad-law-h-3 (delta x d) k h = {!!}
482 470
483 -} 471 -}
472 -}