Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/monad.agda @ 125:6dcc68ef8f96

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove right-unity-law for DeltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 02 Feb 2015 14:09:30 +0900
parents 48b44bd85056
children 5902b2a24abf
comparison
equal deleted inserted replaced
124:48b44bd85056 125:6dcc68ef8f96
24 (d : DeltaM M A (S n)) -> deltaM (unDeltaM d) ≡ d 24 (d : DeltaM M A (S n)) -> deltaM (unDeltaM d) ≡ d
25 deconstruct-id {n = O} (deltaM x) = refl 25 deconstruct-id {n = O} (deltaM x) = refl
26 deconstruct-id {n = S n} (deltaM x) = refl 26 deconstruct-id {n = S n} (deltaM x) = refl
27 27
28 28
29 headDeltaM-with-appendDeltaM : {l : Level} {A : Set l} {n m : Nat}
30 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
31 (d : DeltaM M A (S n)) -> (ds : DeltaM M A (S m)) ->
32 headDeltaM (appendDeltaM d ds) ≡ headDeltaM d
33 headDeltaM-with-appendDeltaM {l} {A} {O} {O} (deltaM (mono _)) (deltaM _) = refl
34 headDeltaM-with-appendDeltaM {l} {A} {O} {S m} (deltaM (mono _)) (deltaM _) = refl
35 headDeltaM-with-appendDeltaM {l} {A} {S n} {O} (deltaM (delta _ _)) (deltaM _) = refl
36 headDeltaM-with-appendDeltaM {l} {A} {S n} {S m} (deltaM (delta _ _)) (deltaM _) = refl
37
38
39 29
40 fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} 30 fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
41 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> 31 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
42 (x : T A) -> (fmap F ((headDeltaM {n = n} {M = M}) ∙ deltaM-eta) x) ≡ fmap F (eta M) x 32 (x : T A) -> (fmap F ((headDeltaM {n = n} {M = M}) ∙ deltaM-eta) x) ≡ fmap F (eta M) x
43 fmap-headDeltaM-with-deltaM-eta {n = O} x = refl 33 fmap-headDeltaM-with-deltaM-eta {n = O} x = refl
44 fmap-headDeltaM-with-deltaM-eta {n = S n} x = refl 34 fmap-headDeltaM-with-deltaM-eta {n = S n} x = refl
45 35
46 36
47 37
97 ≡⟨ refl ⟩ 87 ≡⟨ refl ⟩
98 deltaM-fmap f (deltaM-eta {n = S n} x) 88 deltaM-fmap f (deltaM-eta {n = S n} x)
99 ∎ 89 ∎
100 90
101 91
102 {- 92
103 93
104 postulate deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} 94 postulate deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat}
105 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} 95 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
106 (f : A -> B) -> 96 (f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) ->
107 (d : DeltaM T {F} {M} (DeltaM T A (S n)) (S n)) ->
108 deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d) 97 deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d)
109
110 postulate deltaM-right-unity-law : {l : Level} {A : Set l}
111 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} {n : Nat}
112 (d : DeltaM M {functorM} {monadM} A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d
113 {- 98 {-
114 deltaM-right-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin 99 deltaM-mu-is-nt {l} {A} {B} {O} {T} {F} {M} f (deltaM (mono x)) = begin
100 deltaM-fmap f (deltaM-mu (deltaM (mono x)))
101 ≡⟨ refl ⟩
102 deltaM-fmap f (deltaM (mono (mu M (fmap F headDeltaM x))))
103 ≡⟨ refl ⟩
104 deltaM (mono (fmap F f (mu M (fmap F headDeltaM x))))
105 ≡⟨ cong (\de -> deltaM (mono de)) (sym (mu-is-nt M f (fmap F headDeltaM x))) ⟩
106 deltaM (mono (mu M (fmap F (fmap F f) (fmap F headDeltaM x))))
107 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F headDeltaM (fmap F f) x)) ⟩
108 deltaM (mono (mu M (fmap F ((fmap F f) ∙ headDeltaM) x)))
109 ≡⟨ {!!} ⟩
110 deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)))
111 ≡⟨ {!!} ⟩
112 deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)))
113 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F (deltaM-fmap f) (headDeltaM) x) ⟩
114 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x))))
115 ≡⟨ refl ⟩
116 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x)))))))
117 ≡⟨ refl ⟩
118 deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x)))
119 ≡⟨ refl ⟩
120 deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (mono x)))
121 ∎
122 deltaM-mu-is-nt {n = S n} f (deltaM (delta x d)) = {!!}
123
124 -}
125
126
127 deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat}
128 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
129 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d
130 deltaM-right-unity-law {l} {A} {O} {M} {fm} {mm} (deltaM (mono x)) = begin
115 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ 131 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
116 deltaM-mu (deltaM (mono (eta mm (deltaM (mono x))))) ≡⟨ refl ⟩ 132 deltaM-mu (deltaM (mono (eta mm (deltaM (mono x))))) ≡⟨ refl ⟩
117 deltaM (mono (mu mm (fmap fm (headDeltaM {M = M})(eta mm (deltaM (mono x)))))) 133 deltaM (mono (mu mm (fmap fm (headDeltaM {M = mm})(eta mm (deltaM (mono x))))))
118 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (eta-is-nt mm headDeltaM (deltaM (mono x)) )) ⟩ 134 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (eta-is-nt mm headDeltaM (deltaM (mono x)) )) ⟩
119 deltaM (mono (mu mm (eta mm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) (deltaM (mono x)))))) ≡⟨ refl ⟩ 135 deltaM (mono (mu mm (eta mm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) (deltaM (mono x)))))) ≡⟨ refl ⟩
120 deltaM (mono (mu mm (eta mm x))) ≡⟨ cong (\de -> deltaM (mono de)) (sym (right-unity-law mm x)) ⟩ 136 deltaM (mono (mu mm (eta mm x))) ≡⟨ cong (\de -> deltaM (mono de)) (sym (right-unity-law mm x)) ⟩
121 deltaM (mono x) 137 deltaM (mono x)
122 ∎ 138 ∎
123 deltaM-right-unity-law {l} {A} {M} {fm} {mm} {S n} (deltaM (delta x d)) = begin 139 deltaM-right-unity-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
124 deltaM-mu (deltaM-eta (deltaM (delta x d))) 140 deltaM-mu (deltaM-eta (deltaM (delta x d)))
125 ≡⟨ refl ⟩ 141 ≡⟨ refl ⟩
126 deltaM-mu (deltaM (delta (eta mm (deltaM (delta x d))) (delta-eta (eta mm (deltaM (delta x d)))))) 142 deltaM-mu (deltaM (delta (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d))))))
127 ≡⟨ refl ⟩ 143 ≡⟨ refl ⟩
128 appendDeltaM (deltaM (mono (mu mm (fmap fm (headDeltaM {monadM = mm}) (eta mm (deltaM (delta x d))))))) 144 deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta {l} {T (DeltaM M A (S (S n)))} {n} (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d)))))))))
129 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) 145 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d)))))))))))
130 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de))) 146 ≡⟨ refl ⟩
131 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))) 147 deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (eta M (deltaM (delta x d)))))
132 (sym (eta-is-nt mm headDeltaM (deltaM (delta x d)))) ⟩ 148 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
133 appendDeltaM (deltaM (mono (mu mm (eta mm ((headDeltaM {monadM = mm}) (deltaM (delta x d))))))) 149 ≡⟨ cong (\de -> deltaM (delta (mu M de)
134 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) 150 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))))
135 ≡⟨ refl ⟩ 151 (sym (eta-is-nt M headDeltaM (deltaM (delta x d)))) ⟩
136 appendDeltaM (deltaM (mono (mu mm (eta mm x)))) 152 deltaM (delta (mu M (eta M (headDeltaM {M = M} (deltaM (delta x d)))))
137 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) 153 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
138 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))) 154 ≡⟨ refl ⟩
139 (sym (right-unity-law mm x)) ⟩ 155 deltaM (delta (mu M (eta M x))
140 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) 156 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
141 ≡⟨ refl ⟩ 157 ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))))
142 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-eta (eta mm (deltaM (delta x d))))))) 158 (sym (right-unity-law M x)) ⟩
143 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM de))) (sym (eta-is-nt delta-is-monad (fmap fm tailDeltaM) (eta mm (deltaM (delta x d))))) ⟩ 159 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
144 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta (fmap fm tailDeltaM (eta mm (deltaM (delta x d))))))) 160 ≡⟨ refl ⟩
145 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta de)))) (sym (eta-is-nt mm tailDeltaM (deltaM (delta x d)))) ⟩ 161 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-fmap (fmap F tailDeltaM) (delta-eta (eta M (deltaM (delta x d)))))))))
146 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta (eta mm (tailDeltaM (deltaM (delta x d))))))) 162 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM de)))))
147 ≡⟨ refl ⟩ 163 (sym (delta-eta-is-nt (fmap F tailDeltaM) (eta M (deltaM (delta x d))))) ⟩
148 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta (eta mm (deltaM d))))) 164 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (fmap F tailDeltaM (eta M (deltaM (delta x d)))))))))
149 ≡⟨ refl ⟩ 165 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta de))))))
150 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-eta (deltaM d))) 166 (sym (eta-is-nt M tailDeltaM (deltaM (delta x d)))) ⟩
151 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) de) (deltaM-right-unity-law (deltaM d)) ⟩ 167 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (eta M (tailDeltaM (deltaM (delta x d)))))))))
152 appendDeltaM (deltaM (mono x)) (deltaM d) 168 ≡⟨ refl ⟩
169 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (eta M (deltaM d)))))))
170 ≡⟨ refl ⟩
171 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-eta (deltaM d)))))
172 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-right-unity-law (deltaM d)) ⟩
173 deltaM (delta x (unDeltaM {M = M} (deltaM d)))
153 ≡⟨ refl ⟩ 174 ≡⟨ refl ⟩
154 deltaM (delta x d) 175 deltaM (delta x d)
155 ∎ 176 ∎
156 -} 177
157 178
158 179
159 180 {-
160 181
161 182
162 postulate deltaM-left-unity-law : {l : Level} {A : Set l} 183 postulate deltaM-left-unity-law : {l : Level} {A : Set l}
163 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} 184 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM}
164 {n : Nat} 185 {n : Nat}