Mercurial > hg > Members > atton > delta_monad

comparison agda/delta/functor.agda @ 131:d205ff1e406f InfiniteDeltaWithMonad

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 }