Control.Category.Instances.Cokleisli

This module defines a co-Kleisli category construction on an
arbitrary comonad in an arbitrary premonoidal category.

Definitions

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

  The co-Kleisli category of a category `cat` with comonad `w`. This
  forms another category with the same objects. In addition, if
  `cat` is a premonoidal category and `w` has tensorial costrength,
  then this category inherits its premonoidal structure.
  (Note that this is NOT the case for monoidal structure.)

Totality: total
Visibility: public export
Constructor: 

MkCokleisli : cat (w a) b -> Cokleisli cat w a b

Projection: 

.runCokleisli : Cokleisli cat w a b -> cat (w a) b

Hints:

PreBimonoidal cat add mul z i => (StrongComonad cat add w, StrongComonad cat mul w) => PreBimonoidal (Cokleisli cat w) add mul z i

PreBraided cat ten i => StrongComonad cat ten w => PreBraided (Cokleisli cat w) ten i

PreCartesian cat ten i => StrongComonad cat ten w => PreCartesian (Cokleisli cat w) ten i

Category cat => StrongComonad cat ten w => EndoBinoidal cat ten => EndoBinoidal (Cokleisli cat w) ten

Category cat => CatComonad cat w => Category (Cokleisli cat w)

PreCocartesian cat ten i => StrongComonad cat ten w => PreCocartesian (Cokleisli cat w) ten i

PreSymmetric cat ten i => StrongComonad cat ten w => PreSymmetric (Cokleisli cat w) ten i

PreMonoidal cat ten i => StrongComonad cat ten w => PreMonoidal (Cokleisli cat w) ten i

Promonad0 cat => CatComonad cat w => Promonad0 (Cokleisli cat w)

.runCokleisli : Cokleisli cat w a b -> cat (w a) b

Totality: total
Visibility: public export

runCokleisli : Cokleisli cat w a b -> cat (w a) b

Totality: total
Visibility: public export

CokleisliBinoidal : Category cat => StrongComonad cat ten w => EndoBinoidal cat ten => EndoBinoidal (Cokleisli cat w) ten

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

Totality: total
Visibility: public export

CokleisliPreMonoidal : PreMonoidal cat ten i => StrongComonad cat ten w => PreMonoidal (Cokleisli cat w) ten i

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

Totality: total
Visibility: public export

CokleisliPreBraided : PreBraided cat ten i => StrongComonad cat ten w => PreBraided (Cokleisli cat w) ten i

Totality: total
Visibility: public export

CokleisliPreSymmetric : PreSymmetric cat ten i => StrongComonad cat ten w => PreSymmetric (Cokleisli cat w) ten i

Totality: total
Visibility: public export

CokleisliPreCartesian : PreCartesian cat ten i => StrongComonad cat ten w => PreCartesian (Cokleisli cat w) ten i

Totality: total
Visibility: public export

CokleisliPreCocartesian : PreCocartesian cat ten i => StrongComonad cat ten w => PreCocartesian (Cokleisli cat w) ten i

Totality: total
Visibility: public export

CokleisliPreBimonoidal : PreBimonoidal cat add mul z i => (StrongComonad cat add w, StrongComonad cat mul w) => PreBimonoidal (Cokleisli cat w) add mul z i

Totality: total
Visibility: public export

Cokleisli : (cat : CategoryR) -> ComonadR cat -> CategoryR

Totality: total
Visibility: public export

CokleisliInj : FunctorR cat (Cokleisli cat w)

Totality: total
Visibility: public export

Cokleisli : (cat : PreMonoidalR) -> StrongComonadR cat -> PreMonoidalR

Totality: total
Visibility: public export

Cokleisli : (cat : PreBraidedR) -> StrongComonadR (cat .monoidalR) -> PreBraidedR

Totality: total
Visibility: public export

Cokleisli : (cat : PreSymmetricR) -> StrongComonadR (cat .monoidalR) -> PreSymmetricR

Totality: total
Visibility: public export

Cokleisli : (cat : PreCartesianR) -> StrongComonadR (cat .monoidalR) -> PreCartesianR

Totality: total
Visibility: public export

Cokleisli : (cat : PreCocartesianR) -> StrongComonadR (cat .monoidalR) -> PreCocartesianR

Totality: total
Visibility: public export