The type of reals

[ayberkt]

I have been looking for a definition of ℝ around here but I haven't been able to find one.

Is there a particular reason that this is the case? Otherwise, I can do this and send a PR.

[Saizan]

No particular reason as far as I understand, a PR would be great!

[UlrikBuchholtz]

Which definition are you planning to use? Probably, some kind of Dedekind reals are a good start, but perhaps parametrized by an arbitrary σ-frame, as suggested in Sec. 11.2 of the HoTT book. Then it can be instantiated with either Prop or the initial σ-frame.

It could also be a good idea to axiomatize the notion of a Caucy-complete Archimedean ordered field, as in Auke Booij's thesis, and show that Dedekind reals are an instance. The HoTT reals are then another instance. (Can cubical Agda handle the HoTT reals as a HIIT yet?)

[Saizan]

(Can cubical Agda handle the HoTT reals as a HIIT yet?)+

I would suggest to start experimenting with them, transp won't compute yet but should be very soon and I could use some examples to test it on.

[ayberkt]

@UlrikBuchholtz thanks for the suggestions.

Which definition are you planning to use? Probably, some kind of Dedekind reals are a good start, but perhaps parametrized by an arbitrary σ-frame, as suggested in Sec. 11.2 of the HoTT book. Then it can be instantiated with either Prop or the initial σ-frame.

Yes, I was planning to follow Sec. 11.2 (option (iv) for Ω) of the book as you suggested. I was planning to use the initial σ-frame instead of parametrising, but it might be better to parametrise. By the way, I have some stuff on frames and their nuclei here: https://ayberkt.gitlab.io/msc-thesis/Frame.html#936. Uses the SNS from this library (an older version).

It could also be a good idea to axiomatize the notion of a Caucy-complete Archimedean ordered field, as in Auke Booij's thesis, and show that Dedekind reals are an instance. The HoTT reals are then another instance. (Can cubical Agda handle the HoTT reals as a HIIT yet?)

Sounds like a good idea. I need to look at the thesis.

Also related: I have been working on formalising formal topologies in Cubical Agda, and it might be an interesting experiment to define reals as the formal points of the formal topology of the reals (as in Inductively generated formal topologies Sec. 4.2) in addition to a direct definition.

[ayberkt]

I guess #116 is a dependency (operations on rationals).

[m-yac]

I would also love to see such a PR! I got started on this a while ago, but don't have time to finish it up right now. I made a gist with most of the progress I made, but won't be making a PR anytime soon: https://gist.github.com/m-yac/7d3fd934852fb321446d0c2322f99481

By the way, I have some stuff on frames and their nuclei here: https://ayberkt.gitlab.io/msc-thesis/Frame.html#936. Uses the SNS from this library (an older version).

If we end up adding a HIT for the initial σ-frame, I think this code would be great to have as well.

Also related: I have been working on formalising formal topologies in Cubical Agda, and it might be an interesting experiment to define reals as the formal points of the formal topology of the reals (as in Inductively generated formal topologies Sec. 4.2) in addition to a direct definition.

This sounds awesome! Personally, I am always interested in seeing multiple equivalent definitions of things.

[ayberkt]

@m-yac

I would also love to see such a PR! I got started on this a while ago, but don't have time to finish it up right now. I made a gist with most of the progress I made, but won't be making a PR anytime soon: https://gist.github.com/m-yac/7d3fd934852fb321446d0c2322f99481

Thanks, this is really useful! I didn't look at everything very carefully, but it seems that you were almost done. Did you end up encountering a particular problem that prevented you from completing?

If we end up adding a HIT for the initial σ-frame, I think this code would be great to have as well.

Where would be an appropriate place for the general definition of frame? I can perhaps prove the initiality of the initial frame.

[m-yac]

Thanks, this is really useful! I didn't look at everything very carefully, but it seems that you were almost done. Did you end up encountering a particular problem that prevented you from completing?

Just time! Also, it's easy to get a definition wrong without proving some things about it, so I would want to prove some things first before considering things done. In fact I think the definition I gave in the gist is wrong – based on what's in the HoTT book the dedekind cuts over A should use a ℚ-frame not an A-frame, I believe this would've come up when proving Cuts ℝ ≃ ℝ.

Where would be an appropriate place for the general definition of frame? I can perhaps prove the initiality of the initial frame.

Structures.Frame, and that would be awesome! Looks like you're already working on it! :)

[ayberkt]

