Mercurial > hg > Members > atton > delta_monad
diff agda/deltaM.agda @ 112:0a3b6cb91a05
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 | e6bcc7467335 |
line wrap: on
line diff
--- a/agda/deltaM.agda Thu Jan 29 11:42:22 2015 +0900 +++ b/agda/deltaM.agda Fri Jan 30 21:57:31 2015 +0900 @@ -11,9 +11,9 @@ -- DeltaM definitions data DeltaM {l : Level} - (M : {l' : Level} -> Set l' -> Set l') - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} {A : Set l'} -> Monad {l'} M functorM} + (M : Set l -> Set l) + {functorM : Functor M} + {monadM : Monad M functorM} (A : Set l) : (Nat -> Set l) where deltaM : {n : Nat} -> Delta (M A) (S n) -> DeltaM M {functorM} {monadM} A (S n) @@ -22,28 +22,22 @@ -- DeltaM utils headDeltaM : {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} + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} -> DeltaM M {functorM} {monadM} A (S n) -> M A headDeltaM (deltaM d) = headDelta d tailDeltaM : {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} + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} -> DeltaM {l} M {functorM} {monadM} A (S (S n)) -> DeltaM M {functorM} {monadM} A (S n) tailDeltaM {_} {n} (deltaM d) = deltaM (tailDelta d) appendDeltaM : {l : Level} {A : Set l} {n m : Nat} - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM} -> + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} -> DeltaM M {functorM} {monadM} A (S n) -> DeltaM M {functorM} {monadM} A (S m) -> - DeltaM M {functorM} {monadM} A ((S n) + (S m)) + DeltaM M {functorM} {monadM} A ((S n) + (S m)) appendDeltaM (deltaM d) (deltaM dd) = deltaM (deltaAppend d dd) @@ -52,9 +46,7 @@ -- functor definitions open Functor deltaM-fmap : {l : Level} {A B : Set l} {n : Nat} - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM} + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} -> (A -> B) -> DeltaM M {functorM} {monadM} A (S n) -> DeltaM M {functorM} {monadM} B (S n) deltaM-fmap {l} {A} {B} {n} {M} {functorM} f (deltaM d) = deltaM (fmap delta-is-functor (fmap functorM f) d) @@ -65,16 +57,12 @@ open Monad deltaM-eta : {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} -> + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} -> 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} -> + {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} (deltaM (mono x)) = deltaM (mono (mu mm (fmap fm headDeltaM x))) @@ -84,9 +72,9 @@ deltaM-bind : {l : Level} {A B : Set l} {n : Nat} - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM} -> + {M : Set l -> Set l} + {functorM : Functor M} + {monadM : Monad M functorM} -> (DeltaM M {functorM} {monadM} A (S n)) -> (A -> DeltaM M {functorM} {monadM} B (S n)) -> DeltaM M {functorM} {monadM} B (S n)