nLab evaluation map

Context

Monoidal categories

monoidal categories

With traces

• trace

• traced monoidal category?

category theory

Contents

Definition

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

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

of the identity morphism

$\mathrm{Id}:\left[X,Y\right]\to \left[X,Y\right]$Id : [X,Y] \to [X,Y]

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

Properties

Syntax and semantics

In a cartesian closed category the evaluation map

$\left[X,Y\right]×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,\phantom{\rule{thickmathspace}{0ex}}x:X\phantom{\rule{thickmathspace}{0ex}}⊢\phantom{\rule{thickmathspace}{0ex}}f\left(x\right):Y$f : X \to Y,\; x : X \; \vdash \; f(x) : Y

expressing function application.

Revised on September 26, 2012 01:33:00 by Urs Schreiber (82.169.65.155)