nLab evaluation map

Definition

Let $C$ be a closed monoidal category. For $X,Y \in C$ two objects, the adjunct

$$ev : [X,Y]\otimes X \to Y$$

of the identity morphism

$$Id : [X,Y] \to [X,Y]$$

is the evaluation morphism for the internal hom $[X,Y]$.

Properties

Syntax and semantics

In a cartesian closed category the evaluation map

$$[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 \to Y,\; x : X \; \vdash \; f(x) : Y$$

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

See also

• concrete category (for the external version)