Control.Category.Records.Monoidal

Definitions

record MonoidalR : Type

  A *monoidal category* is a category equipped with a binary operator
  on its objects called the *tensor product* that respects its
  internal structure. This operation is required to be a monoid,
  that is to be associative and have an identity object (up to
  isomorphism).
  
  See `Monoidal` for required laws.

Totality: total
Visibility: public export
Constructor:

MkMonoidalR : (hom : Hom obj) -> (tensor : (obj -> obj -> obj)) -> (unit : obj) -> Monoidal hom tensor unit => MonoidalR

Projections:

.assoc : (rec : MonoidalR) -> rec .hom (rec .tensor (rec .tensor a b) c) (rec .tensor a (rec .tensor b c))

  The left-biased associator. This must be the inverse of `(.assoc')`.

.assoc' : (rec : MonoidalR) -> rec .hom (rec .tensor a (rec .tensor b c)) (rec .tensor (rec .tensor a b) c)

  The right-biased associator. This must be the inverse of `(.assoc)`.

.categoryR : MonoidalR -> CategoryR

  Convert this into a `CategoryR`.

.comp : (rec : MonoidalR) -> rec .hom b c -> rec .hom a b -> rec .hom a c

  Binary right-to-left composition of morphisms.

.hom : ({rec:0} : MonoidalR) -> Hom ({rec:0} .obj)

.id : (rec : MonoidalR) -> rec .hom a a

  The identity morphism of an object `a`.

.impl : ({rec:0} : MonoidalR) -> Monoidal ({rec:0} .hom) ({rec:0} .tensor) ({rec:0} .unit)

.monoidalR : MonoidalR -> MonoidalR

  Convert this into a `MonoidalR`.

0 .obj : MonoidalR -> Type

.tensor : ({rec:0} : MonoidalR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj

.tensorR : (rec : MonoidalR) -> EndoBifunctorR (rec .categoryR)

  Return the tensor product as a `BifunctorR`.

.unit : ({rec:0} : MonoidalR) -> {rec:0} .obj

.unitl : (rec : MonoidalR) -> rec .hom (rec .tensor (rec .unit) a) a

  The left unitor.

.unitl' : (rec : MonoidalR) -> rec .hom a (rec .tensor (rec .unit) a)

  The inverse of `(.unitl)`, the left unitor.

.unitr : (rec : MonoidalR) -> rec .hom (rec .tensor a (rec .unit)) a

  The right unitor.

.unitr' : (rec : MonoidalR) -> rec .hom a (rec .tensor a (rec .unit))

  The inverse of `(.unitr)`, the right unitor.

.hom : ({rec:0} : MonoidalR) -> Hom ({rec:0} .obj)