Idris2Doc : Control.Category.Monad

Control.Category.Monad

(source)
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
interface StrongFunctor : Hom obj -> (obj -> obj -> obj) -> (obj -> obj) -> Type
  An endofunctor has *tensorial strength* if it is compatible with a
  monoidal category's tensor product. Generally, `cat` is a monoidal
  category with `ten` as its tensor produt, though this is not
  enforced by the interface.
  
  Note that while all Prelude functors have strength over `Pair`,
  this does not necessarily hold for other tensor products or in
  other categories.
  
  This is the interface-style definition of a strong functor. For
  the record-style definition, see `Control.Category.Records.StrongFunctorR`.
  
  Laws (when `cat` is a monoidal category):
  * `map unitl . strongl = unitl`
  * `map unitr . strongr = unitr`
  * `map assoc . strongl = strongl . mapr strongl . assoc`
  * `map assoc' . strongr = strongr . mapl strongr . assoc'`
  * `strongr . mapl strongl = strongl . mapr strongr . assoc`

  Parameters: cat, ten, f
Constraints: CatFunctor cat cat f
Constructor: 
MkStrongFunctor

Methods:
  
strongl : cat (ten a (f b)) (f (ten a b))
  The left tensor strength.
  
strongr : cat (ten (f a) b) (f (ten a b))
  The right tensor strength.
strongl : StrongFunctor cat ten f => cat (ten a (f b)) (f (ten a b))
  The left tensor strength.

  Totality: total
  Visibility: public export
strongr : StrongFunctor cat ten f => cat (ten (f a) b) (f (ten a b))
  The right tensor strength.

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