{C : Type u} →
  [𝒞 : CategoryTheory.Category.{v, u} C] →
    (tensorObj : C → C → C) →
      ((X : C) → {Y₁ Y₂ : C} → (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂)) →
        ({X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → tensorObj X₁ Y ⟶ tensorObj X₂ Y) →
          ({X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂)) →
            (tensorUnit : C) →
              ((X Y Z : C) → tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)) →
                ((X : C) → tensorObj tensorUnit X ≅ X) →
                  ((X : C) → tensorObj X tensorUnit ≅ X) → CategoryTheory.MonoidalCategoryStruct C