evaluation map in nLab

Contents

Contents

Definition

Let (𝒞,⊗,𝟙)\big(\mathcal{C}, \otimes, \mathbb{1}\big) be a closed monoidal category. For S,D∈CS, D \in C two objects, with internal hom [S,-][S, \text{-}] right adjoint to the tensor product S⊗(-)S \otimes (\text{-}), the evaluation map

ev:S⊗[S,D]→D ev \;\colon\; S \otimes [S, D] \to D

is the counit of this adjunction, hence the adjunct of the identity morphism

Id:[S,D]→[S,D]. Id \;\colon\; [S,D] \to [S,D] \,.

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:

S×[S,D] ⟶ev D (s,f) ↦ f(s). \array{ S \times [S,D] &\overset{ev}{\longrightarrow}& D \\ \big( s ,\, f \big) &\mapsto& f(s) \mathrlap{\,.} }

If 𝒞\mathcal{C} is moreover compact then for D=𝟙D = \mathbb{1} the tensor unit we have that [S,𝟙]=S *[S, \mathbb{1}] \,=\, S^\ast is the dual object to SS, whence the evaluation map becomes the pairing of objects with their duals

S⊗S *⟶ev𝟙. S \otimes S^\ast \overset{ev}{\longrightarrow} \mathbb{1} \,.

Therefore, sometimes the pairing map on dual objects may be called “evaluation” even when the ambient category is not compact closed.

Properties

Syntax and semantics

In a cartesian closed category the evaluation map

[X,Y]×X→evalY [X,Y]\times X \stackrel{eval}{\to} Y

is the categorical semantics of what in the type theory internal language is the dependent type whose syntax is

f:X→Y,x:X⊢f(x):Y f \colon X \to Y ,\; x \colon X \; \vdash \; f(x) \colon Y

expressing function application. On propositions ((-1)-truncated types) this is the modus ponens deduction rule.

See also

• coevaluation map

• state monad, costate comonad

• concrete category (for the external version)