# nLab evaluation map

Contents

### Context

#### Monoidal categories

monoidal categories

With braiding

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

#### Mapping space

internal hom/mapping space

# Contents

## Definition

Let $\big(\mathcal{C}, \otimes, \mathbb{1}\big)$ be a closed monoidal category. For $S, D \in C$ two objects, with internal hom $[S, \text{-}]$ right adjoint to the tensor product $S \otimes (\text{-})$, the evaluation map

$ev \;\colon\; S \otimes [S, D] \to D$

is the counit of this adjunction, hence the adjunct of the identity morphism

$Id \;\colon\; [S,D] \to [S,D] \,.$

Concretely for $\mathcal{C}$ = Sets or generally on generalized elements, the evaluation map is given by evaluating a function at a value, whence the name:

$\array{ S \times [S,D] &\overset{ev}{\longrightarrow}& D \\ \big( s ,\, f \big) &\mapsto& f(s) \mathrlap{\,.} }$

If $\mathcal{C}$ is moreover compact then for $D = \mathbb{1}$ the tensor unit we have that $[S, \mathbb{1}] \,=\, S^\ast$ is the dual object to $S$, whence the evaluation map becomes the pairing of objects with their duals

$S \otimes S^\ast \overset{ev}{\longrightarrow} \mathbb{1} \,.$

Therefore, sometimes the pairing map on dual objects may be called “evaluation” even when the ambient category is not compact closed.

## 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 \colon X \to Y ,\; x \colon X \; \vdash \; f(x) \colon Y$

expressing function application. On propositions ((-1)-truncated types) this is the modus ponens deduction rule.