Apply - Universal Property

Universal Property

Consider a function, that is, where the bracket notation denotes the space of functions from A to B. By means of currying, there is a unique function . Then Apply provides the universal morphism

,

so that

or, equivalently one has the commuting diagram

The notation for the space of functions from A to B occurs more commonly in computer science. In category theory, however, is known as the exponential object, and is written as . There are other common notational differences as well; for example Apply is often called Eval, even though in computer science, these are not the same thing, with eval distinguished from Apply, as being the evaluation of the quoted string form of a function with its arguments, rather than the application of a function to some arguments.

Also, in category theory, curry is commonly denoted by, so that is written for curry(g). This notation is in conflict with the use of in lambda calculus, where lambda is used to denote free variables. With all of these notational changes accounted for, the adjointness of Apply and curry is then expressed in the commuting diagram

The articles on exponential object and Cartesian closed category provide a more precise discussion of the category-theoretic formulation of this idea. Thus use of lambda here is not accidental; Cartesian-closed categories provide the general, natural setting for lambda calculus.