Mercurial > hg > Members > atton > delta_monad
comparison agda/delta/functor.agda @ 131:d205ff1e406f InfiniteDeltaWithMonad
Cleanup proofs
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 03 Feb 2015 12:57:13 +0900 |
parents | 5902b2a24abf |
children |
comparison
equal
deleted
inserted
replaced
130:ac45d065cbf2 | 131:d205ff1e406f |
---|---|
9 | 9 |
10 module delta.functor where | 10 module delta.functor where |
11 | 11 |
12 -- Functor-laws | 12 -- Functor-laws |
13 | 13 |
14 -- Functor-law-1 : T(id) = id' | 14 -- functor-law 1 : T(id) = id' |
15 functor-law-1 : {l : Level} {A : Set l} {n : Nat} -> (d : Delta A (S n)) -> (delta-fmap id) d ≡ id d | 15 delta-preserve-id : {l : Level} {A : Set l} {n : Nat} -> (d : Delta A (S n)) -> (delta-fmap id) d ≡ id d |
16 functor-law-1 (mono x) = refl | 16 delta-preserve-id (mono x) = refl |
17 functor-law-1 (delta x d) = cong (delta x) (functor-law-1 d) | 17 delta-preserve-id (delta x d) = cong (delta x) (delta-preserve-id d) |
18 | 18 |
19 -- Functor-law-2 : T(f . g) = T(f) . T(g) | 19 |
20 functor-law-2 : {l : Level} {n : Nat} {A B C : Set l} -> | 20 -- functor-law 2 : T(f . g) = T(f) . T(g) |
21 delta-covariant : {l : Level} {n : Nat} {A B C : Set l} -> | |
21 (f : B -> C) -> (g : A -> B) -> (d : Delta A (S n)) -> | 22 (f : B -> C) -> (g : A -> B) -> (d : Delta A (S n)) -> |
22 (delta-fmap (f ∙ g)) d ≡ ((delta-fmap f) ∙ (delta-fmap g)) d | 23 (delta-fmap (f ∙ g)) d ≡ ((delta-fmap f) ∙ (delta-fmap g)) d |
23 functor-law-2 f g (mono x) = refl | 24 delta-covariant f g (mono x) = refl |
24 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d) | 25 delta-covariant f g (delta x d) = cong (delta (f (g x))) (delta-covariant f g d) |
25 | 26 |
26 | 27 |
27 delta-fmap-equiv : {l : Level} {A B : Set l} {n : Nat} {f g : A -> B} | 28 delta-fmap-equiv : {l : Level} {A B : Set l} {n : Nat} {f g : A -> B} |
28 (eq : (x : A) -> f x ≡ g x) -> (d : Delta A (S n)) -> | 29 (eq : (x : A) -> f x ≡ g x) -> (d : Delta A (S n)) -> |
29 delta-fmap f d ≡ delta-fmap g d | 30 delta-fmap f d ≡ delta-fmap g d |
30 delta-fmap-equiv {l} {A} {B} {O} {f} {g} eq (mono x) = begin | 31 delta-fmap-equiv {l} {A} {B} {O} {f} {g} eq (mono x) = begin |
31 mono (f x) ≡⟨ cong mono (eq x) ⟩ | 32 mono (f x) ≡⟨ cong mono (eq x) ⟩ |
32 mono (g x) | 33 mono (g x) |
39 | 40 |
40 | 41 |
41 | 42 |
42 delta-is-functor : {l : Level} {n : Nat} -> Functor {l} (\A -> Delta A (S n)) | 43 delta-is-functor : {l : Level} {n : Nat} -> Functor {l} (\A -> Delta A (S n)) |
43 delta-is-functor = record { fmap = delta-fmap | 44 delta-is-functor = record { fmap = delta-fmap |
44 ;preserve-id = functor-law-1 | 45 ; preserve-id = delta-preserve-id |
45 ; covariant = \f g -> functor-law-2 g f | 46 ; covariant = \f g -> delta-covariant g f |
46 ; fmap-equiv = delta-fmap-equiv | 47 ; fmap-equiv = delta-fmap-equiv |
47 } | 48 } |