Mercurial > hg > Members > atton > delta_monad
diff agda/deltaM.agda @ 118:53cb21845dea
Prove association-law for DeltaM
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 02 Feb 2015 11:54:23 +0900 |
| parents | f02c5ad4a327 |
| children | 0f9ecd118a03 |
line wrap: on
line diff
--- a/agda/deltaM.agda Mon Feb 02 09:57:37 2015 +0900 +++ b/agda/deltaM.agda Mon Feb 02 11:54:23 2015 +0900 @@ -21,6 +21,11 @@ -- DeltaM utils +unDeltaM : {l : Level} {A : Set l} {n : Nat} + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} -> + (DeltaM M {functorM} {monadM} A (S n)) -> Delta (M A) (S n) +unDeltaM (deltaM d) = d + headDeltaM : {l : Level} {A : Set l} {n : Nat} {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} -> DeltaM M {functorM} {monadM} A (S n) -> M A @@ -69,9 +74,9 @@ {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad 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} d = deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d)))) -deltaM-mu {n = S n} {functorM = fm} {monadM = mm} d = appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d))))) - (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM d))) +deltaM-mu {n = O} {functorM = fm} {monadM = mm} d = deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d)))) +deltaM-mu {n = S n} {functorM = fm} {monadM = mm} d = deltaM (delta (mu mm (fmap fm headDeltaM (headDeltaM d))) + (unDeltaM (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM d))))) deltaM-bind : {l : Level} {A B : Set l}