interface LaxMonFunctor : Hom obj -> (obj -> obj -> obj) -> obj -> Hom obj' -> (obj' -> obj' -> obj') -> obj' -> (obj -> obj') -> Type A lax monoidal functor from `cat` to `cat'`.
This is the interface-style definition of a lax monoidal functor.
For the record-style definition, see `Control.Category.Records.LaxMonFunctorR`.
Laws:
* `map assoc . fjoin . mapl fjoin = fjoin . mapr fjoin . assoc`
* `map unitl . fjoin . mapl funit = unitl`
* `map unitr . fjoin . mapr funit = unitr`
Parameters: cat, ten, i, cat', ten', i', f
Constraints: CatFunctor cat cat' f
Constructor: MkLaxMonFunctor
Methods:
fjoin : cat' (ten' (f a) (f b)) (f (ten a b)) The lax monoidal functor action on the tensor product.
funit : cat' i' (f i) The lax monoidal functor action on the unit object.
Implementation: MonFunctor cat ten i cat' ten' i' f -> LaxMonFunctor cat ten i cat' ten' i' f
fjoin : LaxMonFunctor cat ten i cat' ten' i' f => cat' (ten' (f a) (f b)) (f (ten a b)) The lax monoidal functor action on the tensor product.
Totality: total
Visibility: public exportfunit : LaxMonFunctor cat ten i cat' ten' i' f => cat' i' (f i) The lax monoidal functor action on the unit object.
Totality: total
Visibility: public exportLaxMonEndofunctor : Hom obj -> (obj -> obj -> obj) -> obj -> (obj -> obj) -> Type A type synonym for a lax monoidal endofunctor, a lax monoidal
functor from a monoidal category to itself.
This is the interface-style definition of a lax monoidal
endofunctor. For the record-style definition, see
`Control.Category.Records.LaxMonEndofunctorR`.
Totality: total
Visibility: public exportinterface MonFunctor : Hom obj -> (obj -> obj -> obj) -> obj -> Hom obj' -> (obj' -> obj' -> obj') -> obj' -> (obj -> obj') -> Type A (strong) monoidal functor from `cat` to `cat'`.
This is the interface-style definition of a monoidal functor. For
the record-style definition, see `Control.Category.Records.MonFunctorR`.
Laws:
* `funit . funit' = funit' . funit = id`
* `fjoin . fjoin' = fjoin' . fjoin = id`
Parameters: cat, ten, i, cat', ten', i', f
Constraints: LaxMonFunctor cat ten i cat' ten' i' f
Constructor: MkMonFunctor
Methods:
fjoin' : cat' (f (ten a b)) (ten' (f a) (f b)) The inverse monoidal functor action on the tensor product.
This is the inverse of `fjoin`.
funit' : cat' (f i) i' The inverse monoidal functor action on the unit object.
This is the inverse of `funit`.
fjoin' : MonFunctor cat ten i cat' ten' i' f => cat' (f (ten a b)) (ten' (f a) (f b)) The inverse monoidal functor action on the tensor product.
This is the inverse of `fjoin`.
Totality: total
Visibility: public exportfunit' : MonFunctor cat ten i cat' ten' i' f => cat' (f i) i' The inverse monoidal functor action on the unit object.
This is the inverse of `funit`.
Totality: total
Visibility: public exportMonEndofunctor : Hom obj -> (obj -> obj -> obj) -> obj -> (obj -> obj) -> Type A type synonym for a monoidal endofunctor, a monoidal functor from
a monoidal category to itself.
This is the interface-style definition of a monoidal endofunctor.
For the record-style definition, see `Control.Category.Records.MonEndofunctorR`.
Totality: total
Visibility: public exportinterface StrongFunctor : Hom obj -> (obj -> obj -> obj) -> (obj -> obj) -> Type An endofunctor has *tensorial strength* if it is compatible with a
monoidal category's tensor product. Generally, `cat` is a monoidal
category with `ten` as its tensor product, though this is not
enforced by the interface.
Note that while all Prelude functors have strength over `Pair`,
this does not necessarily hold for other tensor products or in
other categories.
This is the interface-style definition of a strong functor. For
the record-style definition, see `Control.Category.Records.StrongFunctorR`.
Laws (when `cat` is a monoidal category):
* `map unitl . strongl = unitl`
* `map unitr . strongr = unitr`
* `map assoc . strongl = strongl . mapr strongl . assoc`
* `map assoc' . strongr = strongr . mapl strongr . assoc'`
* `strongr . mapl strongl = strongl . mapr strongr . assoc`
Parameters: cat, ten, f
Constraints: CatFunctor cat cat f
Constructor: MkStrongFunctor
Methods:
strongl : cat (ten a (f b)) (f (ten a b)) The left tensor strength.
strongr : cat (ten (f a) b) (f (ten a b)) The right tensor strength.
strongl : StrongFunctor cat ten f => cat (ten a (f b)) (f (ten a b)) The left tensor strength.
Totality: total
Visibility: public exportstrongr : StrongFunctor cat ten f => cat (ten (f a) b) (f (ten a b)) The right tensor strength.
Totality: total
Visibility: public exportinterface CostrongFunctor : Hom obj -> (obj -> obj -> obj) -> (obj -> obj) -> 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. Generally, `cat` is a monoidal category with
`ten` as its tensor product, though this is not enforced by the
interface.
This is the interface-style definition of a costrong functor. For
the record-style definition, see `Control.Category.Records.CostrongFunctorR`.
Laws (when `cat` is a monoidal category):
* `unitl . costrongl = map unitl`
* `unitr . costrongr = map unitr`
* `costrongl . map assoc' = assoc' . mapr costrongl . costrongl`
* `costrongr . map assoc' = assoc' . mapl costrongr . costrongr`
* `mapl costrongl . cstrongr = assoc' . mapr costrongr . costrongl`
Parameters: cat, ten, f
Constraints: CatFunctor cat cat f
Constructor: MkCostrongFunctor
Methods:
costrongl : cat (f (ten a b)) (ten a (f b)) The left tensor costrength.
costrongr : cat (f (ten a b)) (ten (f a) b) The right tensor costrength.
costrongl : CostrongFunctor cat ten f => cat (f (ten a b)) (ten a (f b)) The left tensor costrength.
Totality: total
Visibility: public exportcostrongr : CostrongFunctor cat ten f => cat (f (ten a b)) (ten (f a) b) The right tensor costrength.
Totality: total
Visibility: public export