Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM.agda @ 118:53cb21845dea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
117:6f86b55bf8b4 118:53cb21845dea
18 : (Nat -> Set l) where 18 : (Nat -> Set l) where
19 deltaM : {n : Nat} -> Delta (M A) (S n) -> DeltaM M {functorM} {monadM} A (S n) 19 deltaM : {n : Nat} -> Delta (M A) (S n) -> DeltaM M {functorM} {monadM} A (S n)
20 20
21 21
22 -- DeltaM utils 22 -- DeltaM utils
23
24 unDeltaM : {l : Level} {A : Set l} {n : Nat}
25 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} ->
26 (DeltaM M {functorM} {monadM} A (S n)) -> Delta (M A) (S n)
27 unDeltaM (deltaM d) = d
23 28
24 headDeltaM : {l : Level} {A : Set l} {n : Nat} 29 headDeltaM : {l : Level} {A : Set l} {n : Nat}
25 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} 30 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM}
26 -> DeltaM M {functorM} {monadM} A (S n) -> M A 31 -> DeltaM M {functorM} {monadM} A (S n) -> M A
27 headDeltaM (deltaM d) = headDelta d 32 headDeltaM (deltaM d) = headDelta d
67 72
68 deltaM-mu : {l : Level} {A : Set l} {n : Nat} 73 deltaM-mu : {l : Level} {A : Set l} {n : Nat}
69 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} -> 74 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} ->
70 DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A (S n)) (S n) -> 75 DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A (S n)) (S n) ->
71 DeltaM M {functorM} {monadM} A (S n) 76 DeltaM M {functorM} {monadM} A (S n)
72 deltaM-mu {n = O} {functorM = fm} {monadM = mm} d = deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d)))) 77 deltaM-mu {n = O} {functorM = fm} {monadM = mm} d = deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d))))
73 deltaM-mu {n = S n} {functorM = fm} {monadM = mm} d = appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d))))) 78 deltaM-mu {n = S n} {functorM = fm} {monadM = mm} d = deltaM (delta (mu mm (fmap fm headDeltaM (headDeltaM d)))
74 (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM d))) 79 (unDeltaM (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM d)))))
75 80
76 81
77 deltaM-bind : {l : Level} {A B : Set l} 82 deltaM-bind : {l : Level} {A B : Set l}
78 {n : Nat} 83 {n : Nat}
79 {M : Set l -> Set l} 84 {M : Set l -> Set l}