∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {V : Type u_2}
  [inst_1 : CategoryTheory.Category.{u_1, u_2} V] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory V] {F : CategoryTheory.MonoidalCategory.DayFunctor C V}
  (φ :
    CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶
      F.functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
  ⦃X Y : CategoryTheory.Discrete PUnit.{1}⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).map f) φ =
    CategoryTheory.CategoryStruct.comp φ
      (((CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).comp F.functor).map f)