Small refactorings for real numbers

UniMath / agda-unimath

The agda-unimath library

https://unimath.github.io/agda-unimath/

MIT License

222 stars 71 forks source link

Open fredrik-bakke opened 8 months ago

fredrik-bakke commented 8 months ago

[ ] Factor out lower and upper Dedekind cuts into their own files.
[ ] lower and upper Dedekind reals should probably be their own files too.
[ ] Use the theory of lower and upper sets of posets in the definition of Dedekind cuts.