[Agda] decidable equality in algebra

[Martin Escardo]

On 05/10/17 19:58, mechvel at botik.ru wrote:

> I wonder of how many nice algorithms are known for real numbers, whether
> they are interesting so that it could be worthy to lift the ≟
> requirement.

There is a huge literature on constructive analysis. You may with to 
start with Bishop's Founctions of Constructive Analysis, and Bishop and 
Bridges' Constructive Analysis.

Bishop works with setoids, and in particular with a setoid of real 
numbers along the lines you describe in your message.


Fred Richman has many interesting papers on constructive analysis, most 
of them available on his web page. But he doesn't work with setoids. If 
I were to try to formalize his work, I would use univalent type theory 
rather than setoids.

As I said, many authors have worked on this vast subject.

Best,
Martin