bimonoid objects

Stream: PR reviews

[Kim Morrison]

I have a little stack of PRs leading up to bimonoid objects. The first three are independent.

• #10098 feat: comonoid objects in a braided category form a monoidal category
• #10103 feat: no interesting comonoid objects in cartesian monoidal categories
• #12856 feat: oplax monoidal functors
• #12858 feat: oplax monoidal functors take comonoids to comonoids (depends on #10098 and #12856)
• #12970 feat: definition of bimonoid object in a braided category (depends on #12858)

From here it's a short step to defining Hopf monoids (which in a cartesian monoidal category reduce to group objects).