@mchristianl I'm just curious, how is your progress on this issue going?

[mchristianl]

Hi @ayberkt,

The latest progress that I made was in proving Cubical.HITs.Rationals.QuoQ to be an instance of a LinearlyOrderedField in Number.Instances.QuoQ. This is just a preparation for a definition of cauchy-completeness which is given in terms of some rational numbers from @abooij 's thesis.

The used definitions were my own ones and I have talked to @mortberg at the Agda Implementors meeting a few weeks ago about how these Ideas could end up in the cubical standard library. @mortberg would be happy to #404 Reorganize files and prove equivalences of the many types of integers and rationals w.r.t. the standard identity principle that is embraced in the cubical standard library and I have tried my hand at it.

So in summary, I guess that #404 is blocking this issue.

I took a week off and had some other work to do, but I would be happy to resume working on this topic these days.

[mchristianl]

To clarify: I would like to obtain an Agda definition of cauchy-complete archimedean field. Adding various constructions of real numbers is unfortunately not my area of expertise.

[mortberg]

Hi @ayberkt,

The latest progress that I made was in proving Cubical.HITs.Rationals.QuoQ to be an instance of a LinearlyOrderedField in Number.Instances.QuoQ. This is just a preparation for a definition of cauchy-completeness which is given in terms of some rational numbers from @abooij 's thesis.

The used definitions were my own ones and I have talked to @mortberg at the Agda Implementors meeting a few weeks ago about how these Ideas could end up in the cubical standard library. @mortberg would be happy to #404 Reorganize files and prove equivalences of the many types of integers and rationals w.r.t. the standard identity principle that is embraced in the cubical standard library and I have tried my hand at it.

So in summary, I guess that #404 is blocking this issue.

I took a week off and had some other work to do, but I would be happy to resume working on this topic these days.

Sorry I've been so slow with reviewing this... I've been very busy lately. This week I'm also swamped, but next week things will be back to normal and I'll look at all the open PRs. Just so you know, you can open PRs based on other PRs. So if #404 is blocking just open whatever PRs you want that are relying on #404

[mchristianl]

Sorry I've been so slow with reviewing this...

That's not an issue at all!

So if #404 is blocking just open whatever PRs you want that are relying on #404

Ok. I'll start continuing this way adding a few more properties for QuoQ.

[ayberkt]

Thanks for the response @mchristianl!

[UrsSchreiber]

Hi,

just found this old thread by looking for implementations of real numbers in (cubical) Agda.

I see there is:

Zachary Murray:
"Constructive Analysis in the Agda Proof Assistant"
arxiv.org/abs/2205.08354

but maybe that's not readily adapted to cubical(?)

Is there any other (upcoming) work along these lines?

[LuuBluum]

I can't say that I'm necessarily planning on approaching an implementation of the reals from that direction (rather, the HoTT book manages both an implementation of the Dedekind reals and the Cauchy reals, though proving their equivalence would require LEM), though my PR on various forms of order #969 is so that a future PR has an easier time defining concepts such as a complete Archimedean field and, eventually, the reals.

[UrsSchreiber]

Thanks for the reply!

I would, a priori, be interested in having available any implementation of the reals in cubical Agda (as it's not clear to me yet which version will be best in real-world application).

Concretely, we need the reals in cubical Agda for a topological quantum simulator project at nyuad/cqts --- but I imagine there will be a plethora of other applications.

If you know of anyone who could be incentivized to look into this based on the code you already have, I would be grateful if you could drop me a note.

[LuuBluum]

I can take a look at trying an implementation. I was hoping to get to it down the line anyway, so might as well start now. No promises as to when it'll be ready, though.

Notably, it seems we don't even have a defined order over rationals (let alone that they form an ordered field; we merely have that they're a field), so there's a lot of work to be done.

[UrsSchreiber]

Thanks for the reply, that sounds great.

You know, I sense that some people here at out research center would be eager to hear you present already the code on "Cardinality and Order" which you already have.

I know it's short notice, but might you be available to speak in our seminar, end of this month (as we happen to have a free slot on Feb 27)? Just drop me an email (here), if you like.

[LuuBluum]

Unfortunately I would not be available at that time; I appreciate the offer though. That PR for the most part is just definitions derived from nLab or the HoTT book; there's still a ton of work to be done to fully flesh out all the details and make use of them.

[UrsSchreiber]

Just to say that yesterday we had Zach Murray speaking about his real numbers Agda library here (video)