With braiding
With duals for objects
category with duals (list of them)
dualizable object (what they have)
ribbon category, a.k.a. tortile category
With duals for morphisms
monoidal dagger-category?
With traces
Closed structure
Special sorts of products
Semisimplicity
Morphisms
Internal monoids
Examples
Theorems
In higher category theory
hom-set, hom-object, internal hom, exponential object, derived hom-space
loop space object, free loop space object, derived loop space
Let $\big(\mathcal{C}, \otimes, \mathbb{1}\big)$ be a closed monoidal category. For $S, D \in C$ two objects, with internal hom $[S, \text{-}]$ right adjoint to the tensor product $S \otimes (\text{-})$, the evaluation map
is the counit of this adjunction, hence the adjunct of the identity morphism
Concretely for $\mathcal{C}$ = Sets or generally on generalized elements, the evaluation map is given by evaluating a function at a value, whence the name:
If $\mathcal{C}$ is moreover compact then for $D = \mathbb{1}$ the tensor unit we have that $[S, \mathbb{1}] \,=\, S^\ast$ is the dual object to $S$, whence the evaluation map becomes the pairing of objects with their duals
Therefore, sometimes the pairing map on dual objects may be called βevaluationβ even when the ambient category is not compact closed.
In a cartesian closed category the evaluation map
is the categorical semantics of what in the type theory internal language is the dependent type whose syntax is
expressing function application. On propositions ((-1)-truncated types) this is the modus ponens deduction rule.
concrete category (for the external version)
Last revised on September 10, 2023 at 13:36:43. See the history of this page for a list of all contributions to it.