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