Commit 2024-08-14 09:17 a7e0ad18

feat(CategoryTheory/Monoidal): Hopf monoids (#13317) Defines Hopf monoids in a braided category. Proves two facts (antipode is an antihomomorphism, morphisms intertwine antipode) that are not yet proved for unbundled Hopf algebras. Once we prove Hopf_ (ModuleCat R) is equivalent to HopfAlgebraCat (having defined that!), we will get those two facts for free. We should also check later that Hopf_ C in a cartesian monoidal category is equivalent GroupObject_ C (being defined independently elsewhere).

• depends on: #13313
• depends on: #13312 (probably doesn't actually depend, but I don't want to sort out the git history now)
• depends on: #13315