This repository contains code that is developing towards a constructive library of Dedekind Reals.
The files are built on top of TypeTopology library, with a view towards integration when the code is cleaned up and finished.
A list of the files that I have developed as part of this project can be found in AgdaCode/AndrewIndex.lagda