record CocartesianR : Type A monoidal category is *cocartesian* if its tensor product
coincides with the categorical coproduct. This automatically
implies that it is symmetric (see `Braided`).
See `Cocartesian` for required laws.
Totality: total
Visibility: public export
Constructor: MkCocartesianR : (hom : Hom obj) -> (tensor : (obj -> obj -> obj)) -> (unit : obj) -> Cocartesian hom tensor unit => CocartesianR
Projections:
.assoc : (rec : CocartesianR) -> 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 : CocartesianR) -> 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 : CocartesianR) -> rec .hom (rec .tensor a b) (rec .tensor b a) The braiding of the category.
.braid' : (rec : CocartesianR) -> rec .hom (rec .tensor b a) (rec .tensor a b) The inverse of `(.braid)`, the braiding of the category.
.braidedR : CocartesianR -> BraidedR Convert this into a `BraidedR`.
.categoryR : CocartesianR -> CategoryR Convert this into a `CategoryR`.
.cocartesianR : CocartesianR -> CocartesianR Convert this into a `CocartesianR`.
.comp : (rec : CocartesianR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
.coprod : (rec : CocartesianR) -> rec .hom a b -> rec .hom a' b -> rec .hom (rec .tensor a a') b The universal property of the coproduct.
.hom : ({rec:0} : CocartesianR) -> Hom ({rec:0} .obj).id : (rec : CocartesianR) -> rec .hom a a The identity morphism of an object `a`.
.impl : ({rec:0} : CocartesianR) -> Cocartesian ({rec:0} .hom) ({rec:0} .tensor) ({rec:0} .unit).injl : (rec : CocartesianR) -> rec .hom a (rec .tensor a b) The left injection of the coproduct.
.injr : (rec : CocartesianR) -> rec .hom b (rec .tensor a b) The right injection of the coproduct.
.intro : (rec : CocartesianR) -> rec .hom (rec .unit) a The unit of the universal monoid structure.
.merge : (rec : CocartesianR) -> rec .hom (rec .tensor a a) a The join of the universal monoid structure.
.monoidalR : CocartesianR -> MonoidalR Convert this into a `MonoidalR`.
0 .obj : CocartesianR -> Type.tensor : ({rec:0} : CocartesianR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj.tensorR : (rec : CocartesianR) -> EndoBifunctorR (rec .categoryR) Return the tensor product as a `BifunctorR`.
.unit : ({rec:0} : CocartesianR) -> {rec:0} .obj.unitl : (rec : CocartesianR) -> rec .hom (rec .tensor (rec .unit) a) a The left unitor.
.unitl' : (rec : CocartesianR) -> rec .hom a (rec .tensor (rec .unit) a) The inverse of `(.unitl)`, the left unitor.
.unitr : (rec : CocartesianR) -> rec .hom (rec .tensor a (rec .unit)) a The right unitor.
.unitr' : (rec : CocartesianR) -> rec .hom a (rec .tensor a (rec .unit)) The inverse of `(.unitr)`, the right unitor.
.hom : ({rec:0} : CocartesianR) -> Hom ({rec:0} .obj)- Totality: total
Visibility: public export .tensor : ({rec:0} : CocartesianR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj- Totality: total
Visibility: public export .unit : ({rec:0} : CocartesianR) -> {rec:0} .obj- Totality: total
Visibility: public export .impl : ({rec:0} : CocartesianR) -> Cocartesian ({rec:0} .hom) ({rec:0} .tensor) ({rec:0} .unit)- Totality: total
Visibility: public export PreCocartesianR : Type See `PreMonoidal`.
Totality: total
Visibility: public export.categoryR : CocartesianR -> CategoryR Convert this into a `CategoryR`.
Totality: total
Visibility: public export.id : (rec : CocartesianR) -> rec .hom a a The identity morphism of an object `a`.
Totality: total
Visibility: public export.comp : (rec : CocartesianR) -> 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 : CocartesianR) -> EndoBifunctorR (rec .categoryR) Return the tensor product as a `BifunctorR`.
Totality: total
Visibility: public export.monoidalR : CocartesianR -> MonoidalR Convert this into a `MonoidalR`.
Totality: total
Visibility: public export.assoc : (rec : CocartesianR) -> 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 : CocartesianR) -> 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 : CocartesianR) -> rec .hom (rec .tensor (rec .unit) a) a The left unitor.
Totality: total
Visibility: public export.unitl' : (rec : CocartesianR) -> rec .hom a (rec .tensor (rec .unit) a) The inverse of `(.unitl)`, the left unitor.
Totality: total
Visibility: public export.unitr : (rec : CocartesianR) -> rec .hom (rec .tensor a (rec .unit)) a The right unitor.
Totality: total
Visibility: public export.unitr' : (rec : CocartesianR) -> rec .hom a (rec .tensor a (rec .unit)) The inverse of `(.unitr)`, the right unitor.
Totality: total
Visibility: public export.braidedR : CocartesianR -> BraidedR Convert this into a `BraidedR`.
Totality: total
Visibility: public export.braid : (rec : CocartesianR) -> rec .hom (rec .tensor a b) (rec .tensor b a) The braiding of the category.
Totality: total
Visibility: public export.braid' : (rec : CocartesianR) -> rec .hom (rec .tensor b a) (rec .tensor a b) The inverse of `(.braid)`, the braiding of the category.
Totality: total
Visibility: public export.cocartesianR : CocartesianR -> CocartesianR Convert this into a `CocartesianR`.
Totality: total
Visibility: public export.injl : (rec : CocartesianR) -> rec .hom a (rec .tensor a b) The left injection of the coproduct.
Totality: total
Visibility: public export.injr : (rec : CocartesianR) -> rec .hom b (rec .tensor a b) The right injection of the coproduct.
Totality: total
Visibility: public export.coprod : (rec : CocartesianR) -> rec .hom a b -> rec .hom a' b -> rec .hom (rec .tensor a a') b The universal property of the coproduct.
Totality: total
Visibility: public export.merge : (rec : CocartesianR) -> rec .hom (rec .tensor a a) a The join of the universal monoid structure.
Totality: total
Visibility: public export.intro : (rec : CocartesianR) -> rec .hom (rec .unit) a The unit of the universal monoid structure.
Totality: total
Visibility: public export