nLab evaluation map

Contents

Context

Monoidal categories

monoidal categories

category theory

Contents

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.

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