[Agda] HOTT-style reals in Agda

[Bas Spitters]

Great! When did you do this?

On Mon, Jul 13, 2015 at 3:51 PM, Thorsten Altenkirch
<Thorsten.Altenkirch at nottingham.ac.uk> wrote:
> 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.
>