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

@[implicit_reducible]

instance CategoryTheory.instLaxMonoidalObjOppositeFunctorTypeCoyonedaOpTensorUnit (C : Type u) [Category.{v, u} C] [MonoidalCategory C] : (coyoneda.obj (Opposite.op (MonoidalCategoryStruct.tensorUnit C))).LaxMonoidal

Equations

• One or more equations did not get rendered due to their size.