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.
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)- Totality: total
Visibility: public export .tensor : ({rec:0} : BraidedR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj- Totality: total
Visibility: public export .unit : ({rec:0} : BraidedR) -> {rec:0} .obj- Totality: total
Visibility: public export .impl : ({rec:0} : BraidedR) -> Braided ({rec:0} .hom) ({rec:0} .tensor) ({rec:0} .unit)- Totality: total
Visibility: public export PreBraidedR : Type See `PreMonoidal`.
Totality: total
Visibility: public export.categoryR : BraidedR -> CategoryR Convert this into a `CategoryR`.
Totality: total
Visibility: public export.id : (rec : BraidedR) -> rec .hom a a The identity morphism of an object `a`.
Totality: total
Visibility: public export.comp : (rec : BraidedR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
Totality: total
Visibility: public export.tensorR : (rec : BraidedR) -> EndoBifunctorR (rec .categoryR) Return the tensor product as a `BifunctorR`.
Totality: total
Visibility: public export.monoidalR : BraidedR -> MonoidalR Convert this into a `MonoidalR`.
Totality: total
Visibility: public export.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')`.
Totality: total
Visibility: public export.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)`.
Totality: total
Visibility: public export.unitl : (rec : BraidedR) -> rec .hom (rec .tensor (rec .unit) a) a The left unitor.
Totality: total
Visibility: public export.unitl' : (rec : BraidedR) -> rec .hom a (rec .tensor (rec .unit) a) The inverse of `(.unitl)`, the left unitor.
Totality: total
Visibility: public export.unitr : (rec : BraidedR) -> rec .hom (rec .tensor a (rec .unit)) a The right unitor.
Totality: total
Visibility: public export.unitr' : (rec : BraidedR) -> rec .hom a (rec .tensor a (rec .unit)) The inverse of `(.unitr)`, the right unitor.
Totality: total
Visibility: public export.braidedR : BraidedR -> BraidedR Convert this into a `BraidedR`.
Totality: total
Visibility: public export.braid : (rec : BraidedR) -> rec .hom (rec .tensor a b) (rec .tensor b a) The braiding of the category.
Totality: total
Visibility: public export.braid' : (rec : BraidedR) -> rec .hom (rec .tensor b a) (rec .tensor a b) The inverse of `(.braid)`, the braiding of the category.
Totality: total
Visibility: public export.flipBraid : BraidedR -> BraidedR Invert the braiding of the monoidal category. If the braiding is
symmetric, this does nothing.
Totality: total
Visibility: public exportrecord SymmetricR : Type A monoidal category is *symmetric* when it has a braiding that is
equal to its own inverse.
See `MonSymmetric` for required laws.
Totality: total
Visibility: public export
Constructor: MkSymmetricR : (hom : Hom obj) -> (tensor : (obj -> obj -> obj)) -> (unit : obj) -> MonSymmetric hom tensor unit => SymmetricR
Projections:
.assoc : (rec : SymmetricR) -> 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 : SymmetricR) -> 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 : SymmetricR) -> rec .hom (rec .tensor a b) (rec .tensor b a) The braiding of the category.
.braidedR : SymmetricR -> BraidedR Convert this into a `BraidedR`.
.categoryR : SymmetricR -> CategoryR Convert this into a `CategoryR`.
.comp : (rec : SymmetricR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
.hom : ({rec:0} : SymmetricR) -> Hom ({rec:0} .obj).id : (rec : SymmetricR) -> rec .hom a a The identity morphism of an object `a`.
.impl : ({rec:0} : SymmetricR) -> MonSymmetric ({rec:0} .hom) ({rec:0} .tensor) ({rec:0} .unit).monoidalR : SymmetricR -> MonoidalR Convert this into a `MonoidalR`.
0 .obj : SymmetricR -> Type.tensor : ({rec:0} : SymmetricR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj.tensorR : (rec : SymmetricR) -> EndoBifunctorR (rec .categoryR) Return the tensor product as a `BifunctorR`.
.unit : ({rec:0} : SymmetricR) -> {rec:0} .obj.unitl : (rec : SymmetricR) -> rec .hom (rec .tensor (rec .unit) a) a The left unitor.
.unitl' : (rec : SymmetricR) -> rec .hom a (rec .tensor (rec .unit) a) The inverse of `(.unitl)`, the left unitor.
.unitr : (rec : SymmetricR) -> rec .hom (rec .tensor a (rec .unit)) a The right unitor.
.unitr' : (rec : SymmetricR) -> rec .hom a (rec .tensor a (rec .unit)) The inverse of `(.unitr)`, the right unitor.
.hom : ({rec:0} : SymmetricR) -> Hom ({rec:0} .obj)- Totality: total
Visibility: public export .tensor : ({rec:0} : SymmetricR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj- Totality: total
Visibility: public export .unit : ({rec:0} : SymmetricR) -> {rec:0} .obj- Totality: total
Visibility: public export .impl : ({rec:0} : SymmetricR) -> MonSymmetric ({rec:0} .hom) ({rec:0} .tensor) ({rec:0} .unit)- Totality: total
Visibility: public export PreSymmetricR : Type See `PreMonoidal`.
Totality: total
Visibility: public export.categoryR : SymmetricR -> CategoryR Convert this into a `CategoryR`.
Totality: total
Visibility: public export.id : (rec : SymmetricR) -> rec .hom a a The identity morphism of an object `a`.
Totality: total
Visibility: public export.comp : (rec : SymmetricR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
Totality: total
Visibility: public export.tensorR : (rec : SymmetricR) -> EndoBifunctorR (rec .categoryR) Return the tensor product as a `BifunctorR`.
Totality: total
Visibility: public export.monoidalR : SymmetricR -> MonoidalR Convert this into a `MonoidalR`.
Totality: total
Visibility: public export.assoc : (rec : SymmetricR) -> 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')`.
Totality: total
Visibility: public export.assoc' : (rec : SymmetricR) -> 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)`.
Totality: total
Visibility: public export.unitl : (rec : SymmetricR) -> rec .hom (rec .tensor (rec .unit) a) a The left unitor.
Totality: total
Visibility: public export.unitl' : (rec : SymmetricR) -> rec .hom a (rec .tensor (rec .unit) a) The inverse of `(.unitl)`, the left unitor.
Totality: total
Visibility: public export.unitr : (rec : SymmetricR) -> rec .hom (rec .tensor a (rec .unit)) a The right unitor.
Totality: total
Visibility: public export.unitr' : (rec : SymmetricR) -> rec .hom a (rec .tensor a (rec .unit)) The inverse of `(.unitr)`, the right unitor.
Totality: total
Visibility: public export.braidedR : SymmetricR -> BraidedR Convert this into a `BraidedR`.
Totality: total
Visibility: public export.braid : (rec : SymmetricR) -> rec .hom (rec .tensor a b) (rec .tensor b a) The braiding of the category.
Totality: total
Visibility: public export