record CartesianR : Type A monoidal category is *cartesian* if its tensor product coincides
with the categorical product. This automatically implies that it
is symmetric (see `Braided`).
See `Cartesian` for required laws.
Totality: total
Visibility: public export
Constructor: MkCartesianR : (hom : Hom obj) -> (tensor : (obj -> obj -> obj)) -> (unit : obj) -> Cartesian hom tensor unit => CartesianR
Projections:
.assoc : (rec : CartesianR) -> 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 : CartesianR) -> 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 : CartesianR) -> rec .hom (rec .tensor a b) (rec .tensor b a) The braiding of the category.
.braidedR : CartesianR -> BraidedR Convert this into a `BraidedR`.
.cartesianR : CartesianR -> CartesianR Convert this into a `CartesianR`.
.categoryR : CartesianR -> CategoryR Convert this into a `CategoryR`.
.comp : (rec : CartesianR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
.elim : (rec : CartesianR) -> rec .hom a (rec .unit) The counit of the universal comonoid structure.
.hom : ({rec:0} : CartesianR) -> Hom ({rec:0} .obj).id : (rec : CartesianR) -> rec .hom a a The identity morphism of an object `a`.
.impl : ({rec:0} : CartesianR) -> Cartesian ({rec:0} .hom) ({rec:0} .tensor) ({rec:0} .unit).monoidalR : CartesianR -> MonoidalR Convert this into a `MonoidalR`.
0 .obj : CartesianR -> Type.prod : (rec : CartesianR) -> rec .hom a b -> rec .hom a b' -> rec .hom a (rec .tensor b b') The universal property of the product.
.projl : (rec : CartesianR) -> rec .hom (rec .tensor a b) a The left projection of the product.
.projr : (rec : CartesianR) -> rec .hom (rec .tensor a b) b The right projection of the product.
.split : (rec : CartesianR) -> rec .hom a (rec .tensor a a) The cojoin of the universal comonoid structure.
.symmetricR : CartesianR -> SymmetricR Convert this into a `SymmetricR`.
.tensor : ({rec:0} : CartesianR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj.tensorR : (rec : CartesianR) -> EndoBifunctorR (rec .categoryR) Return the tensor product as a `BifunctorR`.
.unit : ({rec:0} : CartesianR) -> {rec:0} .obj.unitl : (rec : CartesianR) -> rec .hom (rec .tensor (rec .unit) a) a The left unitor.
.unitl' : (rec : CartesianR) -> rec .hom a (rec .tensor (rec .unit) a) The inverse of `(.unitl)`, the left unitor.
.unitr : (rec : CartesianR) -> rec .hom (rec .tensor a (rec .unit)) a The right unitor.
.unitr' : (rec : CartesianR) -> rec .hom a (rec .tensor a (rec .unit)) The inverse of `(.unitr)`, the right unitor.
.hom : ({rec:0} : CartesianR) -> Hom ({rec:0} .obj)- Totality: total
Visibility: public export .tensor : ({rec:0} : CartesianR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj- Totality: total
Visibility: public export .unit : ({rec:0} : CartesianR) -> {rec:0} .obj- Totality: total
Visibility: public export .impl : ({rec:0} : CartesianR) -> Cartesian ({rec:0} .hom) ({rec:0} .tensor) ({rec:0} .unit)- Totality: total
Visibility: public export PreCartesianR : Type See `PreMonoidal`.
Totality: total
Visibility: public export.categoryR : CartesianR -> CategoryR Convert this into a `CategoryR`.
Totality: total
Visibility: public export.id : (rec : CartesianR) -> rec .hom a a The identity morphism of an object `a`.
Totality: total
Visibility: public export.comp : (rec : CartesianR) -> 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 : CartesianR) -> EndoBifunctorR (rec .categoryR) Return the tensor product as a `BifunctorR`.
Totality: total
Visibility: public export.monoidalR : CartesianR -> MonoidalR Convert this into a `MonoidalR`.
Totality: total
Visibility: public export.assoc : (rec : CartesianR) -> 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 : CartesianR) -> 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 : CartesianR) -> rec .hom (rec .tensor (rec .unit) a) a The left unitor.
Totality: total
Visibility: public export.unitl' : (rec : CartesianR) -> rec .hom a (rec .tensor (rec .unit) a) The inverse of `(.unitl)`, the left unitor.
Totality: total
Visibility: public export.unitr : (rec : CartesianR) -> rec .hom (rec .tensor a (rec .unit)) a The right unitor.
Totality: total
Visibility: public export.unitr' : (rec : CartesianR) -> rec .hom a (rec .tensor a (rec .unit)) The inverse of `(.unitr)`, the right unitor.
Totality: total
Visibility: public export.braidedR : CartesianR -> BraidedR Convert this into a `BraidedR`.
Totality: total
Visibility: public export.symmetricR : CartesianR -> SymmetricR Convert this into a `SymmetricR`.
Totality: total
Visibility: public export.braid : (rec : CartesianR) -> rec .hom (rec .tensor a b) (rec .tensor b a) The braiding of the category.
Totality: total
Visibility: public export.cartesianR : CartesianR -> CartesianR Convert this into a `CartesianR`.
Totality: total
Visibility: public export.projl : (rec : CartesianR) -> rec .hom (rec .tensor a b) a The left projection of the product.
Totality: total
Visibility: public export.projr : (rec : CartesianR) -> rec .hom (rec .tensor a b) b The right projection of the product.
Totality: total
Visibility: public export.prod : (rec : CartesianR) -> rec .hom a b -> rec .hom a b' -> rec .hom a (rec .tensor b b') The universal property of the product.
Totality: total
Visibility: public export.split : (rec : CartesianR) -> rec .hom a (rec .tensor a a) The cojoin of the universal comonoid structure.
Totality: total
Visibility: public export.elim : (rec : CartesianR) -> rec .hom a (rec .unit) The counit of the universal comonoid structure.
Totality: total
Visibility: public export