Pseudomonads and their Kleisli bicategories

[masaeedu]

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)?

[JacquesCarette]

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.

[masaeedu]

@JacquesCarette Ah yes, a "weak 2-monad" is what I meant indeed. Somewhat confusingly, the relevant equipment includes pseudonatural (and not lax natural) transformations...