Control.Category.Records.Braided

Definitions

record BraidedR : Type

  A monoidal category is *braided* when it is possible to flip the
  order of the tensor product in a coherent way, determined by the
  braiding isomorphism.
  
  Additionally, a braided monoidal category may be *symmetric*,
  requiring that `(.braid) = (.braid')`. Since the only difference
  is in laws, the same record is used for this case.
  
  See `Braided` for required laws.

Totality: total
Visibility: public export
Constructor:

MkBraidedR : (hom : Hom obj) -> (tensor : (obj -> obj -> obj)) -> (unit : obj) -> Braided hom tensor unit => BraidedR

Projections:

.assoc : (rec : BraidedR) -> 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 : BraidedR) -> 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)`.

.braid : (rec : BraidedR) -> rec .hom (rec .tensor a b) (rec .tensor b a)

  The braiding of the category.

.braid' : (rec : BraidedR) -> rec .hom (rec .tensor b a) (rec .tensor a b)

  The inverse of `(.braid)`, the braiding of the category.

.braidedR : BraidedR -> BraidedR

  Convert this into a `BraidedR`.

.categoryR : BraidedR -> CategoryR

  Convert this into a `CategoryR`.

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

  Binary right-to-left composition of morphisms.

.flipBraid : BraidedR -> BraidedR

  Invert the braiding of the monoidal category. If the braiding is
  symmetric, this does nothing.

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

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

  The identity morphism of an object `a`.

.impl : ({rec:0} : BraidedR) -> Braided ({rec:0} .hom) ({rec:0} .tensor) ({rec:0} .unit)

.monoidalR : BraidedR -> MonoidalR

  Convert this into a `MonoidalR`.

0 .obj : BraidedR -> Type

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

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

  Return the tensor product as a `BifunctorR`.

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

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

  The left unitor.

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

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

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

  The right unitor.

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

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

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