search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
447 stars 136 forks source link

Move Rationals around #1027

Closed timorl closed 1 year ago

timorl commented 1 year ago

Now they are in Data and structured more like the various integers. In particular, QuoQ is now "the preferred version of the rationals in the library" – I picked it since it was the only one used in other places.

This is intended to be part of #404 – if this gets accepted then the only remaining work there will be proving the equivalence of HITQ and QuoQ. I'm already working on that, the main hurdle being that they are defined using different integers, so I first want to prove that arithmetic operations on the integers are equal.

timorl commented 1 year ago

Hm, can I request a review here, say from @ecavallo ?

felixwellen commented 1 year ago

Don't know if anyone is working right now (I am also on vacation). I am back next week and might have time for reviewing (don't know what yet).

mortberg commented 1 year ago

This seems reasonable to me. What do you think @felixwellen @ecavallo ?

felixwellen commented 1 year ago

Looks good to me!