[Agda] HOTT-style reals in Agda

[Joachim Breitner]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part
Url : http://lists.chalmers.se/pipermail/agda/attachments/20150713/01170976/attachment.bin