Control.Category.Records.Monad

Definitions

record MonadR : CategoryR -> Type

  A *monad* `m` is a monoid object in the category of endofunctors
  in `cat`, where the tensor product is given by composition.
  
  See `CatMonad` for required laws.

Totality: total
Visibility: public export
Constructor: 

MkMonadR : (fun : (cat .obj -> cat .obj)) -> CatMonad (cat .hom) fun => MonadR cat

Projections:

.fun : MonadR cat -> cat .obj -> cat .obj

.functorR : MonadR cat -> EndofunctorR cat

  Convert this into a `FunctorR`.

.impl : ({rec:0} : MonadR cat) -> CatMonad (cat .hom) ({rec:0} .fun)

.join : (rec : MonadR cat) -> cat .hom (rec .fun (rec .fun a)) (rec .fun a)

  The join transformation of the monad.

.map : (rec : MonadR cat) -> cat .hom a b -> cat .hom (rec .fun a) (rec .fun b)

  Apply the monad to a morphism in `cat`.

.monadR : MonadR cat -> MonadR cat

  Convert this into a `MonadR`.

.unit : (rec : MonadR cat) -> cat .hom a (rec .fun a)

  The unit transformation of the monad.

.fun : MonadR cat -> cat .obj -> cat .obj

Totality: total
Visibility: public export

.impl : ({rec:0} : MonadR cat) -> CatMonad (cat .hom) ({rec:0} .fun)

Totality: total
Visibility: public export

.functorR : MonadR cat -> EndofunctorR cat

  Convert this into a `FunctorR`.

Totality: total
Visibility: public export

.map : (rec : MonadR cat) -> cat .hom a b -> cat .hom (rec .fun a) (rec .fun b)

  Apply the monad to a morphism in `cat`.

Totality: total
Visibility: public export

.monadR : MonadR cat -> MonadR cat

  Convert this into a `MonadR`.

Totality: total
Visibility: public export

.join : (rec : MonadR cat) -> cat .hom (rec .fun (rec .fun a)) (rec .fun a)

  The join transformation of the monad.

Totality: total
Visibility: public export

.unit : (rec : MonadR cat) -> cat .hom a (rec .fun a)

  The unit transformation of the monad.

Totality: total
Visibility: public export

record StrongFunctorR : MonoidalR -> Type

  An endofunctor has *tensorial strength* if it is compatible with a
  monoidal category's tensor product.
  
  See `StrongFunctor` for required laws.

Totality: total
Visibility: public export
Constructor: 

MkStrongFunctorR : (fun : (cat .obj -> cat .obj)) -> StrongFunctor (cat .hom) (cat .tensor) fun => StrongFunctorR cat

Projections:

.fun : StrongFunctorR cat -> cat .obj -> cat .obj

.functorR : StrongFunctorR cat -> EndofunctorR (cat .categoryR)

  Convert this into a `FunctorR`.

.impl : ({rec:0} : StrongFunctorR cat) -> StrongFunctor (cat .hom) (cat .tensor) ({rec:0} .fun)

.map : (rec : StrongFunctorR cat) -> cat .hom a b -> cat .hom (rec .fun a) (rec .fun b)

  Apply the functor to a morphism in `cat`.

.strongl : (rec : StrongFunctorR cat) -> cat .hom (cat .tensor a (rec .fun b)) (rec .fun (cat .tensor a b))

  The left tensor strength.

.strongr : (rec : StrongFunctorR cat) -> cat .hom (cat .tensor (rec .fun a) b) (rec .fun (cat .tensor a b))

  The right tensor strength.

.fun : StrongFunctorR cat -> cat .obj -> cat .obj

Totality: total
Visibility: public export

.impl : ({rec:0} : StrongFunctorR cat) -> StrongFunctor (cat .hom) (cat .tensor) ({rec:0} .fun)

Totality: total
Visibility: public export

.functorR : StrongFunctorR cat -> EndofunctorR (cat .categoryR)

  Convert this into a `FunctorR`.

Totality: total
Visibility: public export

.map : (rec : StrongFunctorR cat) -> cat .hom a b -> cat .hom (rec .fun a) (rec .fun b)

  Apply the functor to a morphism in `cat`.

