{C : Type u_1} →
  (motive : (x x_1 : CategoryTheory.FreeMonoidalCategory C) → x.Hom x_1 → Sort u_2) →
    (x x_1 : CategoryTheory.FreeMonoidalCategory C) →
      (x_2 : x.Hom x_1) →
        ((X : CategoryTheory.FreeMonoidalCategory C) → motive X X (CategoryTheory.FreeMonoidalCategory.Hom.id X)) →
          ((X Y Z : CategoryTheory.FreeMonoidalCategory C) →
              motive ((X.tensor Y).tensor Z) (X.tensor (Y.tensor Z))
                (CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z)) →
            ((X Y Z : CategoryTheory.FreeMonoidalCategory C) →
                motive (X.tensor (Y.tensor Z)) ((X.tensor Y).tensor Z)
                  (CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z)) →
              ((a : CategoryTheory.FreeMonoidalCategory C) →
                  motive (a.tensor CategoryTheory.FreeMonoidalCategory.unit) a
                    (CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom a)) →
                ((a : CategoryTheory.FreeMonoidalCategory C) →
                    motive a (a.tensor CategoryTheory.FreeMonoidalCategory.unit)
                      (CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv a)) →
                  ((a : CategoryTheory.FreeMonoidalCategory C) →
                      motive (CategoryTheory.FreeMonoidalCategory.unit.tensor a) a
                        (CategoryTheory.FreeMonoidalCategory.Hom.l_hom a)) →
                    ((a : CategoryTheory.FreeMonoidalCategory C) →
                        motive a (CategoryTheory.FreeMonoidalCategory.unit.tensor a)
                          (CategoryTheory.FreeMonoidalCategory.Hom.l_inv a)) →
                      ((x x_3 Y : CategoryTheory.FreeMonoidalCategory C) →
                          (f : x.Hom Y) → (g : Y.Hom x_3) → motive x x_3 (f.comp g)) →
                        ((X Y₁ Y₂ : CategoryTheory.FreeMonoidalCategory C) →
                            (f : Y₁.Hom Y₂) →
                              motive (X.tensor Y₁) (X.tensor Y₂)
                                (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X f)) →
                          ((X₁ X₂ : CategoryTheory.FreeMonoidalCategory C) →
                              (f : X₁.Hom X₂) →
                                (X : CategoryTheory.FreeMonoidalCategory C) →
                                  motive (X₁.tensor X) (X₂.tensor X) (f.whiskerRight X)) →
                            ((W X Y Z : CategoryTheory.FreeMonoidalCategory C) →
                                (f : W.Hom Y) → (g : X.Hom Z) → motive (W.tensor X) (Y.tensor Z) (f.tensor g)) →
                              motive x x_1 x_2