nLab
evaluation map

Definition

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

$$\mathrm{ev}:[X,Y]\otimes X\to Y$$ev : [X,Y]\otimes X \to Y

of the identity morphism

$$\mathrm{Id}:[X,Y]\to [X,Y]$$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{\mathrm{eval}}{\to }Y$$[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⊢f(x):Y$$f : X \to Y,\; x : X \; \vdash \; f(x) : Y

expressing function application.