We are interested in exact real numbers, as opposed to floating point numbers. The final goal is to develop the basics of real analysis in such a way that from a proof of an existence formula one can extract a program. For instance, from a proof of the intermediate value theorem we want to extract a program that, given an arbitrary error bound 2^-k, computes a rational a where the given function is zero up to the error bound. - The novel aspect of the present work is the development of elementary constructive analysis in such a way that witnesses have as low a type level as possible. This clearly is important for the complexity of extracted programs.