{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} →
              {P : Sort u} →
                {η :
                    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
                      CategoryTheory.MonoidalCategoryStruct.tensorUnit D} →
                  {δ :
                      (X Y : C) →
                        F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ⟶
                          CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)} →
                    {δ_natural_left :
                        autoParam
                          (∀ {X Y : C} (f : X ⟶ Y) (X' : C),
                            CategoryTheory.CategoryStruct.comp (δ X X')
                                (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) =
                              CategoryTheory.CategoryStruct.comp
                                (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X')) (δ Y X'))
                          CategoryTheory.Functor.OplaxMonoidal.δ_natural_left._autoParam} →
                      {δ_natural_right :
                          autoParam
                            (∀ {X Y : C} (X' : C) (f : X ⟶ Y),
                              CategoryTheory.CategoryStruct.comp (δ X' X)
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) =
                                CategoryTheory.CategoryStruct.comp
                                  (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f)) (δ X' Y))
                            CategoryTheory.Functor.OplaxMonoidal.δ_natural_right._autoParam} →
                        {oplax_associativity :
                            autoParam
                              (∀ (X Y Z : C),
                                CategoryTheory.CategoryStruct.comp
                                    (δ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
                                    (CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ X Y) (F.obj Z))
                                      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y)
                                          (F.obj Z)).hom) =
                                  CategoryTheory.CategoryStruct.comp
                                    (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
                                    (CategoryTheory.CategoryStruct.comp
                                      (δ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
                                      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ Y Z))))
                              CategoryTheory.Functor.OplaxMonoidal.oplax_associativity._autoParam} →
                          {oplax_left_unitality :
                              autoParam
                                (∀ (X : C),
                                  (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv =
                                    CategoryTheory.CategoryStruct.comp
                                      (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv)
                                      (CategoryTheory.CategoryStruct.comp
                                        (δ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
                                        (CategoryTheory.MonoidalCategoryStruct.whiskerRight η (F.obj X))))
                                CategoryTheory.Functor.OplaxMonoidal.oplax_left_unitality._autoParam} →
                            {oplax_right_unitality :
                                autoParam
                                  (∀ (X : C),
                                    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).inv =
                                      CategoryTheory.CategoryStruct.comp
                                        (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv)
                                        (CategoryTheory.CategoryStruct.comp
                                          (δ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) η)))
                                  CategoryTheory.Functor.OplaxMonoidal.oplax_right_unitality._autoParam} →
                              {η' :
                                  F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
                                    CategoryTheory.MonoidalCategoryStruct.tensorUnit D} →
                                {δ' :
                                    (X Y : C) →
                                      F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ⟶
                                        CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)} →
                                  {δ_natural_left' :
                                      autoParam
                                        (∀ {X Y : C} (f : X ⟶ Y) (X' : C),
                                          CategoryTheory.CategoryStruct.comp (δ' X X')
                                              (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f)
                                                (F.obj X')) =
                                            CategoryTheory.CategoryStruct.comp
                                              (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X'))
                                              (δ' Y X'))
                                        CategoryTheory.Functor.OplaxMonoidal.δ_natural_left._autoParam} →
                                    {δ_natural_right' :
                                        autoParam
                                          (∀ {X Y : C} (X' : C) (f : X ⟶ Y),
                                            CategoryTheory.CategoryStruct.comp (δ' X' X)
                                                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X')
                                                  (F.map f)) =
                                              CategoryTheory.CategoryStruct.comp
                                                (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f))
                                                (δ' X' Y))
                                          CategoryTheory.Functor.OplaxMonoidal.δ_natural_right._autoParam} →
                                      {oplax_associativity' :
                                          autoParam
                                            (∀ (X Y Z : C),
                                              CategoryTheory.CategoryStruct.comp
                                                  (δ' (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
                                                  (CategoryTheory.CategoryStruct.comp
                                                    (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ' X Y)
                                                      (F.obj Z))
                                                    (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X)
                                                        (F.obj Y) (F.obj Z)).hom) =
                                                CategoryTheory.CategoryStruct.comp
                                                  (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
                                                  (CategoryTheory.CategoryStruct.comp
                                                    (δ' X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
                                                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X)
                                                      (δ' Y Z))))
                                            CategoryTheory.Functor.OplaxMonoidal.oplax_associativity._autoParam} →
                                        {oplax_left_unitality' :
                                            autoParam
                                              (∀ (X : C),
                                                (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv =
                                                  CategoryTheory.CategoryStruct.comp
                                                    (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv)
                                                    (CategoryTheory.CategoryStruct.comp
                                                      (δ' (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
                                                      (CategoryTheory.MonoidalCategoryStruct.whiskerRight η'
                                                        (F.obj X))))
                                              CategoryTheory.Functor.OplaxMonoidal.oplax_left_unitality._autoParam} →
                                          {oplax_right_unitality' :
                                              autoParam
                                                (∀ (X : C),
                                                  (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).inv =
                                                    CategoryTheory.CategoryStruct.comp
                                                      (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv)
                                                      (CategoryTheory.CategoryStruct.comp
                                                        (δ' X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                                        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X)
                                                          η')))
                                                CategoryTheory.Functor.OplaxMonoidal.oplax_right_unitality._autoParam} →
                                            { η := η, δ := δ, δ_natural_left := δ_natural_left,
                                                  δ_natural_right := δ_natural_right,
                                                  oplax_associativity := oplax_associativity,
                                                  oplax_left_unitality := oplax_left_unitality,
                                                  oplax_right_unitality := oplax_right_unitality } =
                                                { η := η', δ := δ', δ_natural_left := δ_natural_left',
                                                  δ_natural_right := δ_natural_right',
                                                  oplax_associativity := oplax_associativity',
                                                  oplax_left_unitality := oplax_left_unitality',
                                                  oplax_right_unitality := oplax_right_unitality' } →
                                              (η ≍ η' → δ ≍ δ' → P) → P