∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  (CategoryTheory.equivToOverUnit C).functor =
    CategoryTheory.Over.forget (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)