Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM.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 5bd5f4a7ce8d
children 0a3b6cb91a05
comparison
equal deleted inserted replaced
110:cd058dd89864 111:9fe3d0bd1149
69 {functorM : {l' : Level} -> Functor {l'} M} 69 {functorM : {l' : Level} -> Functor {l'} M}
70 {monadM : {l' : Level} -> Monad {l'} M functorM} -> 70 {monadM : {l' : Level} -> Monad {l'} M functorM} ->
71 A -> (DeltaM M {functorM} {monadM} A (S n)) 71 A -> (DeltaM M {functorM} {monadM} A (S n))
72 deltaM-eta {n = n} {monadM = mm} x = deltaM (delta-eta {n = n} (eta mm x)) 72 deltaM-eta {n = n} {monadM = mm} x = deltaM (delta-eta {n = n} (eta mm x))
73 73
74 deltaM-mu : {l : Level} {A : Set l} {n : Nat}
75 {M : {l' : Level} -> Set l' -> Set l'}
76 {functorM : {l' : Level} -> Functor {l'} M}
77 {monadM : {l' : Level} -> Monad {l'} M functorM} ->
78 DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A (S n)) (S n) ->
79 DeltaM M {functorM} {monadM} A (S n)
80 deltaM-mu {n = O} {functorM = fm} {monadM = mm} (deltaM (mono x)) = deltaM (mono (mu mm (fmap fm headDeltaM x)))
81 deltaM-mu {n = S n} {functorM = fm} {monadM = mm} (deltaM (delta x d)) = appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x))))
82 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))
83
74 84
75 deltaM-bind : {l : Level} {A B : Set l} 85 deltaM-bind : {l : Level} {A B : Set l}
76 {n : Nat} 86 {n : Nat}
77 {M : {l' : Level} -> Set l' -> Set l'} 87 {M : {l' : Level} -> Set l' -> Set l'}
78 {functorM : {l' : Level} -> Functor {l'} M} 88 {functorM : {l' : Level} -> Functor {l'} M}
83 deltaM-bind {n = O} {monadM = mm} (deltaM (mono x)) f = deltaM (mono (bind mm x (headDeltaM ∙ f))) 93 deltaM-bind {n = O} {monadM = mm} (deltaM (mono x)) f = deltaM (mono (bind mm x (headDeltaM ∙ f)))
84 deltaM-bind {n = S n} {monadM = mm} (deltaM (delta x d)) f = appendDeltaM (deltaM (mono (bind mm x (headDeltaM ∙ f)))) 94 deltaM-bind {n = S n} {monadM = mm} (deltaM (delta x d)) f = appendDeltaM (deltaM (mono (bind mm x (headDeltaM ∙ f))))
85 (deltaM-bind (deltaM d) (tailDeltaM ∙ f)) 95 (deltaM-bind (deltaM d) (tailDeltaM ∙ f))
86 96
87 97
88 deltaM-mu : {l : Level} {A : Set l} {n : Nat}
89 {M : {l' : Level} -> Set l' -> Set l'}
90 {functorM : {l' : Level} -> Functor {l'} M}
91 {monadM : {l' : Level} -> Monad {l'} M functorM}
92 -> (DeltaM M (DeltaM M {functorM} {monadM} A (S n)) (S n)) -> DeltaM M {functorM} {monadM} A (S n)
93 deltaM-mu d = deltaM-bind d id