∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X : C} (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
  ⦃X_1 Y : CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)⦄ (f_1 : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (({ obj := fun Y => CategoryTheory.Over.mk (CategoryTheory.SemiCartesianMonoidalCategory.snd Y.left X),
                map := fun {Y Z} g =>
                  CategoryTheory.Over.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerRight g.left X) ⋯,
                map_id := ⋯, map_comp := ⋯ }.comp
            (CategoryTheory.Over.map f)).map
        f_1)
      (CategoryTheory.Over.homMk (CategoryTheory.SemiCartesianMonoidalCategory.fst Y.left X) ⋯) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.homMk (CategoryTheory.SemiCartesianMonoidalCategory.fst X_1.left X) ⋯)
      ((CategoryTheory.Functor.id (CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).map f_1)