Decidability in Intuitionistic Type Theory is functionally decidable

In this paper we show that the usual intuitionistic characterization of the decidability of the propositional function B(x) prop [x : A], i.e. to require that the predicate (For All x is an element of A)(B(x) V-B(x)) is provable, is equivalent, when working within the framework of Martin-Lof's Intuitionistic Type Theory, to require that there exists a decision function rho : A --> Boole such that (For All x is an element of A) ((rho(x) = (Boole) true) <----> B(x)). Since we will also show that the proposition x = (Boole) true [x : Boole] is decidable, we can alternatively say that the main result of this paper is a proof that the decidability of the predicate B(x)prop[x : A] can be effectively reduced by a function rho is an element of A --> Boole to the decidability of the predicate rho(x) = (Boole) true [x : A]. All the proofs are carried out within the Intuitionistic Type Theory and hence the decision function rho, together with a proof of its correctness, is effectively constructed as a function of the proof of (For All s is an element of A)(B(x)V - B(x)).