ℚ is a Field

[kangrongji]

This PR shows ℚ is a field, using the QuoQ in library. The codes are basically copied from my own repo. I've always thought to move these codes to cubical library and it's time for ℚ.

[felixwellen]

Thanks for the contribution! It is great to finally have the field of rationals...

[kangrongji]

If I am trying to apply solver to an explicit CommRing, for example:

f : ...
f = ...
  where
  helper : (x y : ℚCommRing .fst) → (x · y) · 1r ≡ 1r · (y · x)
  helper = solve ℚCommRing

It will cause errors. You can try it. So I have to pack up them in a module with abstract CommRing as parameter, then open it when needed.

[felixwellen]

If I am trying to apply solver to an explicit CommRing, for example:

f : ...
f = ...
  where
  helper : (x y : ℚCommRing .fst) → (x · y) · 1r ≡ 1r · (y · x)
  helper = solve ℚCommRing

It will cause errors. You can try it. So I have to pack up them in a module with abstract CommRing as parameter, then open it when needed.

Ah, yes - I know why, but that takes time to fix.

[kangrongji]

If I am trying to apply solver to an explicit CommRing, for example:

f : ...
f = ...
  where
  helper : (x y : ℚCommRing .fst) → (x · y) · 1r ≡ 1r · (y · x)
  helper = solve ℚCommRing

It will cause errors. You can try it. So I have to pack up them in a module with abstract CommRing as parameter, then open it when needed.

Ah, yes - I know why, but that takes time to fix.

Thanks! Please remember to @ me if you make it work.

[felixwellen]

I'll do my best...