[Agda] HOTT-style reals in Agda

[Thorsten Altenkirch]

On 13/07/2015 14:08, "Bas Spitters" <b.a.w.spitters at gmail.com> wrote:

>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.)

I guess you mean the partiality monad.

Nils Anders Danielsson and I came up with a formalisation (in Agda)

http://www.cse.chalmers.se/~nad/listings/equality/Partiality-monad.Inductiv
e.html

which tackles the problem that you want ³Partial A² be a wDCPO, i.e.
Closed under the lubs of increasing omega-chains. This seems impossible to
show for the naïve definition which is also the source of the problem
reported by Chapman, Uustalu and Veltri at the Types meeting.

The fix is basically the same as for the reals, you inductively define
Partial A to be given by now A, never, and a constructor lub for
increasing chains. You mutually define the order and decree that the
constructor of the chains is actually the lub. The equality is just the
symmetric closure of the order but it is important that it is defined at
the same time.

For this definition it is possible to show that it is a monad without
using choice. 

Cheers,
Thorsten

>
>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
>>
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.