Control.Category.Promonad

Definitions

interface Promonad : Hom Type -> Type

  A *promonad* (short for profunctor monad, no relation to regular
  Prelude monads) is a monad in the bicategory of profunctors.
  
  Equivalently, a promonad is a category equipped with an
  identity-on-objects functor from the category `Typ`.
  
  Laws - `funit` is functorial (see `CatFunctor`), meaning:
  * `funit id = id`
  * `funit f . funit g = funit (f . g)`

Parameters: cat
Constraints: Category cat
Methods:

funit : (a -> b) -> cat a b

  The unit transformation of the promonad.
  Equivalently, the action of the unit functor on morphisms.

Implementations:

Promonad Morphism

Monad m => Promonad (Kleislimorphism m)

funit : Promonad cat => (a -> b) -> cat a b

  The unit transformation of the promonad.
  Equivalently, the action of the unit functor on morphisms.

Totality: total
Visibility: public export

interface Promonad0 : Hom Type0 -> Type

  Like `Promonad`, but allows the category's objects to be wrapped
  using `Wrap0`. This is typically the more practical option.

Parameters: cat
Constraints: Category cat
Methods:

funitW : (a -> b) -> cat (W0 a) (W0 b)

  The unit transformation of the promonad.
  Equivalently, the action of the unit functor on morphisms.

funitW : Promonad0 cat => (a -> b) -> cat (W0 a) (W0 b)

  The unit transformation of the promonad.
  Equivalently, the action of the unit functor on morphisms.

Totality: total
Visibility: public export