The Clowder Project

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

1. For example, given a function
   \[ \Phi \colon \textup{Hom}_{\mathsf{Sets}}\webleft (X,Y\webright )\to K \]

   taking values on a set of functions such as $\textup{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:

   1. Square brackets $\webleft [x\mapsto f\webleft (x\webright )\webright ]$;
   2. Parentheses $\webleft (x\mapsto f\webleft (x\webright )\webright )$;

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

   1. Equivalence classes, cf.:
      1. $[\mspace {-3mu}[\webleft [x\webright ]\mapsto f\webleft (\webleft [x\webright ]\webright )]\mspace {-3mu}]$
      2. $\webleft [\webleft [x\webright ]\mapsto f\webleft (\webleft [x\webright ]\webright )\webright ]$
      3. $\webleft (\lambda \webleft [x\webright ].\ f\webleft (\webleft [x\webright ]\webright )\webright )$
   2. Function evaluations, cf.:
      1. $\Phi \webleft ([\mspace {-3mu}[x\mapsto f\webleft (x\webright )]\mspace {-3mu}]\webright )$
      2. $\Phi \webleft (\webleft (x\mapsto f\webleft (x\webright )\webright )\webright )$
      3. $\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:
   1. Writing $f\webleft (-_{1}\webright )$ for a function $f\colon A\to B$.
   2. Writing $f\webleft (-_{1},-_{2}\webright )$ for a function $f\colon A\times B\to C$.
   3. 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}]$.

   4. Denoting a composition of the form
      \[ A\times B\overset {\phi \times \text{id}_{B}}{\to }A'\times B\overset {f}{\to }C \]

      by $f\webleft (\phi \webleft (-_{1}\webright ),-_{2}\webright )$.

4. Finally, given a function $f\colon A\to B$, we 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$.

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