Reorganize files and prove equivalences of the many types of integers and rationals

[mortberg]

The library contains a lot of different representations of the integers:

• https://github.com/agda/cubical/tree/master/Cubical/HITs/Ints
• https://github.com/agda/cubical/tree/master/Cubical/Data/DiffInt
• https://github.com/agda/cubical/tree/master/Cubical/Data/Int
• https://github.com/agda/cubical/blob/master/Cubical/HITs/S1/Base.agda#L40

and the rationals:

• https://github.com/agda/cubical/tree/master/Cubical/HITs/Rationals

It would be good to collect these in one place, maybe in a folder in Cubical.Algebra? No matter what the Data/HITs distinction doesn't really make sense. This reorganization should be done in a separate PR.

Once the files are in the same place we should have proofs that all of the different representations are equivalent. This might be easier for some representations than others, but once https://github.com/agda/cubical/pull/400 is done we will then be able to transport the proof that the integers form a commutative ring to all of the other representations using the SIP. Doing one or more of these equivalences would be a good first PR for someone trying to learn Cubical Agda.

[mortberg]

These issues are related:

• https://github.com/agda/cubical/issues/116
• https://github.com/agda/cubical/issues/126
• https://github.com/agda/cubical/issues/150

It might be possible to close some of them.

[mortberg]

@mchristianl I don't know why, but I can't assign you to this issue...

[mchristianl]

That's strange. I got the notification email, so this should be the correct identifier at least

[mchristianl]

About the boolean-valuedness of decidable orders _<_: we do already have a type-valued order on ℕ:

https://github.com/agda/cubical/blob/367dd3d4cf185693f02aac3deef93888dedc7eeb/Cubical/Data/Nat/Order.agda#L22-L26

and it is also defined likewise (as a relation) in the non-cubical standard library

data _≤_ : Rel ℕ 0ℓ where
  z≤n : ∀ {n}                 → zero  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

_<_ : Rel ℕ 0ℓ
m < n = suc m ≤ n

Which approach should we follow?

[knrafto]

A point in favor of the first definition is that it works nicely for ints as well:

_≤_ : ℤ → ℤ → Type₀ 
m ≤ n = Σ[ k ∈ ℕ ] pos k + m ≡ n

[mortberg]

The question about boolean or non-boolean orders is orthogonal to this issue... But I personally like boolean tests that then get lifted to types using boolean reflection à la SSReflect. I don't know why other Agda libraries tend to not do this?

Btw, Egbert had a tweet about using boolean reflection for primality testing in Agda recently which illustrates why this technique is so powerful: https://twitter.com/EgbertRijke/status/1309072950797185033

[knrafto]

I personally think of decidability as a "property" of a definition, rather than a definition itself. So I would rather define the order as proposition, and then prove that it's decidable, rather than take a boolean-valued function as a definition. And then you can use the technique that Egbert shows on this decidability proof

[xekoukou]

To transport the structure of CommRIng from one Int into the other, one needs to reorganize the CommRingStr, split the raw structure from the Propositions : https://github.com/agda/cubical/pull/552

I will give it a try.