Mercurial > hg > Members > atton > delta_monad
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 -} |