Yoneda embedding of CommMon C #
theorem
CategoryTheory.IsCommMonObj.ofRepresentableBy
{C : Type u}
[Category.{v, u} C]
[CartesianMonoidalCategory C]
[BraidedCategory C]
(X : C)
(F : Functor Cᵒᵖ CommMonCat)
(α : (F.comp (forget CommMonCat)).RepresentableBy X)
:
If X represents a presheaf of commutative monoids, then X is a commutative monoid object.