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