{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} 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) →
                    autoParam
                        (∀ {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
                          tensorHom f g = CategoryTheory.CategoryStruct.comp (whiskerRight f X₂) (whiskerLeft Y₁ g))
                        CategoryTheory.MonoidalCategory.tensorHom_def._autoParam →
                      autoParam
                          (∀ (X₁ X₂ : C),
                            tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.CategoryStruct.id X₂) =
                              CategoryTheory.CategoryStruct.id (tensorObj X₁ X₂))
                          CategoryTheory.MonoidalCategory.id_tensorHom_id._autoParam →
                        autoParam
                            (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
                              CategoryTheory.CategoryStruct.comp (tensorHom f₁ f₂) (tensorHom g₁ g₂) =
                                tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁)
                                  (CategoryTheory.CategoryStruct.comp f₂ g₂))
                            CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom._autoParam →
                          autoParam
                              (∀ (X Y : C),
                                whiskerLeft X (CategoryTheory.CategoryStruct.id Y) =
                                  CategoryTheory.CategoryStruct.id (tensorObj X Y))
                              CategoryTheory.MonoidalCategory.whiskerLeft_id._autoParam →
                            autoParam
                                (∀ (X Y : C),
                                  whiskerRight (CategoryTheory.CategoryStruct.id X) Y =
                                    CategoryTheory.CategoryStruct.id (tensorObj X Y))
                                CategoryTheory.MonoidalCategory.id_whiskerRight._autoParam →
                              autoParam
                                  (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
                                    CategoryTheory.CategoryStruct.comp (tensorHom (tensorHom f₁ f₂) f₃)
                                        (associator Y₁ Y₂ Y₃).hom =
                                      CategoryTheory.CategoryStruct.comp (associator X₁ X₂ X₃).hom
                                        (tensorHom f₁ (tensorHom f₂ f₃)))
                                  CategoryTheory.MonoidalCategory.associator_naturality._autoParam →
                                autoParam
                                    (∀ {X Y : C} (f : X ⟶ Y),
                                      CategoryTheory.CategoryStruct.comp (whiskerLeft tensorUnit f) (leftUnitor Y).hom =
                                        CategoryTheory.CategoryStruct.comp (leftUnitor X).hom f)
                                    CategoryTheory.MonoidalCategory.leftUnitor_naturality._autoParam →
                                  autoParam
                                      (∀ {X Y : C} (f : X ⟶ Y),
                                        CategoryTheory.CategoryStruct.comp (whiskerRight f tensorUnit)
                                            (rightUnitor Y).hom =
                                          CategoryTheory.CategoryStruct.comp (rightUnitor X).hom f)
                                      CategoryTheory.MonoidalCategory.rightUnitor_naturality._autoParam →
                                    autoParam
                                        (∀ (W X Y Z : C),
                                          CategoryTheory.CategoryStruct.comp (whiskerRight (associator W X Y).hom Z)
                                              (CategoryTheory.CategoryStruct.comp (associator W (tensorObj X Y) Z).hom
                                                (whiskerLeft W (associator X Y Z).hom)) =
                                            CategoryTheory.CategoryStruct.comp (associator (tensorObj W X) Y Z).hom
                                              (associator W X (tensorObj Y Z)).hom)
                                        CategoryTheory.MonoidalCategory.pentagon._autoParam →
                                      autoParam
                                          (∀ (X Y : C),
                                            CategoryTheory.CategoryStruct.comp (associator X tensorUnit Y).hom
                                                (whiskerLeft X (leftUnitor Y).hom) =
                                              whiskerRight (rightUnitor X).hom Y)
                                          CategoryTheory.MonoidalCategory.triangle._autoParam →
                                        (isTerminalTensorUnit : CategoryTheory.Limits.IsTerminal tensorUnit) →
                                          (fst : (X Y : C) → tensorObj X Y ⟶ X) →
                                            (snd : (X Y : C) → tensorObj X Y ⟶ Y) →
                                              autoParam
                                                  (∀ (X Y : C),
                                                    fst X Y =
                                                      CategoryTheory.CategoryStruct.comp
                                                        (whiskerLeft X (isTerminalTensorUnit.from Y))
                                                        (rightUnitor X).hom)
                                                  CategoryTheory.SemiCartesianMonoidalCategory.fst_def._autoParam →
                                                autoParam
                                                    (∀ (X Y : C),
                                                      snd X Y =
                                                        CategoryTheory.CategoryStruct.comp
                                                          (whiskerRight (isTerminalTensorUnit.from X) Y)
                                                          (leftUnitor Y).hom)
                                                    CategoryTheory.SemiCartesianMonoidalCategory.snd_def._autoParam →
                                                  CategoryTheory.SemiCartesianMonoidalCategory C