delta-is-monad : {l : Level} {n : Nat} ->
        Monad {l} (\A -> Delta A (S n))  delta-is-functor
delta-is-monad = record
              { eta             = delta-eta;
                mu              = delta-mu;
                eta-is-nt       = delta-eta-is-nt;
                mu-is-nt        = delta-mu-is-nt;
                association-law = delta-association-law;
                left-unity-law  = delta-left-unity-law ;
                right-unity-law = \x -> (sym (delta-right-unity-law x)) }