nLab evaluation map

Contents

Context

Monoidal categories

monoidal categories

With symmetry

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products

Semisimplicity

Morphisms

Internal monoids

Examples

Theorems

In higher category theory

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.

See also

Last revised on May 18, 2022 at 06:42:27. See the history of this page for a list of all contributions to it.