Timeline for Cat as a bicategory of monads over another category
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 7, 2023 at 16:30 | comment | added | Ilk | @fosco do do you mean 2-cells as in 2-cells, turning 1-category of monads on C into a 2 category? or 2-cells in the bicategory of monads in Cat sense? | |
| Jan 6, 2023 at 16:57 | comment | added | fosco | I wrote the code. It indeed refers to the notion of monad map that allows for 2-cells, as in Street "formal theory". | |
| Jan 5, 2023 at 15:24 | comment | added | Simon Henry | A monad morphism for two monads on a fixed category $C$ is already a natural transformation, so there no natural transformation between morphisms. I don't fully understand the Agda code you sent me, but it seems to refers to the notion of morphism between a monad on $C$ and a monad on another category $D$. In this case there is indeed a notion of 2-cell, but then you are not talking about the category of monads on $C$, you are talking about the bicategory of monads in the bicategory $Cat$ of categories. | |
| Jan 5, 2023 at 15:17 | comment | added | Ilk | Taking 2-cells as natural transformations between underlying morphisms of monad morphisms, that satisfy; commutativity of a diagram as defined here github.com/agda/agda-categories/blob/master/src/Categories/…, I think this should be the construction in ncatlab.org/nlab/show/monad#the_bicategory_of_monads, I am trying to arrange it into bicategory in agda right now, to check that my understanding is correct. | |
| Jan 5, 2023 at 2:56 | comment | added | Simon Henry | Wait. How do you get a "bicategory of monads" on a 1-category $C$ ? I now how to get a "bicategory of monads in a bicategory" or a "1-category of monads on a 1-category $C$ " but I don't see what category you are talking about here. | |
| Jan 4, 2023 at 15:22 | history | edited | Ilk | CC BY-SA 4.0 |
edited title
|
| Jan 4, 2023 at 15:13 | history | asked | Ilk | CC BY-SA 4.0 |