{V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        (Hom : C → C → V) →
          (id : (X : C) → CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ Hom X X) →
            (comp : (X Y Z : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj (Hom X Y) (Hom Y Z) ⟶ Hom X Z) →
              autoParam
                  (∀ (X Y : C),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Hom X Y)).inv
                        (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (id X) (Hom X Y)) (comp X X Y)) =
                      CategoryTheory.CategoryStruct.id (Hom X Y))
                  CategoryTheory.EnrichedCategory.id_comp._autoParam →
                autoParam
                    (∀ (X Y : C),
                      CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Hom X Y)).inv
                          (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Hom X Y) (id Y)) (comp X Y Y)) =
                        CategoryTheory.CategoryStruct.id (Hom X Y))
                    CategoryTheory.EnrichedCategory.comp_id._autoParam →
                  autoParam
                      (∀ (W X Y Z : C),
                        CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.associator (Hom W X) (Hom X Y) (Hom Y Z)).inv
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.whiskerRight (comp W X Y) (Hom Y Z))
                              (comp W Y Z)) =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Hom W X) (comp X Y Z)) (comp W X Z))
                      CategoryTheory.EnrichedCategory.assoc._autoParam →
                    CategoryTheory.EnrichedCategory V C