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 }