record ClosedR : Type A monoidal category is *closed* if it can meaningfully represent
its morphisms as an object inside of itself. More specifically,
the internal hom `ihom a b` is an object that encodes the set of
morphisms from `a` to `b`.
Formally, a monoidal category is closed if the functor
``(`tensor` a)`` has a right adjoint functor `ihom a`.
See `Closed` for required laws.
Totality: total
Visibility: public export
Constructor: MkClosedR : (hom : Hom obj) -> (tensor : (obj -> obj -> obj)) -> (ihom : (obj -> obj -> obj)) -> (unit : obj) -> Closed hom tensor ihom unit => ClosedR
Projections:
.assoc : (rec : ClosedR) -> 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 : ClosedR) -> 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)`.
.categoryR : ClosedR -> CategoryR Convert this into a `CategoryR`.
.closedR : ClosedR -> ClosedR Convert this into a `ClosedR`.
.coeval : (rec : ClosedR) -> rec .hom a (rec .ihom b (rec .tensor a b)) The coevaluation map.
.comp : (rec : ClosedR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
.curry : (rec : ClosedR) -> rec .hom (rec .tensor a b) c -> rec .hom a (rec .ihom b c) The currying transformation.
.eval : (rec : ClosedR) -> rec .hom (rec .tensor (rec .ihom a b) a) b The evaluation map.
.hom : ({rec:0} : ClosedR) -> Hom ({rec:0} .obj).id : (rec : ClosedR) -> rec .hom a a The identity morphism of an object `a`.
.ihom : ({rec:0} : ClosedR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj.impl : ({rec:0} : ClosedR) -> Closed ({rec:0} .hom) ({rec:0} .tensor) ({rec:0} .ihom) ({rec:0} .unit).monoidalR : ClosedR -> MonoidalR Convert this into a `MonoidalR`.
0 .obj : ClosedR -> Type.tensor : ({rec:0} : ClosedR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj.tensorR : (rec : ClosedR) -> EndoBifunctorR (rec .categoryR) Return the tensor product as a `BifunctorR`.
.uncurry : (rec : ClosedR) -> rec .hom a (rec .ihom b c) -> rec .hom (rec .tensor a b) c The uncurrying transformation.
.unit : ({rec:0} : ClosedR) -> {rec:0} .obj.unitl : (rec : ClosedR) -> rec .hom (rec .tensor (rec .unit) a) a The left unitor.
.unitl' : (rec : ClosedR) -> rec .hom a (rec .tensor (rec .unit) a) The inverse of `(.unitl)`, the left unitor.
.unitr : (rec : ClosedR) -> rec .hom (rec .tensor a (rec .unit)) a The right unitor.
.unitr' : (rec : ClosedR) -> rec .hom a (rec .tensor a (rec .unit)) The inverse of `(.unitr)`, the right unitor.
.hom : ({rec:0} : ClosedR) -> Hom ({rec:0} .obj)- Totality: total
Visibility: public export .tensor : ({rec:0} : ClosedR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj- Totality: total
Visibility: public export .ihom : ({rec:0} : ClosedR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj- Totality: total
Visibility: public export .unit : ({rec:0} : ClosedR) -> {rec:0} .obj- Totality: total
Visibility: public export .impl : ({rec:0} : ClosedR) -> Closed ({rec:0} .hom) ({rec:0} .tensor) ({rec:0} .ihom) ({rec:0} .unit)- Totality: total
Visibility: public export .categoryR : ClosedR -> CategoryR Convert this into a `CategoryR`.
Totality: total
Visibility: public export.id : (rec : ClosedR) -> rec .hom a a The identity morphism of an object `a`.
Totality: total
Visibility: public export.comp : (rec : ClosedR) -> 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 : ClosedR) -> EndoBifunctorR (rec .categoryR) Return the tensor product as a `BifunctorR`.
Totality: total
Visibility: public export.monoidalR : ClosedR -> MonoidalR Convert this into a `MonoidalR`.
Totality: total
Visibility: public export.assoc : (rec : ClosedR) -> 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 : ClosedR) -> 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 : ClosedR) -> rec .hom (rec .tensor (rec .unit) a) a The left unitor.
Totality: total
Visibility: public export.unitl' : (rec : ClosedR) -> rec .hom a (rec .tensor (rec .unit) a) The inverse of `(.unitl)`, the left unitor.
Totality: total
Visibility: public export.unitr : (rec : ClosedR) -> rec .hom (rec .tensor a (rec .unit)) a The right unitor.
Totality: total
Visibility: public export.unitr' : (rec : ClosedR) -> rec .hom a (rec .tensor a (rec .unit)) The inverse of `(.unitr)`, the right unitor.
Totality: total
Visibility: public export.closedR : ClosedR -> ClosedR Convert this into a `ClosedR`.
Totality: total
Visibility: public export.curry : (rec : ClosedR) -> rec .hom (rec .tensor a b) c -> rec .hom a (rec .ihom b c) The currying transformation.
Totality: total
Visibility: public export.uncurry : (rec : ClosedR) -> rec .hom a (rec .ihom b c) -> rec .hom (rec .tensor a b) c The uncurrying transformation.
Totality: total
Visibility: public export.eval : (rec : ClosedR) -> rec .hom (rec .tensor (rec .ihom a b) a) b The evaluation map.
Totality: total
Visibility: public export.coeval : (rec : ClosedR) -> rec .hom a (rec .ihom b (rec .tensor a b)) The coevaluation map.
Totality: total
Visibility: public exportrecord CartesianClosedR : Type A monoidal category that is both cartesian and closed.
Totality: total
Visibility: public export
Constructor: MkCartesianClosedR : (hom : Hom obj) -> (tensor : (obj -> obj -> obj)) -> (ihom : (obj -> obj -> obj)) -> (unit : obj) -> CartesianClosed hom tensor ihom unit => CartesianClosedR
Projections:
.assoc : (rec : CartesianClosedR) -> 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 : CartesianClosedR) -> 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 : CartesianClosedR) -> rec .hom (rec .tensor a b) (rec .tensor b a) The braiding of the category.
.braid' : (rec : CartesianClosedR) -> rec .hom (rec .tensor b a) (rec .tensor a b) The inverse of `(.braid)`, the braiding of the category.
.braidedR : CartesianClosedR -> BraidedR Convert this into a `BraidedR`.
.cartesianR : CartesianClosedR -> CartesianR Convert this into a `CartesianR`.
.categoryR : CartesianClosedR -> CategoryR Convert this into a `CategoryR`.
.closedR : CartesianClosedR -> ClosedR Convert this into a `ClosedR`.
.coeval : (rec : CartesianClosedR) -> rec .hom a (rec .ihom b (rec .tensor a b)) The coevaluation map.
.comp : (rec : CartesianClosedR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
.curry : (rec : CartesianClosedR) -> rec .hom (rec .tensor a b) c -> rec .hom a (rec .ihom b c) The currying transformation.
.elim : (rec : CartesianClosedR) -> rec .hom a (rec .unit) The counit of the universal comonoid structure.
.eval : (rec : CartesianClosedR) -> rec .hom (rec .tensor (rec .ihom a b) a) b The evaluation map.
.hom : ({rec:0} : CartesianClosedR) -> Hom ({rec:0} .obj).id : (rec : CartesianClosedR) -> rec .hom a a The identity morphism of an object `a`.
.ihom : ({rec:0} : CartesianClosedR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj.impl : ({rec:0} : CartesianClosedR) -> CartesianClosed ({rec:0} .hom) ({rec:0} .tensor) ({rec:0} .ihom) ({rec:0} .unit).monoidalR : CartesianClosedR -> MonoidalR Convert this into a `MonoidalR`.
0 .obj : CartesianClosedR -> Type.prod : (rec : CartesianClosedR) -> rec .hom a b -> rec .hom a b' -> rec .hom a (rec .tensor b b') The universal property of the product.
.projl : (rec : CartesianClosedR) -> rec .hom (rec .tensor a b) a The left projection of the product.
.projr : (rec : CartesianClosedR) -> rec .hom (rec .tensor a b) b The right projection of the product.
.split : (rec : CartesianClosedR) -> rec .hom a (rec .tensor a a) The cojoin of the universal comonoid structure.
.tensor : ({rec:0} : CartesianClosedR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj.tensorR : (rec : CartesianClosedR) -> EndoBifunctorR (rec .categoryR) Return the tensor product as a `BifunctorR`.
.uncurry : (rec : CartesianClosedR) -> rec .hom a (rec .ihom b c) -> rec .hom (rec .tensor a b) c The uncurrying transformation.
.unit : ({rec:0} : CartesianClosedR) -> {rec:0} .obj.unitl : (rec : CartesianClosedR) -> rec .hom (rec .tensor (rec .unit) a) a The left unitor.
.unitl' : (rec : CartesianClosedR) -> rec .hom a (rec .tensor (rec .unit) a) The inverse of `(.unitl)`, the left unitor.
.unitr : (rec : CartesianClosedR) -> rec .hom (rec .tensor a (rec .unit)) a The right unitor.
.unitr' : (rec : CartesianClosedR) -> rec .hom a (rec .tensor a (rec .unit)) The inverse of `(.unitr)`, the right unitor.
.hom : ({rec:0} : CartesianClosedR) -> Hom ({rec:0} .obj)- Totality: total
Visibility: public export .tensor : ({rec:0} : CartesianClosedR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj- Totality: total
Visibility: public export .ihom : ({rec:0} : CartesianClosedR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj- Totality: total
Visibility: public export .unit : ({rec:0} : CartesianClosedR) -> {rec:0} .obj- Totality: total
Visibility: public export .impl : ({rec:0} : CartesianClosedR) -> CartesianClosed ({rec:0} .hom) ({rec:0} .tensor) ({rec:0} .ihom) ({rec:0} .unit)- Totality: total
Visibility: public export CCC : Type A shorter synonym for a cartesian closed category (`CartesianClosedR`).
Totality: total
Visibility: public export.categoryR : CartesianClosedR -> CategoryR Convert this into a `CategoryR`.
Totality: total
Visibility: public export.id : (rec : CartesianClosedR) -> rec .hom a a The identity morphism of an object `a`.
Totality: total
Visibility: public export.comp : (rec : CartesianClosedR) -> 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 : CartesianClosedR) -> EndoBifunctorR (rec .categoryR) Return the tensor product as a `BifunctorR`.
Totality: total
Visibility: public export.monoidalR : CartesianClosedR -> MonoidalR Convert this into a `MonoidalR`.
Totality: total
Visibility: public export.assoc : (rec : CartesianClosedR) -> 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 : CartesianClosedR) -> 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 : CartesianClosedR) -> rec .hom (rec .tensor (rec .unit) a) a The left unitor.
Totality: total
Visibility: public export.unitl' : (rec : CartesianClosedR) -> rec .hom a (rec .tensor (rec .unit) a) The inverse of `(.unitl)`, the left unitor.
Totality: total
Visibility: public export.unitr : (rec : CartesianClosedR) -> rec .hom (rec .tensor a (rec .unit)) a The right unitor.
Totality: total
Visibility: public export.unitr' : (rec : CartesianClosedR) -> rec .hom a (rec .tensor a (rec .unit)) The inverse of `(.unitr)`, the right unitor.
Totality: total
Visibility: public export.braidedR : CartesianClosedR -> BraidedR Convert this into a `BraidedR`.
Totality: total
Visibility: public export.braid : (rec : CartesianClosedR) -> rec .hom (rec .tensor a b) (rec .tensor b a) The braiding of the category.
Totality: total
Visibility: public export.braid' : (rec : CartesianClosedR) -> rec .hom (rec .tensor b a) (rec .tensor a b) The inverse of `(.braid)`, the braiding of the category.
Totality: total
Visibility: public export.cartesianR : CartesianClosedR -> CartesianR Convert this into a `CartesianR`.
Totality: total
Visibility: public export.projl : (rec : CartesianClosedR) -> rec .hom (rec .tensor a b) a The left projection of the product.
Totality: total
Visibility: public export.projr : (rec : CartesianClosedR) -> rec .hom (rec .tensor a b) b The right projection of the product.
Totality: total
Visibility: public export.prod : (rec : CartesianClosedR) -> 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 : CartesianClosedR) -> rec .hom a (rec .tensor a a) The cojoin of the universal comonoid structure.
Totality: total
Visibility: public export.elim : (rec : CartesianClosedR) -> rec .hom a (rec .unit) The counit of the universal comonoid structure.
Totality: total
Visibility: public export.closedR : CartesianClosedR -> ClosedR Convert this into a `ClosedR`.
Totality: total
Visibility: public export.curry : (rec : CartesianClosedR) -> rec .hom (rec .tensor a b) c -> rec .hom a (rec .ihom b c) The currying transformation.
Totality: total
Visibility: public export.uncurry : (rec : CartesianClosedR) -> rec .hom a (rec .ihom b c) -> rec .hom (rec .tensor a b) c The uncurrying transformation.
Totality: total
Visibility: public export.eval : (rec : CartesianClosedR) -> rec .hom (rec .tensor (rec .ihom a b) a) b The evaluation map.
Totality: total
Visibility: public export.coeval : (rec : CartesianClosedR) -> rec .hom a (rec .ihom b (rec .tensor a b)) The coevaluation map.
Totality: total
Visibility: public export