Instance MonoidalFunctorsCompose : MonoidalFunctor m1 m3 (f1 >>>> f2) :=
{ mf_id := id_comp (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1))
Instance MonoidalFunctorsCompose : MonoidalFunctor m1 m3 (f1 >>>> f2) :=
{ mf_id := id_comp (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1))