fact: Definition dorp1 := forall (A B : UU0) (f : A -> B), dorp \o [the functor of M \o N] # (M # f) = [the functor of M \o N] # f \o dorp.
imports: mathcomp(all_ssreflect) HB(structures) monae_lib hierarchy monad_lib