Commit 2021-02-10 00:03 7c77279e

feat(category_theory/monad): use bundled monads everywhere (#5889) This PR makes bundled monads the default (adapting definitions by @adamtopaz). The main motivation for this is that the category of algebras for a monad is currently not "hygienic" in that isomorphic monads don't have equivalent Eilenberg-Moore categories, but further that the notion of monad isomorphism is tricky to express, in particular this makes the definition of a monadic functor not preserved by isos either despite not explicitly having monads or algebras in the type. We can now say:

@[simps]
def algebra_equiv_of_iso_monads {T₁ T₂ : monad C} (h : T₁ ≅ T₂) :
  algebra T₁ ≌ algebra T₂ :=

Other than this new data, virtually everything in this PR is just refactoring - in particular there's quite a bit of golfing and generalisation possible, but to keep the diff here minimal I'll do those in later PRs