(𝟙_ C ⟶ -) is a lax monoidal functor to Type

noncomputable def CategoryTheory.coyonedaTensorUnit (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.LaxMonoidalFunctor C (Type v)

(𝟙_ C ⟶ -) is a lax monoidal functor to Type.