Control.Category.Monad

Definitions

interface CatMonad : Hom obj -> (obj -> obj) -> Type

  A *monad* `m` is a monoid object in the category of endofunctors 
  in `cat`, where the tensor product is given by composition.
  Generally, `cat` is a category, though this is not enforced by the
  interface.
  
  This is the interface-style definition of a monad. For the
  record-style definition, see `Control.Category.Records.MonadR`.
  
  Laws (when `cat` is a category):
  * `join . unit = id`
  * `join . map unit = id`
  * `join . join = join . map join`

Parameters: cat, m
Constraints: CatFunctor cat cat m
Constructor: 

MkCatMonad

Methods:

join : cat (m (m a)) (m a)

  The join transformation of the monad.

unit : cat a (m a)

  The unit transformation of the monad.

join : CatMonad cat m => cat (m (m a)) (m a)

  The join transformation of the monad.

Totality: total
Visibility: public export

unit : CatMonad cat m => cat a (m a)

  The unit transformation of the monad.

Totality: total
Visibility: public export

StrongMonad : Hom obj -> (obj -> obj -> obj) -> (obj -> obj) -> Type

  A strong monad is a monad that is also a strong functor, with
  additional compatibility laws.
  
  Laws:
  * `strongl . mapr unit = unit`
  * `strongr . mapl unit = unit`
  * `join . map strongl . strongl = strongl . mapr join`
  * `join . map strongr . strongr = strongr . mapl join`

Totality: total
Visibility: public export

Id : Category cat => StrongMonad cat ten id

Totality: total
Visibility: public export

MorFromMonad : Monad m => Bitraversable ten => StrongMonad Morphism ten m

  Convert a Prelude `Monad` into a strong monad over `Morphism`.

Totality: total
Visibility: public export

FuncFromMonad : Monad m => Bitraversable ten => StrongMonad (~~>) ten m

  Convert a Prelude `Monad` into a strong monad over the function
  category.

Totality: total
Visibility: public export