Mercurial > hg > Papers > 2015 > atton-thesis
diff src/delta_is_functor.agda @ 42:4cc65012412f
Add proofs of functor-laws on delta
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 13 Feb 2015 17:13:23 +0900 |
parents | |
children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/delta_is_functor.agda Fri Feb 13 17:13:23 2015 +0900 @@ -0,0 +1,6 @@ +delta-is-functor : {l : Level} {n : Nat} -> + Functor {l} (\A -> Delta A (S n)) +delta-is-functor = record { fmap = delta-fmap + ; preserve-id = delta-preserve-id + ; covariant = \f g -> delta-covariant g f + ; fmap-equiv = delta-fmap-equiv }