This repo is home to the undergraduate honours project of Zach Murray at Dalhousie University and its extensions by other contributors.
The goal of the project was to implement as much of Errett Bishop's constructive analysis in the Agda proof assistant as possible.
The undergraduate thesis on this project is available on the arXiv at https://arxiv.org/abs/2205.08354.
The version of the repository described in the thesis is at commit 5cd6d3d: https://github.com/z-murray/honours-project-constructive-analysis-in-agda/commit/5cd6d3d023279518213f3e58879bfc867bb2503c.
Bishop's constructive analysis is described in the following reference: E. Bishop and D. S. Bridges, Constructive Analysis. Comprehensive Studies in Mathematics, vol. 279. Springer, 1985
If you would like to submit any changes, please feel free to make a pull request and it will be reviewed.
Thank you to the following contributors for your additional work!
- Viktor Csimma