nLab
evaluation map

Context

Monoidal categories

Category theory

Contents

Definition

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

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

of the identity morphism

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

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

Properties

Syntax and semantics

In a cartesian closed category the evaluation map

[X,Y]×XevalY [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:XY,x:Xf(x):Y 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.

Revised on January 26, 2014 07:08:26 by Urs Schreiber (89.204.138.15)