Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/monad.agda @ 112:0a3b6cb91a05

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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