Commit 2020-08-21 02:24 17190352

feat(category_theory/monad/*): Add category of bundled (co)monads; prove equivalence of monads with monoid objects (#3762) This PR constructs bundled monads, and proves the "usual" equivalence between the category of monads and the category of monoid objects in the endomorphism category. It also includes a definition of morphisms of unbundled monads, and proves some necessary small lemmas in the following two files:

1. category_theory.functor_category
2. category_theory.monoidal.internal Given any isomorphism in Cat, we construct a corresponding equivalence of categories in Cat.equiv_of_iso.