The Clowder Project

Throughout this work, we will sometimes denote a function $f\colon X\to Y$ by

1. 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. 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:

   1. (a)

      Square brackets $[x\mapsto f(x)]$;

   2. (b)

      Parentheses $(x\mapsto f(x))$;

   hoping to improve readability when dealing with e.g.:

   1. (a)

      Equivalence classes, cf.:

      1. (i)

         $[\mspace {-3mu}[[x]\mapsto f([x])]\mspace {-3mu}]$

      2. (ii)

         $[[x]\mapsto f([x])]$

      3. (iii)

         $(\lambda [x].\ f([x]))$

   2. (b)

      Function evaluations, cf.:

      1. (i)

         $\Phi ([\mspace {-3mu}[x\mapsto f(x)]\mspace {-3mu}])$

      2. (ii)

         $\Phi ((x\mapsto f(x)))$

      3. (iii)

         $\Phi ((\lambda x.\ f(x)))$

3. 3.

   We will also sometimes write $-$, $-_{1}$, $-_{2}$, etc. for the arguments of a function. Some examples include:

   1. (a)

      Writing $f(-_{1})$ for a function $f\colon A\to B$.

   2. (b)

      Writing $f(-_{1},-_{2})$ for a function $f\colon A\times B\to C$.

   3. (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}]$.

   4. (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})$.

4. 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$.

For an example of the above notations being used in practice, see the proof of the adjunction