Control.Category.Records.MonFunctor

Definitions

record LaxMonFunctorR : MonoidalR -> MonoidalR -> Type

  A lax monoidal functor from `cat` to `cat'`.
  
  See `LaxMonFunctor` for required laws.

Totality: total
Visibility: public export
Constructor: 

MkLaxMonFunctorR : (fun : (cat .obj -> cat' .obj)) -> LaxMonFunctor (cat .hom) (cat .tensor) (cat .unit) (cat' .hom) (cat' .tensor) (cat' .unit) fun => LaxMonFunctorR cat cat'

Projections:

.fjoin : (rec : LaxMonFunctorR cat cat') -> cat' .hom (cat' .tensor (rec .fun a) (rec .fun b)) (rec .fun (cat .tensor a b))

  The lax monoidal functor action on the tensor product.

.fun : LaxMonFunctorR cat cat' -> cat .obj -> cat' .obj

.functorR : LaxMonFunctorR cat cat' -> FunctorR (cat .categoryR) (cat' .categoryR)

  Convert this into a `FunctorR`.

.funit : (rec : LaxMonFunctorR cat cat') -> cat' .hom (cat' .unit) (rec .fun (cat .unit))

  The lax monoidal functor action on the unit object.

.impl : ({rec:0} : LaxMonFunctorR cat cat') -> LaxMonFunctor (cat .hom) (cat .tensor) (cat .unit) (cat' .hom) (cat' .tensor) (cat' .unit) ({rec:0} .fun)

.laxMonFunctorR : LaxMonFunctorR cat cat' -> LaxMonFunctorR cat cat'

  Convert this into a `LaxMonFunctorR`.

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

  Apply the functor to a morphism in `cat`.

.fun : LaxMonFunctorR cat cat' -> cat .obj -> cat' .obj

Totality: total
Visibility: public export

.impl : ({rec:0} : LaxMonFunctorR cat cat') -> LaxMonFunctor (cat .hom) (cat .tensor) (cat .unit) (cat' .hom) (cat' .tensor) (cat' .unit) ({rec:0} .fun)

Totality: total
Visibility: public export

LaxMonEndofunctorR : MonoidalR -> Type

  A type synonym for a lax monoidal endofunctor.

Totality: total
Visibility: public export

.functorR : LaxMonFunctorR cat cat' -> FunctorR (cat .categoryR) (cat' .categoryR)

  Convert this into a `FunctorR`.

Totality: total
Visibility: public export

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

.laxMonFunctorR : LaxMonFunctorR cat cat' -> LaxMonFunctorR cat cat'

  Convert this into a `LaxMonFunctorR`.

Totality: total
Visibility: public export

.fjoin : (rec : LaxMonFunctorR cat cat') -> cat' .hom (cat' .tensor (rec .fun a) (rec .fun b)) (rec .fun (cat .tensor a b))

  The lax monoidal functor action on the tensor product.

Totality: total
Visibility: public export

.funit : (rec : LaxMonFunctorR cat cat') -> cat' .hom (cat' .unit) (rec .fun (cat .unit))

  The lax monoidal functor action on the unit object.

Totality: total
Visibility: public export

record MonFunctorR : MonoidalR -> MonoidalR -> Type

  A (strong) monoidal functor from `cat` to `cat'`.
  
  See `MonFunctor` for required laws.

Totality: total
Visibility: public export
Constructor: 

MkMonFunctorR : (fun : (cat .obj -> cat' .obj)) -> MonFunctor (cat .hom) (cat .tensor) (cat .unit) (cat' .hom) (cat' .tensor) (cat' .unit) fun => MonFunctorR cat cat'

Projections:

.fjoin : (rec : MonFunctorR cat cat') -> cat' .hom (cat' .tensor (rec .fun a) (rec .fun b)) (rec .fun (cat .tensor a b))

  The monoidal functor action on the tensor product.

.fjoin' : (rec : MonFunctorR cat cat') -> cat' .hom (rec .fun (cat .tensor a b)) (cat' .tensor (rec .fun a) (rec .fun b))

  The inverse monoidal functor action on the tensor product.

.fun : MonFunctorR cat cat' -> cat .obj -> cat' .obj

.functorR : MonFunctorR cat cat' -> FunctorR (cat .categoryR) (cat' .categoryR)

  Convert this into a `FunctorR`.

.funit : (rec : MonFunctorR cat cat') -> cat' .hom (cat' .unit) (rec .fun (cat .unit))

  The monoidal functor action on the unit object.

.funit' : (rec : MonFunctorR cat cat') -> cat' .hom (rec .fun (cat .unit)) (cat' .unit)

  The inverse monoidal functor action on the unit object.

.impl : ({rec:0} : MonFunctorR cat cat') -> MonFunctor (cat .hom) (cat .tensor) (cat .unit) (cat' .hom) (cat' .tensor) (cat' .unit) ({rec:0} .fun)

.laxMonFunctorR : MonFunctorR cat cat' -> LaxMonFunctorR cat cat'

  Convert this into a `LaxMonFunctorR`.

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

  Apply the functor to a morphism in `cat`.

.monFunctorR : MonFunctorR cat cat' -> MonFunctorR cat cat'

  Convert this into a `MonFunctorR`.

.fun : MonFunctorR cat cat' -> cat .obj -> cat' .obj

Totality: total
Visibility: public export

.impl : ({rec:0} : MonFunctorR cat cat') -> MonFunctor (cat .hom) (cat .tensor) (cat .unit) (cat' .hom) (cat' .tensor) (cat' .unit) ({rec:0} .fun)

Totality: total
Visibility: public export

MonEndofunctorR : MonoidalR -> Type

  A type synonym for a monoidal endofunctor.

Totality: total
Visibility: public export

.functorR : MonFunctorR cat cat' -> FunctorR (cat .categoryR) (cat' .categoryR)

  Convert this into a `FunctorR`.

Totality: total
Visibility: public export

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

.laxMonFunctorR : MonFunctorR cat cat' -> LaxMonFunctorR cat cat'

  Convert this into a `LaxMonFunctorR`.

Totality: total
Visibility: public export

.fjoin : (rec : MonFunctorR cat cat') -> cat' .hom (cat' .tensor (rec .fun a) (rec .fun b)) (rec .fun (cat .tensor a b))

  The monoidal functor action on the tensor product.

Totality: total
Visibility: public export

.funit : (rec : MonFunctorR cat cat') -> cat' .hom (cat' .unit) (rec .fun (cat .unit))

  The monoidal functor action on the unit object.

Totality: total
Visibility: public export

.monFunctorR : MonFunctorR cat cat' -> MonFunctorR cat cat'

  Convert this into a `MonFunctorR`.

Totality: total
Visibility: public export

.fjoin' : (rec : MonFunctorR cat cat') -> cat' .hom (rec .fun (cat .tensor a b)) (cat' .tensor (rec .fun a) (rec .fun b))

  The inverse monoidal functor action on the tensor product.

Totality: total
Visibility: public export

.funit' : (rec : MonFunctorR cat cat') -> cat' .hom (rec .fun (cat .unit)) (cat' .unit)

  The inverse monoidal functor action on the unit object.

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 CostrongFunctorR : MonoidalR -> Type

  An endofunctor has *tensorial costrength* if it is compatible with
  a monoidal category's tensor product in a way that is dual to a
  tensorial strength.
  
  See `CostrongFunctor` for required laws.

Totality: total
Visibility: public export
Constructor: 

MkCostrongFunctorR : (fun : (cat .obj -> cat .obj)) -> CostrongFunctor (cat .hom) (cat .tensor) fun => CostrongFunctorR cat

Projections:

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

  The left tensor costrength.

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

  The right tensor costrength.

.fun : CostrongFunctorR cat -> cat .obj -> cat .obj

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

  Convert this into a `FunctorR`.

.impl : ({rec:0} : CostrongFunctorR cat) -> CostrongFunctor (cat .hom) (cat .tensor) ({rec:0} .fun)

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

  Apply the functor to a morphism in `cat`.

.fun : CostrongFunctorR cat -> cat .obj -> cat .obj

Totality: total
Visibility: public export

.impl : ({rec:0} : CostrongFunctorR cat) -> CostrongFunctor (cat .hom) (cat .tensor) ({rec:0} .fun)

Totality: total
Visibility: public export

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

  Convert this into a `FunctorR`.

Totality: total
Visibility: public export

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

.costrongl : (rec : CostrongFunctorR 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 : CostrongFunctorR cat) -> cat .hom (rec .fun (cat .tensor a b)) (cat .tensor (rec .fun a) b)

  The right tensor costrength.

Totality: total
Visibility: public export