Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/functor.agda @ 123:ee7f5162ec1f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix proof functor for DeltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 02 Feb 2015 12:17:50 +0900
parents 47f144540d51
children 5902b2a24abf
comparison
equal deleted inserted replaced
122:e1900c89dea9 123:ee7f5162ec1f
12 12
13 module deltaM.functor where 13 module deltaM.functor where
14 14
15 15
16 deltaM-preserve-id : {l : Level} {A : Set l} {n : Nat} 16 deltaM-preserve-id : {l : Level} {A : Set l} {n : Nat}
17 {M : Set l -> Set l} 17 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
18 (functorM : Functor M) 18 -> (d : DeltaM M A (S n)) -> deltaM-fmap id d ≡ id d
19 {monadM : Monad M functorM} 19 deltaM-preserve-id {F = F} (deltaM (mono x)) = begin
20 -> (d : DeltaM M {functorM} {monadM} A (S n)) -> deltaM-fmap id d ≡ id d 20 deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩
21 deltaM-preserve-id functorM (deltaM (mono x)) = begin 21 deltaM (fmap delta-is-functor (fmap F id) (mono x)) ≡⟨ refl ⟩
22 deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩ 22 deltaM (mono (fmap F id x)) ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id F x) ⟩
23 deltaM (fmap delta-is-functor (fmap functorM id) (mono x)) ≡⟨ refl ⟩ 23 deltaM (mono (id x)) ≡⟨ cong (\x -> deltaM (mono x)) refl ⟩
24 deltaM (mono (fmap functorM id x)) ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id functorM x) ⟩ 24 deltaM (mono x) ∎
25 deltaM (mono (id x)) ≡⟨ cong (\x -> deltaM (mono x)) refl ⟩ 25 deltaM-preserve-id {F = F} (deltaM (delta x d)) = begin
26 deltaM (mono x) ∎
27 deltaM-preserve-id functorM (deltaM (delta x d)) = begin
28 deltaM-fmap id (deltaM (delta x d)) 26 deltaM-fmap id (deltaM (delta x d))
29 ≡⟨ refl ⟩ 27 ≡⟨ refl ⟩
30 deltaM (fmap delta-is-functor (fmap functorM id) (delta x d)) 28 deltaM (fmap delta-is-functor (fmap F id) (delta x d))
31 ≡⟨ refl ⟩ 29 ≡⟨ refl ⟩
32 deltaM (delta (fmap functorM id x) (fmap delta-is-functor (fmap functorM id) d)) 30 deltaM (delta (fmap F id x) (fmap delta-is-functor (fmap F id) d))
33 ≡⟨ cong (\x -> deltaM (delta x (fmap delta-is-functor (fmap functorM id) d))) (preserve-id functorM x) ⟩ 31 ≡⟨ cong (\x -> deltaM (delta x (fmap delta-is-functor (fmap F id) d))) (preserve-id F x) ⟩
34 deltaM (delta x (fmap delta-is-functor (fmap functorM id) d)) 32 deltaM (delta x (fmap delta-is-functor (fmap F id) d))
35 ≡⟨ refl ⟩ 33 ≡⟨ refl ⟩
36 appendDeltaM (deltaM (mono x)) (deltaM (fmap delta-is-functor (fmap functorM id) d)) 34 appendDeltaM (deltaM (mono x)) (deltaM (fmap delta-is-functor (fmap F id) d))
37 ≡⟨ refl ⟩ 35 ≡⟨ refl ⟩
38 appendDeltaM (deltaM (mono x)) (deltaM-fmap id (deltaM d)) 36 appendDeltaM (deltaM (mono x)) (deltaM-fmap id (deltaM d))
39 ≡⟨ cong (\d -> appendDeltaM (deltaM (mono x)) d) (deltaM-preserve-id functorM (deltaM d)) ⟩ 37 ≡⟨ cong (\d -> appendDeltaM (deltaM (mono x)) d) (deltaM-preserve-id {F = F} (deltaM d)) ⟩
40 appendDeltaM (deltaM (mono x)) (deltaM d) 38 appendDeltaM (deltaM (mono x)) (deltaM d)
41 ≡⟨ refl ⟩ 39 ≡⟨ refl ⟩
42 deltaM (delta x d) 40 deltaM (delta x d)
43 ∎ 41 ∎
44 42
45 43
46 deltaM-covariant : {l : Level} {A B C : Set l} {n : Nat} -> 44 deltaM-covariant : {l : Level} {A B C : Set l} {n : Nat}
47 {M : Set l -> Set l} 45 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
48 (functorM : Functor M) 46 (f : B -> C) -> (g : A -> B) -> (d : DeltaM M A (S n)) ->
49 {monadM : Monad M functorM}
50 (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A (S n)) ->
51 (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d 47 (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d
52 deltaM-covariant functorM f g (deltaM (mono x)) = begin 48 deltaM-covariant {F = F} f g (deltaM (mono x)) = begin
53 deltaM-fmap (f ∙ g) (deltaM (mono x)) ≡⟨ refl ⟩ 49 deltaM-fmap (f ∙ g) (deltaM (mono x)) ≡⟨ refl ⟩
54 deltaM (delta-fmap (fmap functorM (f ∙ g)) (mono x)) ≡⟨ refl ⟩ 50 deltaM (delta-fmap (fmap F (f ∙ g)) (mono x)) ≡⟨ refl ⟩
55 deltaM (mono (fmap functorM (f ∙ g) x)) ≡⟨ cong (\x -> (deltaM (mono x))) (covariant functorM g f x) ⟩ 51 deltaM (mono (fmap F (f ∙ g) x)) ≡⟨ cong (\x -> (deltaM (mono x))) (covariant F g f x) ⟩
56 deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x)) ≡⟨ refl ⟩ 52 deltaM (mono (((fmap F f) ∙ (fmap F g)) x)) ≡⟨ refl ⟩
57 deltaM-fmap f (deltaM-fmap g (deltaM (mono x))) ∎ 53 deltaM-fmap f (deltaM-fmap g (deltaM (mono x))) ∎
58 deltaM-covariant functorM f g (deltaM (delta x d)) = begin 54 deltaM-covariant {F = F} f g (deltaM (delta x d)) = begin
59 deltaM-fmap (f ∙ g) (deltaM (delta x d)) 55 deltaM-fmap (f ∙ g) (deltaM (delta x d))
60 ≡⟨ refl ⟩ 56 ≡⟨ refl ⟩
61 deltaM (delta-fmap (fmap functorM (f ∙ g)) (delta x d)) 57 deltaM (delta-fmap (fmap F (f ∙ g)) (delta x d))
62 ≡⟨ refl ⟩ 58 ≡⟨ refl ⟩
63 deltaM (delta (fmap functorM (f ∙ g) x) (delta-fmap (fmap functorM (f ∙ g)) d)) 59 deltaM (delta (fmap F (f ∙ g) x) (delta-fmap (fmap F (f ∙ g)) d))
64 ≡⟨ refl ⟩ 60 ≡⟨ refl ⟩
65 appendDeltaM (deltaM (mono (fmap functorM (f ∙ g) x))) (deltaM (delta-fmap (fmap functorM (f ∙ g)) d)) 61 appendDeltaM (deltaM (mono (fmap F (f ∙ g) x))) (deltaM (delta-fmap (fmap F (f ∙ g)) d))
66 ≡⟨ refl ⟩ 62 ≡⟨ refl ⟩
67 appendDeltaM (deltaM (mono (fmap functorM (f ∙ g) x))) (deltaM-fmap (f ∙ g) (deltaM d)) 63 appendDeltaM (deltaM (mono (fmap F (f ∙ g) x))) (deltaM-fmap (f ∙ g) (deltaM d))
68 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-fmap (f ∙ g) (deltaM d))) (covariant functorM g f x) ⟩ 64 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-fmap (f ∙ g) (deltaM d))) (covariant F g f x) ⟩
69 appendDeltaM (deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x))) (deltaM-fmap (f ∙ g) (deltaM d)) 65 appendDeltaM (deltaM (mono (((fmap F f) ∙ (fmap F g)) x))) (deltaM-fmap (f ∙ g) (deltaM d))
70 ≡⟨ refl ⟩ 66 ≡⟨ refl ⟩
71 appendDeltaM (deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x))) (deltaM-fmap (f ∙ g) (deltaM d)) 67 appendDeltaM (deltaM (mono (((fmap F f) ∙ (fmap F g)) x))) (deltaM-fmap (f ∙ g) (deltaM d))
72 ≡⟨ refl ⟩ 68 ≡⟨ refl ⟩
73 appendDeltaM (deltaM (delta-fmap ((fmap functorM f) ∙ (fmap functorM g)) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d)) 69 appendDeltaM (deltaM (delta-fmap ((fmap F f) ∙ (fmap F g)) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d))
74 ≡⟨ refl ⟩ 70 ≡⟨ refl ⟩
75 appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d)) 71 appendDeltaM (deltaM ((((delta-fmap (fmap F f)) ∙ (delta-fmap (fmap F g)))) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d))
76 ≡⟨ cong (\de -> appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) de) (deltaM-covariant functorM f g (deltaM d)) ⟩ 72 ≡⟨ cong (\de -> appendDeltaM (deltaM ((((delta-fmap (fmap F f)) ∙ (delta-fmap (fmap F g)))) (mono x))) de) (deltaM-covariant {F = F} f g (deltaM d)) ⟩
77 appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) (((deltaM-fmap f) ∙ (deltaM-fmap g)) (deltaM d)) 73 appendDeltaM (deltaM ((((delta-fmap (fmap F f)) ∙ (delta-fmap (fmap F g)))) (mono x))) (((deltaM-fmap f) ∙ (deltaM-fmap g)) (deltaM d))
78 ≡⟨ refl ⟩ 74 ≡⟨ refl ⟩
79 (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d)) 75 (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d))
80 ∎ 76 ∎
81 77
82 78
83 79
84 deltaM-is-functor : {l : Level} {n : Nat} 80 deltaM-is-functor : {l : Level} {n : Nat}
85 {M : Set l -> Set l} 81 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
86 {functorM : Functor M } 82 Functor {l} (\A -> DeltaM M A (S n))
87 {monadM : Monad M functorM} 83 deltaM-is-functor {F = F} = record { fmap = deltaM-fmap
88 -> Functor {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) 84 ; preserve-id = deltaM-preserve-id {F = F}
89 deltaM-is-functor {_} {_} {_} {functorM} = record { fmap = deltaM-fmap ; 85 ; covariant = (\f g -> deltaM-covariant {F = F} g f)
90 preserve-id = deltaM-preserve-id functorM ; 86 }
91 covariant = (\f g -> deltaM-covariant functorM g f) 87
92 } 88