Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/functor.agda @ 110:cd058dd89864

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Rewrite Functor-laws for DeltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 28 Jan 2015 22:36:34 +0900
parents ebd0d6e2772c
children 0a3b6cb91a05
comparison
equal deleted inserted replaced
109:5bd5f4a7ce8d 110:cd058dd89864
5 open import basic 5 open import basic
6 open import delta 6 open import delta
7 open import delta.functor 7 open import delta.functor
8 open import deltaM 8 open import deltaM
9 open import nat 9 open import nat
10 open import revision
11 open import laws 10 open import laws
12 open Functor 11 open Functor
13 12
14 module deltaM.functor where 13 module deltaM.functor where
15 14
16 15
17 deltaM-preserve-id : {l : Level} {A : Set l} {n : Rev} 16 deltaM-preserve-id : {l : Level} {A : Set l} {n : Nat}
18 {M : {l' : Level} -> Set l' -> Set l'} 17 {M : {l' : Level} -> Set l' -> Set l'}
19 (functorM : {l' : Level} -> Functor {l'} M) 18 (functorM : {l' : Level} -> Functor {l'} M)
20 {monadM : {l' : Level} -> Monad {l'} M functorM} 19 {monadM : {l' : Level} -> Monad {l'} M functorM}
21 -> (d : DeltaM M {functorM} {monadM} A n) -> deltaM-fmap id d ≡ id d 20 -> (d : DeltaM M {functorM} {monadM} A (S n)) -> deltaM-fmap id d ≡ id d
22 deltaM-preserve-id functorM (deltaM (mono x)) = begin 21 deltaM-preserve-id functorM (deltaM (mono x)) = begin
23 deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩ 22 deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩
24 deltaM (fmap delta-is-functor (fmap functorM id) (mono x)) ≡⟨ refl ⟩ 23 deltaM (fmap delta-is-functor (fmap functorM id) (mono x)) ≡⟨ refl ⟩
25 deltaM (mono (fmap functorM id x)) ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id functorM x) ⟩ 24 deltaM (mono (fmap functorM id x)) ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id functorM x) ⟩
26 deltaM (mono (id x)) ≡⟨ cong (\x -> deltaM (mono x)) refl ⟩ 25 deltaM (mono (id x)) ≡⟨ cong (\x -> deltaM (mono x)) refl ⟩
27 deltaM (mono x) ∎ 26 deltaM (mono x) ∎
28 deltaM-preserve-id functorM (deltaM (delta x d)) = begin 27 deltaM-preserve-id functorM (deltaM (delta x d)) = begin
29 deltaM-fmap id (deltaM (delta x d)) 28 deltaM-fmap id (deltaM (delta x d))
30 ≡⟨ refl ⟩ 29 ≡⟨ refl ⟩
31 deltaM (fmap delta-is-functor (fmap functorM id) (delta x d)) 30 deltaM (fmap delta-is-functor (fmap functorM id) (delta x d))
32 ≡⟨ refl ⟩ 31 ≡⟨ refl ⟩
33 deltaM (delta (fmap functorM id x) (fmap delta-is-functor (fmap functorM id) d)) 32 deltaM (delta (fmap functorM id x) (fmap delta-is-functor (fmap functorM id) d))
34 ≡⟨ cong (\x -> deltaM (delta x (fmap delta-is-functor (fmap functorM id) d))) (preserve-id functorM x) ⟩ 33 ≡⟨ cong (\x -> deltaM (delta x (fmap delta-is-functor (fmap functorM id) d))) (preserve-id functorM x) ⟩
35 deltaM (delta x (fmap delta-is-functor (fmap functorM id) d)) 34 deltaM (delta x (fmap delta-is-functor (fmap functorM id) d))
42 ≡⟨ refl ⟩ 41 ≡⟨ refl ⟩
43 deltaM (delta x d) 42 deltaM (delta x d)
44 ∎ 43 ∎
45 44
46 45
47 deltaM-covariant : {l : Level} {A B C : Set l} {n : Rev} -> 46 deltaM-covariant : {l : Level} {A B C : Set l} {n : Nat} ->
48 {M : {l' : Level} -> Set l' -> Set l'} 47 {M : {l' : Level} -> Set l' -> Set l'}
49 (functorM : {l' : Level} -> Functor {l'} M) 48 (functorM : {l' : Level} -> Functor {l'} M)
50 {monadM : {l' : Level} -> Monad {l'} M functorM} 49 {monadM : {l' : Level} -> Monad {l'} M functorM}
51 (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A n) -> 50 (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A (S n)) ->
52 (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d 51 (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d
53 deltaM-covariant functorM f g (deltaM (mono x)) = begin 52 deltaM-covariant functorM f g (deltaM (mono x)) = begin
54 deltaM-fmap (f ∙ g) (deltaM (mono x)) ≡⟨ refl ⟩ 53 deltaM-fmap (f ∙ g) (deltaM (mono x)) ≡⟨ refl ⟩
55 deltaM (delta-fmap (fmap functorM (f ∙ g)) (mono x)) ≡⟨ refl ⟩ 54 deltaM (delta-fmap (fmap functorM (f ∙ g)) (mono x)) ≡⟨ refl ⟩
56 deltaM (mono (fmap functorM (f ∙ g) x)) ≡⟨ cong (\x -> (deltaM (mono x))) (covariant functorM g f x) ⟩ 55 deltaM (mono (fmap functorM (f ∙ g) x)) ≡⟨ cong (\x -> (deltaM (mono x))) (covariant functorM g f x) ⟩
57 deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x)) ≡⟨ refl ⟩ 56 deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x)) ≡⟨ refl ⟩
58 deltaM-fmap f (deltaM-fmap g (deltaM (mono x))) ∎ 57 deltaM-fmap f (deltaM-fmap g (deltaM (mono x))) ∎
59 deltaM-covariant functorM f g (deltaM (delta x d)) = begin 58 deltaM-covariant functorM f g (deltaM (delta x d)) = begin
60 deltaM-fmap (f ∙ g) (deltaM (delta x d)) 59 deltaM-fmap (f ∙ g) (deltaM (delta x d))
61 ≡⟨ refl ⟩ 60 ≡⟨ refl ⟩
62 deltaM (delta-fmap (fmap functorM (f ∙ g)) (delta x d)) 61 deltaM (delta-fmap (fmap functorM (f ∙ g)) (delta x d))
63 ≡⟨ refl ⟩ 62 ≡⟨ refl ⟩
64 deltaM (delta (fmap functorM (f ∙ g) x) (delta-fmap (fmap functorM (f ∙ g)) d)) 63 deltaM (delta (fmap functorM (f ∙ g) x) (delta-fmap (fmap functorM (f ∙ g)) d))
65 ≡⟨ refl ⟩ 64 ≡⟨ refl ⟩
79 ≡⟨ refl ⟩ 78 ≡⟨ refl ⟩
80 (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d)) 79 (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d))
81 ∎ 80 ∎
82 81
83 82
84 deltaM-is-functor : {l : Level} {n : Rev} 83 deltaM-is-functor : {l : Level} {n : Nat}
85 {M : {l' : Level} -> Set l' -> Set l'} 84 {M : {l' : Level} -> Set l' -> Set l'}
86 {functorM : {l' : Level} -> Functor {l'} M } 85 {functorM : {l' : Level} -> Functor {l'} M }
87 {monadM : {l' : Level} -> Monad {l'} M functorM} 86 {monadM : {l' : Level} -> Monad {l'} M functorM}
88 -> Functor {l} (\A -> DeltaM M {functorM} {monadM} A n) 87 -> Functor {l} (\A -> DeltaM M {functorM} {monadM} A (S n))
89 deltaM-is-functor {_} {_} {_} {functorM} = record { fmap = deltaM-fmap ; 88 deltaM-is-functor {_} {_} {_} {functorM} = record { fmap = deltaM-fmap ;
90 preserve-id = deltaM-preserve-id functorM ; 89 preserve-id = deltaM-preserve-id functorM ;
91 covariant = (\f g -> deltaM-covariant functorM g f)} 90 covariant = (\f g -> deltaM-covariant functorM g f)}