[Agda] decidable equality in algebra

[Bas Spitters]

We've developed a substantial library for constructive analysis in Coq.
Here's an list of related publications:
http://corn.cs.ru.nl/pub.html

Please let me know it you have any questions.

I agree with Martin, I would also like to UF for this. Perhaps cubical
agda will make this possible!
https://hott-uf.github.io/2017/abstracts/cubicalagda.pdf

Best,

Bas

On Thu, Oct 5, 2017 at 11:43 PM, Martin Escardo <m.escardo at cs.bham.ac.uk> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda