∀ (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]
  [hasDayConvolution :
    ∀ (F G : CategoryTheory.Functor C V),
      (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F G)]
  [hasDayConvolutionUnit :
    (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
      (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))]
  [inst_4 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  ⦃X Y : CategoryTheory.Discrete PUnit.{1}⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).map f)
      (CategoryTheory.MonoidalCategory.DayFunctor.ν C V) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayFunctor.ν C V)
      (((CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).comp
            (CategoryTheory.MonoidalCategoryStruct.tensorUnit
                (CategoryTheory.MonoidalCategory.DayFunctor C V)).functor).map
        f)