Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/functor.agda @ 93:8d92ed54a94f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove functor-laws for deltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 19 Jan 2015 15:21:29 +0900
parents 4d615910c87a
children a271f3ff1922
comparison
equal deleted inserted replaced
92:4d615910c87a 93:8d92ed54a94f
14 14
15 deltaM-preserve-id : {l : Level} {A : Set l} 15 deltaM-preserve-id : {l : Level} {A : Set l}
16 {M : {l' : Level} -> Set l' -> Set l'} 16 {M : {l' : Level} -> Set l' -> Set l'}
17 (functorM : {l' : Level} -> Functor {l'} M) 17 (functorM : {l' : Level} -> Functor {l'} M)
18 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 18 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
19 -> (d : DeltaM M {functorM} {monadM} A) -> (deltaM-fmap id) d ≡ id d 19 -> (d : DeltaM M {functorM} {monadM} A) -> deltaM-fmap id d ≡ id d
20 deltaM-preserve-id functorM (deltaM (mono x)) = begin 20 deltaM-preserve-id functorM (deltaM (mono x)) = begin
21 deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩ 21 deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩
22 deltaM (fmap delta-is-functor (fmap functorM id) (mono x)) ≡⟨ refl ⟩ 22 deltaM (fmap delta-is-functor (fmap functorM id) (mono x)) ≡⟨ refl ⟩
23 deltaM (mono (fmap functorM id x)) ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id functorM x) ⟩ 23 deltaM (mono (fmap functorM id x)) ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id functorM x) ⟩
24 deltaM (mono (id x)) ≡⟨ cong (\x -> deltaM (mono x)) refl ⟩ 24 deltaM (mono (id x)) ≡⟨ cong (\x -> deltaM (mono x)) refl ⟩
39 appendDeltaM (deltaM (mono x)) (deltaM d) 39 appendDeltaM (deltaM (mono x)) (deltaM d)
40 ≡⟨ refl ⟩ 40 ≡⟨ refl ⟩
41 deltaM (delta x d) 41 deltaM (delta x d)
42 ∎ 42 ∎
43 43
44 {- 44
45 deltaM-covariant : {l : Level} {A B C : Set l} -> 45 deltaM-covariant : {l : Level} {A B C : Set l} ->
46 (f : B -> C) -> (g : A -> B) -> (d : Delta A) -> 46 {M : {l' : Level} -> Set l' -> Set l'}
47 (delta-fmap (f ∙ g)) d ≡ (delta-fmap f) (delta-fmap g d) 47 (functorM : {l' : Level} -> Functor {l'} M)
48 deltaM-covariant = {!!} 48 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
49 -} 49 (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A) ->
50 (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d
51 deltaM-covariant functorM f g (deltaM (mono x)) = begin
52 deltaM-fmap (f ∙ g) (deltaM (mono x)) ≡⟨ refl ⟩
53 deltaM (delta-fmap (fmap functorM (f ∙ g)) (mono x)) ≡⟨ refl ⟩
54 deltaM (mono (fmap functorM (f ∙ g) x)) ≡⟨ cong (\x -> (deltaM (mono x))) (covariant functorM g f x) ⟩
55 deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x)) ≡⟨ refl ⟩
56 deltaM-fmap f (deltaM-fmap g (deltaM (mono x))) ∎
57 deltaM-covariant functorM f g (deltaM (delta x d)) = begin
58 deltaM-fmap (f ∙ g) (deltaM (delta x d))
59 ≡⟨ refl ⟩
60 deltaM (delta-fmap (fmap functorM (f ∙ g)) (delta x d))
61 ≡⟨ refl ⟩
62 deltaM (delta (fmap functorM (f ∙ g) x) (delta-fmap (fmap functorM (f ∙ g)) d))
63 ≡⟨ refl ⟩
64 appendDeltaM (deltaM (mono (fmap functorM (f ∙ g) x))) (deltaM (delta-fmap (fmap functorM (f ∙ g)) d))
65 ≡⟨ refl ⟩
66 appendDeltaM (deltaM (mono (fmap functorM (f ∙ g) x))) (deltaM-fmap (f ∙ g) (deltaM d))
67 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-fmap (f ∙ g) (deltaM d))) (covariant functorM g f x) ⟩
68 appendDeltaM (deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x))) (deltaM-fmap (f ∙ g) (deltaM d))
69 ≡⟨ refl ⟩
70 appendDeltaM (deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x))) (deltaM-fmap (f ∙ g) (deltaM d))
71 ≡⟨ refl ⟩
72 appendDeltaM (deltaM (delta-fmap ((fmap functorM f) ∙ (fmap functorM g)) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d))
73 ≡⟨ refl ⟩
74 appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d))
75 ≡⟨ cong (\de -> appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) de) (deltaM-covariant functorM f g (deltaM d)) ⟩
76 appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) (((deltaM-fmap f) ∙ (deltaM-fmap g)) (deltaM d))
77 ≡⟨ refl ⟩
78 (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d))
79 ∎
80
81
82 deltaM-is-functor : {l : Level} {M : {l' : Level} -> Set l' -> Set l'}
83 {functorM : {l' : Level} -> Functor {l'} M }
84 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
85 -> Functor {l} (DeltaM M {functorM} {monadM})
86 deltaM-is-functor {_} {_} {functorM} = record { fmap = deltaM-fmap ;
87 preserve-id = deltaM-preserve-id functorM ;
88 covariant = (\f g -> deltaM-covariant functorM g f)}