Mercurial > hg > Members > atton > delta_monad

diff agda/delta/functor.agda @ 97:f26a954cd068

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update Natural Transformation definitions
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 20 Jan 2015 16:27:55 +0900
parents 8d92ed54a94f
children ebd0d6e2772c
line wrap: on
line diff
--- a/agda/delta/functor.agda	Tue Jan 20 16:25:53 2015 +0900
+++ b/agda/delta/functor.agda	Tue Jan 20 16:27:55 2015 +0900
@@ -22,7 +22,7 @@
 functor-law-2 f g (mono x)    = refl
 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d)
 
-delta-is-functor : {l : Level} -> Functor (Delta {l})
+delta-is-functor : {l : Level} -> Functor {l} Delta 
 delta-is-functor = record {  fmap = delta-fmap ;
                              preserve-id = functor-law-1;
                              covariant  = \f g -> functor-law-2 g f}