Control.Category.Records.Cartesian

Definitions

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.

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

  The inverse of `(.braid)`, 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.

.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)