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 - `fromFunc` is functorial (see `CatFunctor`), meaning:
  * `fromFunc id = id`
  * `fromFunc f . fromFunc g = fromFunc (f . g)`

Parameters: cat
Constraints: Category cat
Methods:

fromFunc : (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)

fromFunc : 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.
  
  See `Promonad` for required laws.

Parameters: cat
Constraints: Category cat
Methods:

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

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

fromFuncW : 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