Control.Category.Closed

Definitions

interface Closed : Hom obj -> (obj -> obj -> obj) -> (obj -> obj -> obj) -> obj -> Type

  A monoidal category is *closed* if it can meaningfully represent
  its morphisms as an object inside of itself. More specifically,
  the internal hom ``(a `hom` b)`` is an object that encodes the
  set of morphisms from `a` to `b`.
  
  Formally, a monoidal category is closed if the functor
  ``(`ten` a)`` has a right adjoint functor `hom a`.
  
  This is the interface-style definition of a closed monoidal category.
  For the record-style definition, see `Control.Category.Records.ClosedR`.
  
  Laws:
  * `curry` is natural in `a`,`b`,`c` (see `NatTrans`)
  * `uncurry` is natural in `a`,`b`,`c` (see `NatTrans`)

Parameters: cat, ten, hom, i
Constraints: Monoidal cat ten i
Constructor: 

MkClosed

Methods:

curry : cat (ten a b) c -> cat a (hom b c)

  The currying transformation.

uncurry : cat a (hom b c) -> cat (ten a b) c

  The uncurrying transformation.

Implementations:

Closed Morphism Pair Morphism ()

Closed Morphism Pair (~~>) ()

curry : Closed cat ten hom i => cat (ten a b) c -> cat a (hom b c)

  The currying transformation.

Totality: total
Visibility: public export

uncurry : Closed cat ten hom i => cat a (hom b c) -> cat (ten a b) c

  The uncurrying transformation.

Totality: total
Visibility: public export

CartesianClosed : Hom obj -> (obj -> obj -> obj) -> (obj -> obj -> obj) -> obj -> Type

  A monoidal category that is both cartesian and closed.
  
  This is the interface-style definition of a cartesian closed
  monoidal category. For the record-style definition, see
  `Control.Category.Records.CartesianClosedR`.

Totality: total
Visibility: public export

eval : Closed cat ten hom i => cat (ten (hom a b) a) b

  The evaluation map of a closed monoidal category.

Totality: total
Visibility: public export

coeval : Closed cat ten hom i => cat a (hom b (ten a b))

  The coevaluation map of a closed monoidal category.

Totality: total
Visibility: public export