A function is a functional and total relation.
-
1.
For example, given a function
\[ \Phi \colon \operatorname {\mathrm{Hom}}_{\mathsf{Sets}}(X,Y)\to K \]taking values on a set of functions such as $\operatorname {\mathrm{Hom}}_{\mathsf{Sets}}(X,Y)$, we will sometimes also write
\[ \Phi (f)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi ([\mspace {-3mu}[x\mapsto f(x)]\mspace {-3mu}]). \] -
2.
This notational choice is based on the lambda notation
\[ f\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(\lambda x.\ f(x)), \]but uses a “$\mathord {\mapsto }$” symbol for better spacing and double brackets instead of either:
hoping to improve readability when dealing with e.g.:
-
(a)
Equivalence classes, cf.:
-
(b)
Function evaluations, cf.:
-
3.
We will also sometimes write $-$, $-_{1}$, $-_{2}$, etc. for the arguments of a function. Some examples include:
-
(a)
Writing $f(-_{1})$ for a function $f\colon A\to B$.
-
(b)
Writing $f(-_{1},-_{2})$ for a function $f\colon A\times B\to C$.
-
(c)
Given a function $f\colon A\times B\to C$, writing
\[ f(a,-)\colon B\to C \]for the function $[\mspace {-3mu}[b\mapsto f(a,b)]\mspace {-3mu}]$.
-
(d)
Denoting a composition of the form
\[ A\times B\overset {\phi \times \operatorname {\mathrm{id}}_{B}}{\to }A'\times B\overset {f}{\to }C \]by $f(\phi (-_{1}),-_{2})$.
-
(a)
-
4.
Finally, given a function $f\colon A\to B$, we will sometimes write
\[ \mathrm{ev}_{a}(f)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f(a) \]for the value of $f$ at some $a\in A$.
3.1.1 Functions
Throughout this work, we will sometimes denote a function $f\colon X\to Y$ by
\[ f\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[\mspace {-3mu}[x\mapsto f(x)]\mspace {-3mu}]. \]
For an example of the above notations being used in practice, see the proof of the adjunction
