 Myhill crucially observes that power set is not needed for constructive  mathematics Bishop-style, as it can be replaced by one of its consequences. This is often called Myhill’s exponentiation axiom and states that we can form a set of all functions from one given set to another. This axiom is clearly equivalent to power set in a classical context, where subsets of a given set may be represented by characteristic functions. In the absence of the principle of excluded middle, however, power set and exponentiation are not equivalent. Myhill’s fundamental observation is that exponentiation suffices to carry out  the mathematics of (Bishop 1967); for example, it allows for  the construction of the (Cauchy) real numbers within constructive set theory.  Myhill claims that exponentiation is constructively meaningful because a function is a rule,  a finite object which can actually be given.