Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/monad.agda @ 111:9fe3d0bd1149

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove right-unity-law on DeltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 29 Jan 2015 11:42:22 +0900
parents ebd0d6e2772c
children 0a3b6cb91a05
comparison
equal deleted inserted replaced
110:cd058dd89864 111:9fe3d0bd1149
3 open ≡-Reasoning 3 open ≡-Reasoning
4 4
5 open import basic 5 open import basic
6 open import delta 6 open import delta
7 open import delta.functor 7 open import delta.functor
8 open import delta.monad
8 open import deltaM 9 open import deltaM
9 open import deltaM.functor 10 open import deltaM.functor
10 open import nat 11 open import nat
11 open import laws 12 open import laws
12 13
14 open Functor 15 open Functor
15 open NaturalTransformation 16 open NaturalTransformation
16 open Monad 17 open Monad
17 18
18 19
19 headDeltaM-commute : {l : Level} {A B : Set l} {n : Nat}
20 {M : {l' : Level} -> Set l' -> Set l'} ->
21 {functorM : {l' : Level} -> Functor {l'} M} ->
22 {monadM : {l' : Level} -> Monad {l'} M (functorM ) } ->
23 (f : A -> B) -> (x : DeltaM M {functorM} {monadM} A n) ->
24 headDeltaM (deltaM-fmap f x) ≡ fmap functorM f (headDeltaM x)
25 headDeltaM-commute f (deltaM (mono x)) = refl
26 headDeltaM-commute f (deltaM (delta x d)) = refl
27
28
29 {-
30 headDeltaM-is-natural-transformation : {l : Level} {A : Set l} {n : Nat}
31 {M : {l' : Level} -> Set l' -> Set l'} ->
32 {functorM : {l' : Level} -> Functor {l'} M}
33 {monadM : {l' : Level} -> Monad {l'} M functorM } ->
34 NaturalTransformation {l} (\A -> DeltaM M {functorM} {monadM} A n) M
35 {\f d → deltaM (mono (headDeltaM (deltaM-fmap f d)))}
36 {fmap functorM} headDeltaM
37
38 headDeltaM-is-natural-transformation = record { commute = headDeltaM-commute }
39 -}
40
41 20
42 deltaM-right-unity-law : {l : Level} {A : Set l} 21 deltaM-right-unity-law : {l : Level} {A : Set l}
43 {M : {l' : Level} -> Set l' -> Set l'} 22 {M : {l' : Level} -> Set l' -> Set l'}
44 (functorM : {l' : Level} -> Functor {l'} M) 23 {functorM : {l' : Level} -> Functor {l'} M}
45 (monadM : {l' : Level} -> Monad {l'} M functorM) 24 {monadM : {l' : Level} -> Monad {l'} M functorM}
46 (d : DeltaM M {functorM} {monadM} A (S O)) -> 25 {n : Nat}
26 (d : DeltaM M {functorM} {monadM} A (S n)) ->
47 (deltaM-mu ∙ deltaM-eta) d ≡ id d 27 (deltaM-mu ∙ deltaM-eta) d ≡ id d
48 deltaM-right-unity-law {l} {A} {M} functorM monadM (deltaM (mono x)) = begin 28 deltaM-right-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin
49 (deltaM-mu ∙ deltaM-eta) (deltaM (mono x)) ≡⟨ refl ⟩ 29 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
50 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ 30 deltaM-mu (deltaM (mono (eta mm (deltaM (mono x))))) ≡⟨ refl ⟩
51 deltaM-mu (deltaM (mono (eta monadM (deltaM (mono x))))) ≡⟨ refl ⟩ 31 deltaM (mono (mu mm (fmap fm (headDeltaM {M = M})(eta mm (deltaM (mono x))))))
52 deltaM (mono (mu monadM (fmap functorM (headDeltaM {l} {A} {S O} {M}) (eta monadM (deltaM (mono x)))))) 32 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (eta-is-nt mm headDeltaM (deltaM (mono x)) )) ⟩
53 ≡⟨ cong (\de -> deltaM (mono (mu monadM (de)))) (sym (eta-is-nt monadM headDeltaM (deltaM (mono x)))) ⟩ 33 deltaM (mono (mu mm (eta mm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) (deltaM (mono x)))))) ≡⟨ refl ⟩
54 deltaM (mono (mu monadM (eta monadM (headDeltaM {l} {A} {S O} {M} {functorM} {monadM} (deltaM (mono x)))))) 34 deltaM (mono (mu mm (eta mm x))) ≡⟨ cong (\de -> deltaM (mono de)) (sym (right-unity-law mm x)) ⟩
35 deltaM (mono x)
36 ∎
37 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)))
55 ≡⟨ refl ⟩ 39 ≡⟨ refl ⟩
56 deltaM (mono (mu monadM (eta monadM x))) 40 deltaM-mu (deltaM (delta (eta mm (deltaM (delta x d))) (delta-eta (eta mm (deltaM (delta x d))))))
57 ≡⟨ cong (\de -> deltaM (mono de)) (sym (right-unity-law monadM x ) )⟩
58 deltaM (mono x)
59 ≡⟨ refl ⟩ 41 ≡⟨ refl ⟩
60 id (deltaM (mono x)) 42 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)))))))
44 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de)))
45 (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)))) ⟩
47 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)))))))
49 ≡⟨ refl ⟩
50 appendDeltaM (deltaM (mono (mu mm (eta mm x))))
51 (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))))))))
53 (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)))))))
55 ≡⟨ refl ⟩
56 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))))) ⟩
58 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta (fmap fm tailDeltaM (eta mm (deltaM (delta x d)))))))
59 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta de)))) (sym (eta-is-nt mm tailDeltaM (deltaM (delta x d)))) ⟩
60 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta (eta mm (tailDeltaM (deltaM (delta x d)))))))
61 ≡⟨ refl ⟩
62 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta (eta mm (deltaM d)))))
63 ≡⟨ refl ⟩
64 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-eta (deltaM d)))
65 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) de) (deltaM-right-unity-law (deltaM d)) ⟩
66 appendDeltaM (deltaM (mono x)) (deltaM d)
67 ≡⟨ refl ⟩
68 deltaM (delta x d)
61 ∎ 69 ∎
62 deltaM-right-unity-law functorM monadM (deltaM (delta x ()))
63 -- cannot apply (mu ∙ eta) for over 2 version delta.
64 70
65 71
66 {- 72 {-
67 deltaM-left-unity-law : {l : Level} {A : Set l} 73 deltaM-left-unity-law : {l : Level} {A : Set l}
68 {M : {l' : Level} -> Set l' -> Set l'} 74 {M : {l' : Level} -> Set l' -> Set l'}
84 90
85 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} 91 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat}
86 {M : {l' : Level} -> Set l' -> Set l'} 92 {M : {l' : Level} -> Set l' -> Set l'}
87 (functorM : {l' : Level} -> Functor {l'} M) 93 (functorM : {l' : Level} -> Functor {l'} M)
88 (monadM : {l' : Level}-> Monad {l'} M functorM) -> 94 (monadM : {l' : Level}-> Monad {l'} M functorM) ->
89 Monad {l} (\A -> DeltaM M {functorM} {monadM} A n) deltaM-is-functor 95 Monad {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) deltaM-is-functor
90 deltaM-is-monad functorM monadM = record 96 deltaM-is-monad functorM monadM = record
91 { mu = deltaM-mu; 97 { mu = deltaM-mu;
92 eta = deltaM-eta; 98 eta = deltaM-eta;
93 return = {!!}; 99 return = deltaM-eta;
94 bind = {!!}; 100 bind = deltaM-bind;
95 association-law = {!!}; 101 association-law = {!!};
96 left-unity-law = {!!}; 102 left-unity-law = {!!};
97 right-unity-law = {!!}; 103 right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ;
98 eta-is-nt = {!!} 104 eta-is-nt = {!!}
99 } 105 }
100 106
101 107
102 108
103 109
104 110