1.1.1 Functions

A function is a functional and total relation.

Throughout this work, we will sometimes denote a function f:XY by

f=def[[xf(x)]].

  1. 1. For example, given a function
    Φ:HomSets(X,Y)K

    taking values on a set of functions such as HomSets(X,Y), we will sometimes also write

    Φ(f)=defΦ([[xf(x)]]).
  2. 2. This notational choice is based on the lambda notation
    f=def(λx. f(x)),

    but uses a “” symbol for better spacing and double brackets instead of either:

    1. (a) Square brackets [xf(x)];
    2. (b) Parentheses (xf(x));

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

    1. (c) Equivalence classes, cf.:
      1. (i) [[[x]f([x])]]
      2. (ii) [[x]f([x])]
      3. (iii) (λ[x]. f([x]))
    2. (d) Function evaluations, cf.:
      1. (i) Φ([[xf(x)]])
      2. (ii) Φ((xf(x)))
      3. (iii) Φ((λ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:AB.
    2. (b) Writing f(1,2) for a function f:A×BC.
    3. (c) Given a function f:A×BC, writing
      f(a,):BC

      for the function [[bf(a,b)]].

    4. (d) Denoting a composition of the form
      A×Bϕ×idBA×BfC

      by f(ϕ(1),2).

  4. 4. Finally, given a function f:AB, we write
    eva(f)=deff(a)

    for the value of f at some aA.

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

stated in Chapter 2: Constructions With Sets, Item 2 of Proposition 2.1.3.1.3.


Noticed something off, or have any comments? Feel free to reach out!


You can also use the contact form below: