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 D] →
              {F : CategoryTheory.Functor C D} →
                F.OplaxMonoidal →
                  {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 D'] →
                              {F' : CategoryTheory.Functor C' D'} → F'.OplaxMonoidal → Sort u