-Abstraction is the process of interpreting a formula for a function (or operation) as defining an actual function.
Often we make the presence of the free variable explicit in the notation, saying that is a term of type ; then
a term of the dependent product . Or if is a term of the constant type , then the same expression is a term of the function type .
Although developed for type theory and commonly used in computer science, -abstraction makes sense in ordinary mathematics usually based on set theory. If the types and are interpreted as sets and we define functions as certain subsets of cartesian products, then the notation (2) refers to
(at least in the simple case where is constant).