Mercurial > hg > Members > atton > delta_monad

diff 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
line wrap: on
line diff
--- a/agda/deltaM.agda	Mon Feb 02 14:09:30 2015 +0900
+++ b/agda/deltaM.agda	Tue Feb 03 11:45:33 2015 +0900
@@ -57,7 +57,7 @@
 deltaM-fmap : {l : Level} {A B : Set l} {n : Nat}
               {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
               (A -> B) -> DeltaM M A (S n) -> DeltaM M B (S n)
-deltaM-fmap {l} {A} {B} {n} {M} {functorM} f (deltaM d) = deltaM (fmap delta-is-functor (fmap functorM f) d)
+deltaM-fmap {l} {A} {B} {n} {M} {functorM} f d = deltaM (fmap delta-is-functor (fmap functorM f) (unDeltaM d))