 For a more explicit example, consider the function + which carries any pair of natural numbers to their sum. We may denote this function by \(+_{((\sigma \sigma)\sigma)}\), where \(\sigma\) is the type of natural numbers. Given any number x, \([+_{((\sigma \sigma)\sigma)}x]\) is the function which, when applied to any number y, gives the value \([[+_{((\sigma \sigma)\sigma)}x]y]\), which is ordinarily abbreviated as \(x + y\). Thus \([+_{((\sigma \sigma)\sigma)}x]\) is the function of one argument which adds x to any number. When we think of \(+_{((\sigma \sigma)\sigma)}\) as a function of one argument, we see that it maps any number x to the function \([+_{((\sigma \sigma)\sigma)}x]\).