Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM.agda @ 126:5902b2a24abf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove mu-is-nt for DeltaM with fmap-equiv
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 11:45:33 +0900
parents 0f9ecd118a03
children
comparison
equal deleted inserted replaced
125:6dcc68ef8f96 126:5902b2a24abf
55 -- functor definitions 55 -- functor definitions
56 open Functor 56 open Functor
57 deltaM-fmap : {l : Level} {A B : Set l} {n : Nat} 57 deltaM-fmap : {l : Level} {A B : Set l} {n : Nat}
58 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> 58 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
59 (A -> B) -> DeltaM M A (S n) -> DeltaM M B (S n) 59 (A -> B) -> DeltaM M A (S n) -> DeltaM M B (S n)
60 deltaM-fmap {l} {A} {B} {n} {M} {functorM} f (deltaM d) = deltaM (fmap delta-is-functor (fmap functorM f) d) 60 deltaM-fmap {l} {A} {B} {n} {M} {functorM} f d = deltaM (fmap delta-is-functor (fmap functorM f) (unDeltaM d))
61 61
62 62
63 63
64 64
65 -- monad definitions 65 -- monad definitions