[Agda] decidable equality in algebra

[Martin Escardo]

Too many typos, sorry. Here we go again more carefully.


There is a huge literature on constructive analysis. You may wish to 
start with Bishop's Foundations 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


On 05/10/17 22:43, Martin Escardo wrote:
> 
> 
> 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

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe