Mercurial > hg > Members > atton > delta_monad
diff agda/deltaM.agda @ 111:9fe3d0bd1149
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 |
line wrap: on
line diff
--- a/agda/deltaM.agda Wed Jan 28 22:36:34 2015 +0900 +++ b/agda/deltaM.agda Thu Jan 29 11:42:22 2015 +0900 @@ -71,6 +71,16 @@ A -> (DeltaM M {functorM} {monadM} A (S n)) deltaM-eta {n = n} {monadM = mm} x = deltaM (delta-eta {n = n} (eta mm x)) +deltaM-mu : {l : Level} {A : Set l} {n : Nat} + {M : {l' : Level} -> Set l' -> Set l'} + {functorM : {l' : Level} -> Functor {l'} M} + {monadM : {l' : Level} -> Monad {l'} M functorM} -> + DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A (S n)) (S n) -> + DeltaM M {functorM} {monadM} A (S n) +deltaM-mu {n = O} {functorM = fm} {monadM = mm} (deltaM (mono x)) = deltaM (mono (mu mm (fmap fm headDeltaM x))) +deltaM-mu {n = S n} {functorM = fm} {monadM = mm} (deltaM (delta x d)) = appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x)))) + (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))) + deltaM-bind : {l : Level} {A B : Set l} {n : Nat} @@ -85,9 +95,3 @@ (deltaM-bind (deltaM d) (tailDeltaM ∙ f)) -deltaM-mu : {l : Level} {A : Set l} {n : Nat} - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM} - -> (DeltaM M (DeltaM M {functorM} {monadM} A (S n)) (S n)) -> DeltaM M {functorM} {monadM} A (S n) -deltaM-mu d = deltaM-bind d id