[Agda] HOTT-style reals in Agda

[Bas Spitters]

It should be possible using the same methods as the ones in the
formalization of the surreals in Coq:
https://github.com/HoTT/HoTT/blob/babaf2181a75f6ebb8b4a947baff686c8cdb09e1/theories/Spaces/No.v

In fact, since agda has induction recursion it should in fact be a bit easier.

An easier project would be to use the same methodology to formalize
the delay monad in HoTT. (Tarmo, Bob and Andreas may already be
working on this.)

In 2013, I had an intern from ENS Lyon (Gaetan Gilbert) to work on the
Cauchy reals. He made a lot of progress. We tried to fake IndInd in
Coq, but by the time we really got there the internship was over.
Still a lot was already done:
https://github.com/SkySkimmer/HoTT-algebra

I'd like to complete the project using the ideas by Mike Shulman, but
I don't know when I find the time for this.

Best,

Bas

On Mon, Jul 13, 2015 at 2:43 PM, Joachim Breitner <breitner at kit.edu> wrote:
> Hi list,
>
> I was looking at the definition of reals via Cauchy sequences in the
> HOTT book, and I wonder how tricky it would be to implement that within
> the hott-agda library.
>
> Given that it has not been done before (as far as I can tell) – is that
> because it is obvious and trivial, or because it is known how to do it,
> and just tedious, or is it because it is expected to be challenging?
>
> Thanks,
> Joachim
>
> --
> Dipl.-Math. Dipl.-Inform. Joachim Breitner
> Wissenschaftlicher Mitarbeiter
> http://pp.ipd.kit.edu/~breitner
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>