Control.Category.Records.Comonad

Definitions

record ComonadR : CategoryR -> Type

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

Totality: total
Visibility: public export
Constructor: 

MkComonadR : (fun : (cat .obj -> cat .obj)) -> CatComonad (cat .hom) fun => ComonadR cat

Projections:

.cojoin : (rec : ComonadR cat) -> cat .hom (rec .fun a) (rec .fun (rec .fun a))

  The cojoin transformation of the comonad.

.comonadR : ComonadR cat -> ComonadR cat

  Convert this into a `ComonadR`.

.counit : (rec : ComonadR cat) -> cat .hom (rec .fun a) a

  The counit transformation of the comonad.

.fun : ComonadR cat -> cat .obj -> cat .obj

.functorR : ComonadR cat -> EndofunctorR cat

  Convert this into a `FunctorR`.

.impl : ({rec:0} : ComonadR cat) -> CatComonad (cat .hom) ({rec:0} .fun)

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

  Apply the monad to a morphism in `cat`.

.fun : ComonadR cat -> cat .obj -> cat .obj

Totality: total
Visibility: public export

.impl : ({rec:0} : ComonadR cat) -> CatComonad (cat .hom) ({rec:0} .fun)

Totality: total
Visibility: public export

.functorR : ComonadR cat -> EndofunctorR cat

  Convert this into a `FunctorR`.

Totality: total
Visibility: public export

.map : (rec : ComonadR 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

.comonadR : ComonadR cat -> ComonadR cat

  Convert this into a `ComonadR`.

Totality: total
Visibility: public export

.cojoin : (rec : ComonadR cat) -> cat .hom (rec .fun a) (rec .fun (rec .fun a))

  The cojoin transformation of the comonad.

Totality: total
Visibility: public export

.counit : (rec : ComonadR cat) -> cat .hom (rec .fun a) a

  The counit transformation of the comonad.

Totality: total
Visibility: public export

record StrongComonadR : MonoidalR -> Type

  A strong comonad is a comonad that is also a costrong functor.
  
  See `StrongComonad` for required laws.

Totality: total
Visibility: public export
Constructor: 

MkStrongComonadR : (fun : (cat .obj -> cat .obj)) -> StrongComonad (cat .hom) (cat .tensor) fun => StrongComonadR cat

Projections:

.cojoin : (rec : StrongComonadR cat) -> cat .hom (rec .fun a) (rec .fun (rec .fun a))

  The cojoin transformation of the comonad.

.comonadR : StrongComonadR cat -> ComonadR (cat .categoryR)

  Convert this into a `ComonadR`.

.costrongFunctorR : StrongComonadR cat -> CostrongFunctorR cat

  Convert this into a `CostrongFunctorR`.

.costrongl : (rec : StrongComonadR cat) -> cat .hom (rec .fun (cat .tensor a b)) (cat .tensor a (rec .fun b))

  The left tensor costrength.

.costrongr : (rec : StrongComonadR cat) -> cat .hom (rec .fun (cat .tensor a b)) (cat .tensor (rec .fun a) b)

  The right tensor costrength.

.counit : (rec : StrongComonadR cat) -> cat .hom (rec .fun a) a

  The counit transformation of the comonad.

.fun : StrongComonadR cat -> cat .obj -> cat .obj

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

  Convert this into a `FunctorR`.

.impl : ({rec:0} : StrongComonadR cat) -> StrongComonad (cat .hom) (cat .tensor) ({rec:0} .fun)

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

  Apply the monad to a morphism in `cat`.

.strongComonadR : StrongComonadR cat -> StrongComonadR cat

  Convert this into a `StrongComonadR`.

.fun : StrongComonadR cat -> cat .obj -> cat .obj

Totality: total
Visibility: public export

.impl : ({rec:0} : StrongComonadR cat) -> StrongComonad (cat .hom) (cat .tensor) ({rec:0} .fun)

Totality: total
Visibility: public export

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

  Convert this into a `FunctorR`.

Totality: total
Visibility: public export

.map : (rec : StrongComonadR 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

.comonadR : StrongComonadR cat -> ComonadR (cat .categoryR)

  Convert this into a `ComonadR`.

Totality: total
Visibility: public export

.cojoin : (rec : StrongComonadR cat) -> cat .hom (rec .fun a) (rec .fun (rec .fun a))

  The cojoin transformation of the comonad.

Totality: total
Visibility: public export

.counit : (rec : StrongComonadR cat) -> cat .hom (rec .fun a) a

  The counit transformation of the comonad.

Totality: total
Visibility: public export

.costrongFunctorR : StrongComonadR cat -> CostrongFunctorR cat

  Convert this into a `CostrongFunctorR`.

Totality: total
Visibility: public export

.costrongl : (rec : StrongComonadR cat) -> cat .hom (rec .fun (cat .tensor a b)) (cat .tensor a (rec .fun b))

  The left tensor costrength.

Totality: total
Visibility: public export

.costrongr : (rec : StrongComonadR cat) -> cat .hom (rec .fun (cat .tensor a b)) (cat .tensor (rec .fun a) b)

  The right tensor costrength.

Totality: total
Visibility: public export

.strongComonadR : StrongComonadR cat -> StrongComonadR cat

  Convert this into a `StrongComonadR`.

Totality: total
Visibility: public export