{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X : C} →
        {motive : CategoryTheory.MonObj X → Sort u} →
          (t : CategoryTheory.MonObj X) →
            ((one : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) →
                (mul : CategoryTheory.MonoidalCategoryStruct.tensorObj X X ⟶ X) →
                  (one_mul :
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight one X)
                          mul =
                        (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom) →
                    (mul_one :
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X one)
                            mul =
                          (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom) →
                      (mul_assoc :
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight mul X)
                              mul =
                            CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X mul) mul)) →
                        motive
                          { one := one, mul := mul, one_mul := one_mul, mul_one := mul_one, mul_assoc := mul_assoc }) →
              motive t