Mercurial > hg > Members > atton > delta_monad
comparison agda/deltaM/monad.agda @ 125:6dcc68ef8f96
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} |