∀ {C : Type u} {motive : {X Y : CategoryTheory.FreeMonoidalCategory C} → (X ⟶ Y) → Prop}
  {X Y : CategoryTheory.FreeMonoidalCategory C} (t : X ⟶ Y),
  (∀ (X : CategoryTheory.FreeMonoidalCategory C), motive (CategoryTheory.CategoryStruct.id X)) →
    (∀ (X Y Z : CategoryTheory.FreeMonoidalCategory C),
        motive (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) →
      (∀ (X Y Z : CategoryTheory.FreeMonoidalCategory C),
          motive (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) →
        (∀ (X : CategoryTheory.FreeMonoidalCategory C),
            motive (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom) →
          (∀ (X : CategoryTheory.FreeMonoidalCategory C),
              motive (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv) →
            (∀ (X : CategoryTheory.FreeMonoidalCategory C),
                motive (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom) →
              (∀ (X : CategoryTheory.FreeMonoidalCategory C),
                  motive (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv) →
                (∀ {X Y Z : CategoryTheory.FreeMonoidalCategory C} (f : X ⟶ Y) (g : Y ⟶ Z),
                    motive f → motive g → motive (CategoryTheory.CategoryStruct.comp f g)) →
                  (∀ (X : CategoryTheory.FreeMonoidalCategory C) {Y Z : CategoryTheory.FreeMonoidalCategory C}
                      (f : Y ⟶ Z), motive f → motive (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)) →
                    (∀ {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X ⟶ Y)
                        (Z : CategoryTheory.FreeMonoidalCategory C),
                        motive f → motive (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)) →
                      motive t