Mercurial > hg > Members > atton > delta_monad
comparison agda/deltaM/monad.agda @ 112:0a3b6cb91a05
Prove left-unity-law for DeltaM
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 30 Jan 2015 21:57:31 +0900 |
parents | 9fe3d0bd1149 |
children | 08403eb8db8b |
comparison
equal
deleted
inserted
replaced
111:9fe3d0bd1149 | 112:0a3b6cb91a05 |
---|---|
16 open NaturalTransformation | 16 open NaturalTransformation |
17 open Monad | 17 open Monad |
18 | 18 |
19 | 19 |
20 | 20 |
21 deltaM-right-unity-law : {l : Level} {A : Set l} | 21 postulate deltaM-right-unity-law : {l : Level} {A : Set l} |
22 {M : {l' : Level} -> Set l' -> Set l'} | 22 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} {n : Nat} |
23 {functorM : {l' : Level} -> Functor {l'} M} | 23 (d : DeltaM M {functorM} {monadM} A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d |
24 {monadM : {l' : Level} -> Monad {l'} M functorM} | 24 {- |
25 {n : Nat} | |
26 (d : DeltaM M {functorM} {monadM} A (S n)) -> | |
27 (deltaM-mu ∙ deltaM-eta) d ≡ id d | |
28 deltaM-right-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin | 25 deltaM-right-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin |
29 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ | 26 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ |
30 deltaM-mu (deltaM (mono (eta mm (deltaM (mono x))))) ≡⟨ refl ⟩ | 27 deltaM-mu (deltaM (mono (eta mm (deltaM (mono x))))) ≡⟨ refl ⟩ |
31 deltaM (mono (mu mm (fmap fm (headDeltaM {M = M})(eta mm (deltaM (mono x)))))) | 28 deltaM (mono (mu mm (fmap fm (headDeltaM {M = M})(eta mm (deltaM (mono x)))))) |
32 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (eta-is-nt mm headDeltaM (deltaM (mono x)) )) ⟩ | 29 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (eta-is-nt mm headDeltaM (deltaM (mono x)) )) ⟩ |
37 deltaM-right-unity-law {l} {A} {M} {fm} {mm} {S n} (deltaM (delta x d)) = begin | 34 deltaM-right-unity-law {l} {A} {M} {fm} {mm} {S n} (deltaM (delta x d)) = begin |
38 deltaM-mu (deltaM-eta (deltaM (delta x d))) | 35 deltaM-mu (deltaM-eta (deltaM (delta x d))) |
39 ≡⟨ refl ⟩ | 36 ≡⟨ refl ⟩ |
40 deltaM-mu (deltaM (delta (eta mm (deltaM (delta x d))) (delta-eta (eta mm (deltaM (delta x d)))))) | 37 deltaM-mu (deltaM (delta (eta mm (deltaM (delta x d))) (delta-eta (eta mm (deltaM (delta x d)))))) |
41 ≡⟨ refl ⟩ | 38 ≡⟨ refl ⟩ |
42 appendDeltaM (deltaM (mono (mu mm (fmap fm (headDeltaM {monadM = mm}) (eta mm (deltaM (delta x d))))))) | 39 appendDeltaM (deltaM (mono (mu mm (fmap fm (headDeltaM {monadM = mm}) (eta mm (deltaM (delta x d))))))) |
43 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) | 40 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) |
44 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de))) | 41 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de))) |
45 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))) | 42 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))) |
46 (sym (eta-is-nt mm headDeltaM (deltaM (delta x d)))) ⟩ | 43 (sym (eta-is-nt mm headDeltaM (deltaM (delta x d)))) ⟩ |
47 appendDeltaM (deltaM (mono (mu mm (eta mm ((headDeltaM {monadM = mm}) (deltaM (delta x d))))))) | 44 appendDeltaM (deltaM (mono (mu mm (eta mm ((headDeltaM {monadM = mm}) (deltaM (delta x d))))))) |
48 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) | 45 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) |
49 ≡⟨ refl ⟩ | 46 ≡⟨ refl ⟩ |
50 appendDeltaM (deltaM (mono (mu mm (eta mm x)))) | 47 appendDeltaM (deltaM (mono (mu mm (eta mm x)))) |
51 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) | 48 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) |
52 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))) | 49 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))) |
53 (sym (right-unity-law mm x)) ⟩ | 50 (sym (right-unity-law mm x)) ⟩ |
54 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) | 51 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) |
55 ≡⟨ refl ⟩ | 52 ≡⟨ refl ⟩ |
56 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-eta (eta mm (deltaM (delta x d))))))) | 53 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-eta (eta mm (deltaM (delta x d))))))) |
57 ≡⟨ 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))))) ⟩ | 54 ≡⟨ 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))))) ⟩ |
65 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) de) (deltaM-right-unity-law (deltaM d)) ⟩ | 62 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) de) (deltaM-right-unity-law (deltaM d)) ⟩ |
66 appendDeltaM (deltaM (mono x)) (deltaM d) | 63 appendDeltaM (deltaM (mono x)) (deltaM d) |
67 ≡⟨ refl ⟩ | 64 ≡⟨ refl ⟩ |
68 deltaM (delta x d) | 65 deltaM (delta x d) |
69 ∎ | 66 ∎ |
70 | 67 -} |
71 | 68 |
72 {- | 69 |
73 deltaM-left-unity-law : {l : Level} {A : Set l} | 70 fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} |
74 {M : {l' : Level} -> Set l' -> Set l'} | 71 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} |
75 (functorM : {l' : Level} -> Functor {l'} M) | 72 (x : M A) -> (fmap functorM ((headDeltaM {l} {A} {n} {M} {functorM} {monadM}) ∙ deltaM-eta) x) ≡ fmap functorM (eta monadM) x |
76 (monadM : {l' : Level} -> Monad {l'} M functorM) | 73 fmap-headDeltaM-with-deltaM-eta {l} {A} {O} {M} {fm} {mm} x = refl |
77 (d : DeltaM M {functorM} {monadM} A (S O)) -> | 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} | |
87 {n : Nat} | |
88 (d : DeltaM M {functorM} {monadM} A (S n)) -> | |
78 (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d | 89 (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d |
79 deltaM-left-unity-law functorM monadM (deltaM (mono x)) = begin | 90 deltaM-left-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin |
80 (deltaM-mu ∙ deltaM-fmap deltaM-eta) (deltaM (mono x)) ≡⟨ refl ⟩ | 91 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) |
81 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ | 92 ≡⟨ refl ⟩ |
82 deltaM-mu (deltaM (mono (fmap functorM deltaM-eta x))) ≡⟨ refl ⟩ | 93 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-eta) (mono x))) |
83 deltaM (mono (mu monadM (fmap functorM headDeltaM (fmap functorM deltaM-eta x)))) ≡⟨ {!!} ⟩ | 94 ≡⟨ refl ⟩ |
84 deltaM (mono (mu monadM (fmap functorM headDeltaM (fmap functorM deltaM-eta x)))) ≡⟨ {!!} ⟩ | 95 deltaM-mu (deltaM (mono (fmap fm deltaM-eta x))) |
85 | 96 ≡⟨ refl ⟩ |
86 id (deltaM (mono x)) | 97 deltaM (mono (mu mm (fmap fm (headDeltaM {l} {A} {O} {M}) (fmap fm deltaM-eta x)))) |
87 ∎ | 98 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (covariant fm deltaM-eta headDeltaM x)) ⟩ |
88 deltaM-left-unity-law functorM monadM (deltaM (delta x ())) | 99 deltaM (mono (mu mm (fmap fm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) ∙ deltaM-eta) x))) |
89 -} | 100 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (fmap-headDeltaM-with-deltaM-eta {l} {A} {O} {M} {fm} {mm} x) ⟩ |
101 deltaM (mono (mu mm (fmap fm (eta mm) x))) | |
102 ≡⟨ cong (\de -> deltaM (mono de)) (left-unity-law mm x) ⟩ | |
103 deltaM (mono x) | |
104 ∎ | |
105 deltaM-left-unity-law {l} {A} {M} {fm} {mm} {S n} (deltaM (delta x d)) = begin | |
106 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (delta x d))) | |
107 ≡⟨ refl ⟩ | |
108 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-eta) (delta x d))) | |
109 ≡⟨ refl ⟩ | |
110 deltaM-mu (deltaM (delta (fmap fm deltaM-eta x) (delta-fmap (fmap fm deltaM-eta) d))) | |
111 ≡⟨ refl ⟩ | |
112 appendDeltaM (deltaM (mono (mu mm (fmap fm (headDeltaM {l} {A} {S n} {M} {fm} {mm}) (fmap fm deltaM-eta x))))) | |
113 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))) | |
114 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de))) | |
115 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d))))) | |
116 (sym (covariant fm deltaM-eta headDeltaM x)) ⟩ | |
117 appendDeltaM (deltaM (mono (mu mm (fmap fm ((headDeltaM {l} {A} {S n} {M} {fm} {mm}) ∙ deltaM-eta) x)))) | |
118 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))) | |
119 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de))) | |
120 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d))))) | |
121 (fmap-headDeltaM-with-deltaM-eta {l} {A} {S n} {M} {fm} {mm} x) ⟩ | |
122 appendDeltaM (deltaM (mono (mu mm (fmap fm (eta mm) x)))) | |
123 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))) | |
124 | |
125 ≡⟨ cong (\de -> (appendDeltaM (deltaM (mono de)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))))) | |
126 (left-unity-law mm x) ⟩ | |
127 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))) | |
128 ≡⟨ refl ⟩ | |
129 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap (tailDeltaM {n = n})(deltaM-fmap deltaM-eta (deltaM d)))) | |
130 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu de)) (sym (covariant deltaM-is-functor deltaM-eta tailDeltaM (deltaM d))) ⟩ | |
131 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap ((tailDeltaM {n = n}) ∙ deltaM-eta) (deltaM d))) | |
132 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu de)) (fmap-tailDeltaM-with-deltaM-eta (deltaM d)) ⟩ | |
133 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap deltaM-eta (deltaM d))) | |
134 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) de) (deltaM-left-unity-law (deltaM d)) ⟩ | |
135 appendDeltaM (deltaM (mono x)) (deltaM d) | |
136 ≡⟨ refl ⟩ | |
137 deltaM (delta x d) | |
138 ∎ | |
139 | |
140 | |
90 | 141 |
91 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} | 142 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} |
92 {M : {l' : Level} -> Set l' -> Set l'} | 143 {M : Set l -> Set l} |
93 (functorM : {l' : Level} -> Functor {l'} M) | 144 (functorM : Functor M) |
94 (monadM : {l' : Level}-> Monad {l'} M functorM) -> | 145 (monadM : Monad M functorM) -> |
95 Monad {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) deltaM-is-functor | 146 Monad {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) (deltaM-is-functor {l} {n}) |
96 deltaM-is-monad functorM monadM = record | 147 deltaM-is-monad functorM monadM = record |
97 { mu = deltaM-mu; | 148 { mu = deltaM-mu; |
98 eta = deltaM-eta; | 149 eta = deltaM-eta; |
99 return = deltaM-eta; | 150 return = deltaM-eta; |
100 bind = deltaM-bind; | 151 bind = deltaM-bind; |
101 association-law = {!!}; | 152 association-law = {!!}; |
102 left-unity-law = {!!}; | 153 left-unity-law = deltaM-left-unity-law; |
103 right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ; | 154 right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ; |
104 eta-is-nt = {!!} | 155 eta-is-nt = {!!} |
105 } | 156 } |
106 | 157 |
107 | 158 |
108 | 159 |
109 | 160 |