evaluation map


Monoidal categories

Category theory



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].


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.

Last revised on January 26, 2014 at 07:08:26. See the history of this page for a list of all contributions to it.