Control.Category.Instances.Kleisli

This module defines a more general Kleisli category construction
that can be used to derive a premonoidal category structure from
any strong monad on any premonoidal category.

Definitions

record Kleisli : Hom obj -> (obj -> obj) -> obj -> obj -> Type

  The Kleisli category of a category `cat` with monad `m`. This
  forms another category with the same objects. In addition, if
  `cat` is a premonoidal category, then this category inherits its
  premonoidal structure. (Note that this is NOT the case for
  monoidal structure.)

Totality: total
Visibility: public export
Constructor: 

MkKleisli : cat a (m b) -> Kleisli cat m a b

Projection: 

.runKleisli : Kleisli cat m a b -> cat a (m b)

Hints:

PreBimonoidal cat add mul z i => (StrongMonad cat add m, StrongMonad cat mul m) => PreBimonoidal (Kleisli cat m) add mul z i

PreBraided cat ten i => StrongMonad cat ten m => PreBraided (Kleisli cat m) ten i

PreCartesian cat ten i => StrongMonad cat ten m => PreCartesian (Kleisli cat m) ten i

Category cat => StrongMonad cat ten m => EndoBinoidal cat ten => EndoBinoidal (Kleisli cat m) ten

Category cat => CatMonad cat m => Category (Kleisli cat m)

PreCocartesian cat ten i => StrongMonad cat ten m => PreCocartesian (Kleisli cat m) ten i

PreMonoidal cat ten i => StrongMonad cat ten m => PreMonoidal (Kleisli cat m) ten i

Promonad0 cat => CatMonad cat m => Promonad0 (Kleisli cat m)

.runKleisli : Kleisli cat m a b -> cat a (m b)

Totality: total
Visibility: public export

runKleisli : Kleisli cat m a b -> cat a (m b)

Totality: total
Visibility: public export

KleisliBinoidal : Category cat => StrongMonad cat ten m => EndoBinoidal cat ten => EndoBinoidal (Kleisli cat m) ten

  WARNING: This is typically a binoidal functor, not a true bifunctor.
  It is only a bifunctor if the monad `m` is commutative over `ten`.

Totality: total
Visibility: public export

KleisliPreMonoidal : PreMonoidal cat ten i => StrongMonad cat ten m => PreMonoidal (Kleisli cat m) ten i

  WARNING: This is typically a premonoidal category, not truly monoidal.
  It is only monoidal if the monad `m` is commutative over `ten`.

Totality: total
Visibility: public export

KleisliPreBraided : PreBraided cat ten i => StrongMonad cat ten m => PreBraided (Kleisli cat m) ten i

Totality: total
Visibility: public export

KleisliPreCartesian : PreCartesian cat ten i => StrongMonad cat ten m => PreCartesian (Kleisli cat m) ten i

Totality: total
Visibility: public export

KleisliPreCocartesian : PreCocartesian cat ten i => StrongMonad cat ten m => PreCocartesian (Kleisli cat m) ten i

Totality: total
Visibility: public export

KleisliPreBimonoidal : PreBimonoidal cat add mul z i => (StrongMonad cat add m, StrongMonad cat mul m) => PreBimonoidal (Kleisli cat m) add mul z i

Totality: total
Visibility: public export

Kleisli : (cat : CategoryR) -> MonadR cat -> CategoryR

Totality: total
Visibility: public export

KleisliInj : FunctorR cat (Kleisli cat m)

Totality: total
Visibility: public export

Kleisli : (cat : PreMonoidalR) -> StrongMonadR cat -> PreMonoidalR

Totality: total
Visibility: public export

Kleisli : (cat : PreBraidedR) -> StrongMonadR (cat .monoidalR) -> PreBraidedR

Totality: total
Visibility: public export

Kleisli : (cat : PreCartesianR) -> StrongMonadR (cat .monoidalR) -> PreCartesianR

Totality: total
Visibility: public export

Kleisli : (cat : PreCocartesianR) -> StrongMonadR (cat .monoidalR) -> PreCocartesianR

Totality: total
Visibility: public export