Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/monad.agda @ 114:08403eb8db8b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove natural transformation for deltaM-eta
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 30 Jan 2015 22:17:46 +0900
parents 0a3b6cb91a05
children e6bcc7467335
comparison
equal deleted inserted replaced
113:47f144540d51 114:08403eb8db8b
15 open Functor 15 open Functor
16 open NaturalTransformation 16 open NaturalTransformation
17 open Monad 17 open Monad
18 18
19 19
20 -- sub proofs
21
22 fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
23 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM}
24 (x : M A) -> (fmap functorM ((headDeltaM {l} {A} {n} {M} {functorM} {monadM}) ∙ deltaM-eta) x) ≡ fmap functorM (eta monadM) x
25 fmap-headDeltaM-with-deltaM-eta {l} {A} {O} {M} {fm} {mm} x = refl
26 fmap-headDeltaM-with-deltaM-eta {l} {A} {S n} {M} {fm} {mm} x = refl
27
28
29 fmap-tailDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
30 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM}
31 (d : DeltaM M {functorM} {monadM} A (S n)) ->
32 deltaM-fmap ((tailDeltaM {n = n} {monadM = monadM} ) ∙ deltaM-eta) d ≡ deltaM-fmap (deltaM-eta) d
33 fmap-tailDeltaM-with-deltaM-eta {n = O} d = refl
34 fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl
35
36
37 -- main proofs
38
39 deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat}
40 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM}
41 (f : A -> B) -> (x : A) ->
42 ((deltaM-eta {l} {B} {n} {M} {functorM} {monadM} )∙ f) x ≡ deltaM-fmap f (deltaM-eta x)
43 deltaM-eta-is-nt {l} {A} {B} {O} {M} {fm} {mm} f x = begin
44 deltaM-eta {n = O} (f x) ≡⟨ refl ⟩
45 deltaM (mono (eta mm (f x))) ≡⟨ cong (\de -> deltaM (mono de)) (eta-is-nt mm f x) ⟩
46 deltaM (mono (fmap fm f (eta mm x))) ≡⟨ refl ⟩
47 deltaM-fmap f (deltaM-eta {n = O} x) ∎
48 deltaM-eta-is-nt {l} {A} {B} {S n} {M} {fm} {mm} f x = begin
49 deltaM-eta {n = S n} (f x) ≡⟨ refl ⟩
50 deltaM (delta-eta {n = S n} (eta mm (f x))) ≡⟨ refl ⟩
51 deltaM (delta (eta mm (f x)) (delta-eta (eta mm (f x))))
52 ≡⟨ cong (\de -> deltaM (delta de (delta-eta de))) (eta-is-nt mm f x) ⟩
53 deltaM (delta (fmap fm f (eta mm x)) (delta-eta (fmap fm f (eta mm x))))
54 ≡⟨ cong (\de -> deltaM (delta (fmap fm f (eta mm x)) de)) (eta-is-nt delta-is-monad (fmap fm f) (eta mm x)) ⟩
55 deltaM (delta (fmap fm f (eta mm x)) (delta-fmap (fmap fm f) (delta-eta (eta mm x))))
56 ≡⟨ refl ⟩
57 deltaM-fmap f (deltaM-eta {n = S n} x)
58 ∎
20 59
21 postulate deltaM-right-unity-law : {l : Level} {A : Set l} 60 postulate deltaM-right-unity-law : {l : Level} {A : Set l}
22 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} {n : Nat} 61 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} {n : Nat}
23 (d : DeltaM M {functorM} {monadM} A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d 62 (d : DeltaM M {functorM} {monadM} A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d
24 {- 63 {-
65 deltaM (delta x d) 104 deltaM (delta x d)
66 ∎ 105 ∎
67 -} 106 -}
68 107
69 108
70 fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} 109
71 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} 110
72 (x : M A) -> (fmap functorM ((headDeltaM {l} {A} {n} {M} {functorM} {monadM}) ∙ deltaM-eta) x) ≡ fmap functorM (eta monadM) x 111
73 fmap-headDeltaM-with-deltaM-eta {l} {A} {O} {M} {fm} {mm} x = refl 112 postulate deltaM-left-unity-law : {l : Level} {A : Set l}
74 fmap-headDeltaM-with-deltaM-eta {l} {A} {S n} {M} {fm} {mm} x = refl
75
76 fmap-tailDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
77 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM}
78 (d : DeltaM M {functorM} {monadM} A (S n)) ->
79 deltaM-fmap ((tailDeltaM {n = n} {monadM = monadM} ) ∙ deltaM-eta) d ≡ deltaM-fmap (deltaM-eta) d
80 fmap-tailDeltaM-with-deltaM-eta {n = O} d = refl
81 fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl
82
83
84
85 deltaM-left-unity-law : {l : Level} {A : Set l}
86 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} 113 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM}
87 {n : Nat} 114 {n : Nat}
88 (d : DeltaM M {functorM} {monadM} A (S n)) -> 115 (d : DeltaM M {functorM} {monadM} A (S n)) ->
89 (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d 116 (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d
117 {-
90 deltaM-left-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin 118 deltaM-left-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin
91 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) 119 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x)))
92 ≡⟨ refl ⟩ 120 ≡⟨ refl ⟩
93 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-eta) (mono x))) 121 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-eta) (mono x)))
94 ≡⟨ refl ⟩ 122 ≡⟨ refl ⟩
135 appendDeltaM (deltaM (mono x)) (deltaM d) 163 appendDeltaM (deltaM (mono x)) (deltaM d)
136 ≡⟨ refl ⟩ 164 ≡⟨ refl ⟩
137 deltaM (delta x d) 165 deltaM (delta x d)
138 ∎ 166 ∎
139 167
168 -}
169
140 170
141 171
142 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} 172 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat}
143 {M : Set l -> Set l} 173 {M : Set l -> Set l}
144 (functorM : Functor M) 174 (functorM : Functor M)
150 return = deltaM-eta; 180 return = deltaM-eta;
151 bind = deltaM-bind; 181 bind = deltaM-bind;
152 association-law = {!!}; 182 association-law = {!!};
153 left-unity-law = deltaM-left-unity-law; 183 left-unity-law = deltaM-left-unity-law;
154 right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ; 184 right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ;
155 eta-is-nt = {!!} 185 eta-is-nt = deltaM-eta-is-nt
156 } 186 }
157 187
158 188
159 189
160 190