Constructing fixed points and economic equilibria

Constructive mathematics is mathematics with intuitionistic logic (together with some appropriate, predicative, foundation)-it is often crudely characterised as mathematics without the law of excluded middle.
The intuitionistic interpretation of the connectives and quantifiers ensure that constructive proofs contain an inherent algorithm which realises the computational content of the result it proves, and, in contrast to results from computable mathematics, these inherent algorithms
come with fixed rates of convergence.
The value of a constructive proof lies in the vast array of models for constructive mathematics. Realizability models and the interpretation of constructive ZF set theory into Martin Löf type theory allows one to view constructive mathematics as a high level programing language, and programs have been extracted and implemented from constructive proofs. Other models, including topological forcing models, of constructive set theory can be used to prove metamathematical results, for example, guaranteeing the (local) continuity of functions or algorithms.
In this thesis we have highlighted any use of choice principles, and those results which do not require any choice, in particular, are valid in any topos.
This thesis looks at what can and cannot be done in the study of the fundamental fixed point theorems from analysis, and gives some applications to mathematical economics where value is given to computability.