A continuation of Zachary Murray's previous work, getting until the definition of continuity.
Check out the agda2hs branch! It's a rewrite which makes the first half of the library compatible with agda2hs, and thus runnable to some extent.
The rewrite is done up until the definition of e.
Actually, it demonstrates that Bishop reals are not suitable for more complex exact-real aritmetic, because of the ineffectiveness of rational operations. See investigation/investigation.txt there.