[Agda] HOTT-style reals in Agda

[Bas Spitters]

It would be a very good project. The formalization of the cumulative
universe is another complicated HIT.
The formalization in Coq showed that the induction principle in the
book was not quite correct.
http://homotopytypetheory.org/2014/09/11/the-cumulative-hierarchy-of-sets-guest-post-by-jeremy-ledent/

(This was another ENS internship project)

It would be nice to have the Cauchy reals verified. It is certainly not trivial.

On Mon, Jul 13, 2015 at 8:05 PM, Jason Dagit <dagitj at gmail.com> wrote:
>
>
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>