Normalised Q plus related

[reswatson]

A normalised rational Q (Base.agda), along with related additions to other numerical Data.

[anshwad10]

What's the difference between this and Cubical.Data.Rationals.MoreRationals.SigmaQ?

[reswatson]

Here the non-experimental well-developed standard 'Int' is used, rather than the under-developed and novel 'QuoInt'. The amount of library code available for Int forces this choice. Further, 'Int' is the standard for Cubical Agda and should be used in preference anyway.

[reswatson]

@anshwad10: Any suggestions or corrections? I'm thinking for example (i) that maybe 'useful lemmas' should be put in its own file and (ii) that converse and contraposition will either have to be left where they are for now or inlined, but I notice you are working on a library for classical logic - logical relations of any sort should perhaps be put in a 'logic' library.

@ALL: Also are there any organisational changes suggested, for example splitting Base into smaller parts? Personally I wouldn't like this as these are mostly minimal essentials that a Properties or an Order might use, but it may be a requested change.