monoids and comonoids in a monoidal category

[Alizter]

Here is a definition of monoid and comonoid object in a monoidal category.

They live in a new file called Algebra/Categorical/MonoidObject.v. This should be a place for "categorical algebra" that is theory about algebraic objects defined using category theory.

In order to define a comonoid as a monoid in the opposite monoidal category we need to be able to take take the opposite monoidal category. This requires restructuring how we define things in Monoidal.v using natural transformations and equivalences where we can. The work in #1952 helped some properties hold more easily. The result is that the monoidal structure is inherited in the opposite category in a fairly straightforward way, modulo moving some inverted morphisms around.

As an "application" we show that x $-> y is a (commutative) monoid when y is a (commutative) monoid object in a cartesian category. (Equivalently, x can be a comonoid). This greatly simplifies the analogous proof in #1929 leaving us only to show that objects of additive categories are comonoids or monoids (whichever turns out to be eaiser).

I've taken the time to also simplify a few proofs in Products.v where new lemmas I've introduced can break up the work.

[jdchristensen]

So far I just looked at the WildCat part. I read the new file when I have more time.

[jdchristensen]

Nice!