{C : Type u} →
  [𝒞 : CategoryTheory.Category.{v, u} C] →
    {motive : CategoryTheory.MonoidalCategoryStruct C → Sort u_1} →
      (t : CategoryTheory.MonoidalCategoryStruct C) →
        ((tensorObj : C → C → C) →
            (whiskerLeft : (X : C) → {Y₁ Y₂ : C} → (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂)) →
              (whiskerRight : {X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → tensorObj X₁ Y ⟶ tensorObj X₂ Y) →
                (tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂)) →
                  (tensorUnit : C) →
                    (associator : (X Y Z : C) → tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)) →
                      (leftUnitor : (X : C) → tensorObj tensorUnit X ≅ X) →
                        (rightUnitor : (X : C) → tensorObj X tensorUnit ≅ X) →
                          motive
                            { tensorObj := tensorObj, whiskerLeft := whiskerLeft, whiskerRight := whiskerRight,
                              tensorHom := tensorHom, tensorUnit := tensorUnit, associator := associator,
                              leftUnitor := leftUnitor, rightUnitor := rightUnitor }) →
          motive t