New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(category_theory/monad/*): Add category of bundled (co)monads; prove equivalence of monads with monoid objects #3762
Conversation
1. Add hcomp_id_app / id_hcomp_app 2. Add Monad.hext 3. Add Mon_.hext 4. Add file equiv_mon.lean
1. Clean up proof of hcomp_id_app 2. Add has_coe_to_sort instance for Cat 3. Add note about bundled (co)monad category
(By the way, since this was still labelled as |
Sorry about this. I'll make sure to replace |
Other than the two new comments above, LGTM. bors d+ |
✌️ adamtopaz can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
bors r+ |
…ove 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`. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
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:
category_theory.functor_category
category_theory.monoidal.internal
Given any isomorphism in
Cat
, we construct a corresponding equivalence of categories inCat.equiv_of_iso
.