∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {V : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} V] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory V] {X Y : CategoryTheory.MonoidalCategory.DayFunctor C V} (f : X.Hom Y),
  {
      natTrans :=
        CategoryTheory.CategoryStruct.comp { natTrans := CategoryTheory.CategoryStruct.id X.functor }.natTrans
          f.natTrans } =
    f