{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.MonoidalCategoryStruct D] →
            {F : CategoryTheory.Functor D C} →
              {motive : CategoryTheory.Monoidal.InducingFunctorData F → Sort u} →
                ((μIso :
                      (X Y : D) →
                        CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ≅
                          F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) →
                    (whiskerLeft_eq :
                        ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂),
                          F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) =
                            CategoryTheory.CategoryStruct.comp (μIso X Y₁).inv
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (F.map f))
                                (μIso X Y₂).hom)) →
                      (whiskerRight_eq :
                          ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D),
                            F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) =
                              CategoryTheory.CategoryStruct.comp (μIso X₁ Y).inv
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj Y))
                                  (μIso X₂ Y).hom)) →
                        (tensorHom_eq :
                            ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
                              F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) =
                                CategoryTheory.CategoryStruct.comp (μIso X₁ X₂).inv
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (F.map g))
                                    (μIso Y₁ Y₂).hom)) →
                          (εIso :
                              CategoryTheory.MonoidalCategoryStruct.tensorUnit C ≅
                                F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) →
                            (associator_eq :
                                ∀ (X Y Z : D),
                                  F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom =
                                    (((μIso (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).symm ≪≫
                                          CategoryTheory.MonoidalCategory.tensorIso (μIso X Y).symm
                                            (CategoryTheory.Iso.refl (F.obj Z))) ≪≫
                                        CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y)
                                            (F.obj Z) ≪≫
                                          CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.Iso.refl (F.obj X))
                                              (μIso Y Z) ≪≫
                                            μIso X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom) →
                              (leftUnitor_eq :
                                  ∀ (X : D),
                                    F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom =
                                      (((μIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X).symm ≪≫
                                            CategoryTheory.MonoidalCategory.tensorIso εIso.symm
                                              (CategoryTheory.Iso.refl (F.obj X))) ≪≫
                                          CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom) →
                                (rightUnitor_eq :
                                    ∀ (X : D),
                                      F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom =
                                        (((μIso X (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).symm ≪≫
                                              CategoryTheory.MonoidalCategory.tensorIso
                                                (CategoryTheory.Iso.refl (F.obj X)) εIso.symm) ≪≫
                                            CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom) →
                                  motive
                                    { μIso := μIso, whiskerLeft_eq := whiskerLeft_eq,
                                      whiskerRight_eq := whiskerRight_eq, tensorHom_eq := tensorHom_eq, εIso := εIso,
                                      associator_eq := associator_eq, leftUnitor_eq := leftUnitor_eq,
                                      rightUnitor_eq := rightUnitor_eq }) →
                  (t : CategoryTheory.Monoidal.InducingFunctorData F) → motive t