Contents

# Contents

## Idea

(…)

### Value of a function

In set theory, the value of a function $f \,\colon\, X \longrightarrow A$ at an element $x \in X$ is the element $f(x) \in A$.

More generally, in type theory the value of a function on a term $x$ of type $X$ is the term $f(x)$ of type $A$.

(…)

## Properties

### Relation to images

The image of a function $f \,\colon\, X \to A$ on a subset $S \subset X$ is the value at $S$ of the function $f_\ast \;\colon\; P(X) \to P(A)$, which in turn is the value at $f$ of the covariant power set functor $P \,\colon\, Set \to Set$ on the category Set of sets.