[Agda] HOTT-style reals in Agda

[Jason Dagit]

On Mon, Jul 13, 2015 at 5:43 AM, 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?
>

I don't know if you already found these, but just in case you haven't seen
them:
  *
http://www.cs.swan.ac.uk/~csetzer/articlesFromOthers/chiMing/chiMingChuangExtractionOfProgramsForExactRealNumberComputation.pdf
  *
http://www.cs.nott.ac.uk/~nzl/Home_Page/Homepage_files/%5BNuo_Li%5D%5Bfinal_year%5DReport.pdf

Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150713/52f29e4d/attachment.html