∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X : C} {X_1 Y Z : CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)} (f : X_1 ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.Over.homMk
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp f g).left X) ⋯ =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.left X) ⋯)
      (CategoryTheory.Over.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerRight g.left X) ⋯)