Sort u →
  {C : Type u₁} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        {D : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
              {A : C} →
                [inst_4 : CategoryTheory.MonObj A] →
                  {M N : CategoryTheory.Mod_ D A} →
                    M.Hom N →
                      {C' : Type u₁} →
                        [inst' : CategoryTheory.Category.{v₁, u₁} C'] →
                          [inst'_1 : CategoryTheory.MonoidalCategory C'] →
                            {D' : Type u₂} →
                              [inst'_2 : CategoryTheory.Category.{v₂, u₂} D'] →
                                [inst'_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C' D'] →
                                  {A' : C'} →
                                    [inst'_4 : CategoryTheory.MonObj A'] →
                                      {M' N' : CategoryTheory.Mod_ D' A'} → M'.Hom N' → Sort u