cubical
cubical copied to clipboard
agda
The type of reals
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.
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?)
(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.
@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.
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.
@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.
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! :)
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.
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.
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
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.