Mercurial > hg > Papers > 2015 > atton-thesis

view paper/src/delta_is_functor.agda @ 78:6f699b37dc55

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add original number count
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 18 Feb 2015 12:26:17 +0900
parents 1181b4facaf9
children
line wrap: on
line source

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 }