doc(CategoryTheory): a doc-string fix (leanprover-community#33457)

Author: sinhp

Mathlib/CategoryTheory/Monad/Products.lean

@@ -13,7 +13,7 @@ public import Mathlib.CategoryTheory.Monad.Algebra
 # Algebras for the coproduct monad
 
 The functor `Y ↦ X ⨿ Y` forms a monad, whose category of monads is equivalent to the under category
-of `X`. Similarly, `Y ↦ X ⨯ Y` forms a comonad, whose category of comonads is equivalent to the
+of `X`. Similarly, `Y ↦ X ⨯ Y` forms a comonad, whose category of coalgebras is equivalent to the
 over category of `X`.
 
 ## TODO