search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
363 stars 68 forks source link

Pseudomonads and their Kleisli bicategories #310

Open masaeedu opened 2 years ago

masaeedu commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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