Totality: total
Visibility: public export

.strongl : (rec : StrongFunctorR cat) -> cat .hom (cat .tensor a (rec .fun b)) (rec .fun (cat .tensor a b))

  The left tensor strength.

Totality: total
Visibility: public export

.strongr : (rec : StrongFunctorR cat) -> cat .hom (cat .tensor (rec .fun a) b) (rec .fun (cat .tensor a b))

  The right tensor strength.

Totality: total
Visibility: public export

record StrongMonadR : MonoidalR -> Type

  A strong monad is a monad that is also a strong functor.
  
  See `StrongMonad` for required laws.

Totality: total
Visibility: public export
Constructor: 

MkStrongMonadR : (fun : (cat .obj -> cat .obj)) -> StrongMonad (cat .hom) (cat .tensor) fun => StrongMonadR cat

Projections:

.fun : StrongMonadR cat -> cat .obj -> cat .obj

.functorR : StrongMonadR cat -> EndofunctorR (cat .categoryR)

  Convert this into a `FunctorR`.

.impl : ({rec:0} : StrongMonadR cat) -> StrongMonad (cat .hom) (cat .tensor) ({rec:0} .fun)

.join : (rec : StrongMonadR cat) -> cat .hom (rec .fun (rec .fun a)) (rec .fun a)

  The join transformation of the monad.

.map : (rec : StrongMonadR cat) -> cat .hom a b -> cat .hom (rec .fun a) (rec .fun b)

  Apply the monad to a morphism in `cat`.

.monadR : StrongMonadR cat -> MonadR (cat .categoryR)

  Convert this into a `MonadR`.

.strongFunctorR : StrongMonadR cat -> StrongFunctorR cat

  Convert this into a `StrongFunctorR`.

.strongMonadR : StrongMonadR cat -> StrongMonadR cat

  Convert this into a `StrongMonadR`.

.strongl : (rec : StrongMonadR cat) -> cat .hom (cat .tensor a (rec .fun b)) (rec .fun (cat .tensor a b))

  The left tensor strength.

.strongr : (rec : StrongMonadR cat) -> cat .hom (cat .tensor (rec .fun a) b) (rec .fun (cat .tensor a b))

  The right tensor strength.

.unit : (rec : StrongMonadR cat) -> cat .hom a (rec .fun a)

  The unit transformation of the monad.

.fun : StrongMonadR cat -> cat .obj -> cat .obj

Totality: total
Visibility: public export

.impl : ({rec:0} : StrongMonadR cat) -> StrongMonad (cat .hom) (cat .tensor) ({rec:0} .fun)

Totality: total
Visibility: public export

.functorR : StrongMonadR cat -> EndofunctorR (cat .categoryR)

  Convert this into a `FunctorR`.

Totality: total
Visibility: public export

.map : (rec : StrongMonadR cat) -> cat .hom a b -> cat .hom (rec .fun a) (rec .fun b)

  Apply the monad to a morphism in `cat`.

Totality: total
Visibility: public export

.monadR : StrongMonadR cat -> MonadR (cat .categoryR)

  Convert this into a `MonadR`.

Totality: total
Visibility: public export

.join : (rec : StrongMonadR cat) -> cat .hom (rec .fun (rec .fun a)) (rec .fun a)

  The join transformation of the monad.

Totality: total
Visibility: public export

.unit : (rec : StrongMonadR cat) -> cat .hom a (rec .fun a)

  The unit transformation of the monad.

Totality: total
Visibility: public export

.strongFunctorR : StrongMonadR cat -> StrongFunctorR cat

  Convert this into a `StrongFunctorR`.

Totality: total
Visibility: public export

.strongl : (rec : StrongMonadR cat) -> cat .hom (cat .tensor a (rec .fun b)) (rec .fun (cat .tensor a b))

  The left tensor strength.

Totality: total
Visibility: public export

.strongr : (rec : StrongMonadR cat) -> cat .hom (cat .tensor (rec .fun a) b) (rec .fun (cat .tensor a b))

  The right tensor strength.

Totality: total
Visibility: public export

.strongMonadR : StrongMonadR cat -> StrongMonadR cat

  Convert this into a `StrongMonadR`.

Totality: total
Visibility: public export