{V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        {motive : CategoryTheory.EnrichedCategory V C → Sort 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) →
                  (id_comp :
                      ∀ (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)) →
                    (comp_id :
                        ∀ (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)) →
                      (assoc :
                          ∀ (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)) →
                        motive
                          { Hom := Hom, id := id, comp := comp, id_comp := id_comp, comp_id := comp_id,
                            assoc := assoc }) →
            (t : CategoryTheory.EnrichedCategory V C) → motive t