agda
Pseudomonads and their Kleisli bicategories
Hello there. I'm not sure if I'm looking in the right places, but it seems like the library doesn't have a notion of a pseudomonad (a monad on a bicategory, as opposed to the monad in a bicategory that lives in src/Categories/Bicategory/Monad.agda). Is that correct? If so, would it be useful to add that (and perhaps the notion of the Kleisli bicategory that can be derived from any such pseudomonad)?
If you mean in the sense of weak 2-monad, then yes, that would be useful. I specify weak because we've found that strictness of various kinds seems to not work so well in this setting.
@JacquesCarette Ah yes, a "weak 2-monad" is what I meant indeed. Somewhat confusingly, the relevant equipment includes pseudonatural (and not lax natural) transformations...