comparison agda/delta/functor.agda @ 126:5902b2a24abf

Prove mu-is-nt for DeltaM with fmap-equiv
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 11:45:33 +0900
parents 47f144540d51
children d205ff1e406f
comparison
equal deleted inserted replaced
125:6dcc68ef8f96 126:5902b2a24abf
22 (delta-fmap (f ∙ g)) d ≡ ((delta-fmap f) ∙ (delta-fmap g)) d 22 (delta-fmap (f ∙ g)) d ≡ ((delta-fmap f) ∙ (delta-fmap g)) d
23 functor-law-2 f g (mono x) = refl 23 functor-law-2 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) 24 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d)
25 25
26 26
27 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 delta-fmap f d ≡ delta-fmap g d
30 delta-fmap-equiv {l} {A} {B} {O} {f} {g} eq (mono x) = begin
31 mono (f x) ≡⟨ cong mono (eq x) ⟩
32 mono (g x)
33
34 delta-fmap-equiv {l} {A} {B} {S n} {f} {g} eq (delta x d) = begin
35 delta (f x) (delta-fmap f d) ≡⟨ cong (\de -> delta de (delta-fmap f d)) (eq x) ⟩
36 delta (g x) (delta-fmap f d) ≡⟨ cong (\de -> delta (g x) de) (delta-fmap-equiv eq d) ⟩
37 delta (g x) (delta-fmap g d)
38
39
40
27 41
28 delta-is-functor : {l : Level} {n : Nat} -> Functor {l} (\A -> Delta A (S n)) 42 delta-is-functor : {l : Level} {n : Nat} -> Functor {l} (\A -> Delta A (S n))
29 delta-is-functor = record { fmap = delta-fmap ; 43 delta-is-functor = record { fmap = delta-fmap
30 preserve-id = functor-law-1; 44 ;preserve-id = functor-law-1
31 covariant = \f g -> functor-law-2 g f 45 ; covariant = \f g -> functor-law-2 g f
32 } 46 ; fmap-equiv = delta-fmap-equiv
47 }