Rational order (#1071)

* Adjust Rationals to use Int instead of QuoInt

* Define ordering over rationals and basic properties

* More properties of rational order

* Clean up definition of order; define trichotomy

* Add multiplication cancelling to rationals

* Fix whitespace

* Remove unnecessary 0<1 proof

* Redefine rec2 with pattern matching

Cubical/Algebra/CommRing/Instances/Int.agda

@@ -22,4 +22,4 @@ isCommRing (snd ℤCommRing) = isCommRingℤ
     isCommRingℤ : IsCommRing 0 1 _+ℤ_ _·ℤ_ -ℤ_
     isCommRingℤ = makeIsCommRing isSetℤ Int.+Assoc (λ _ → refl)
                                  -Cancel Int.+Comm Int.·Assoc
-                                 Int.·Rid ·DistR+ Int.·Comm
+                                 Int.·IdR ·DistR+ Int.·Comm

Cubical/Algebra/CommRing/Instances/Rationals.agda

@@ -9,7 +9,7 @@ module Cubical.Algebra.CommRing.Instances.Rationals where
 open import Cubical.Foundations.Prelude
 
 open import Cubical.Algebra.CommRing
-open import Cubical.Data.Rationals
+open import Cubical.Data.Rationals.MoreRationals.QuoQ
   renaming (ℚ to ℚType ; _+_ to _+ℚ_; _·_ to _·ℚ_; -_ to -ℚ_)
 
 open CommRingStr

Cubical/Algebra/Field/Instances/Rationals.agda

@@ -19,7 +19,7 @@ open import Cubical.Data.Int.MoreInts.QuoInt
            ; ·-zeroˡ to ·ℤ-zeroˡ
            ; ·-identityʳ to ·ℤ-identityʳ)
 open import Cubical.HITs.SetQuotients as SetQuot
-open import Cubical.Data.Rationals
+open import Cubical.Data.Rationals.MoreRationals.QuoQ
   using    (ℚ ; ℕ₊₁→ℤ ; isEquivRel∼)
 
 open import Cubical.Algebra.Field

Cubical/Algebra/Group/ZAction.agda

@@ -12,9 +12,9 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Powerset
 
 open import Cubical.Data.Sigma
-open import Cubical.Data.Int
+open import Cubical.Data.Int as ℤ
   renaming
-    (_·_ to _*_ ; _+_ to _+ℤ_ ; _-_ to _-ℤ_ ; pos·pos to pos·) hiding (·Assoc)
+    (_·_ to _*_ ; _+_ to _+ℤ_ ; _-_ to _-ℤ_ ; pos·pos to pos·) hiding (·Assoc; ·IdL; ·IdR)
 open import Cubical.Data.Nat renaming (_·_ to _·ℕ_ ; _+_ to _+ℕ_)
 open import Cubical.Data.Nat.Mod
 open import Cubical.Data.Nat.Order
@@ -410,7 +410,7 @@ characℤ≅ℤ e =
     (λ p → inr (Σ≡Prop (λ _ → isPropIsGroupHom _ _)
                   (Σ≡Prop (λ _ → isPropIsEquiv _)
                     (funExt λ x →
-                      cong (fst (fst e)) (sym (·Rid x))
+                      cong (fst (fst e)) (sym (ℤ.·IdR x))
                       ∙ GroupHomℤ→ℤPres· ((fst (fst e)) , (snd e)) x 1
                       ∙ cong (x *_) p
                       ∙ ·Comm x -1 ))))

Cubical/Data/Rationals/Base.agda

@@ -3,11 +3,12 @@ module Cubical.Data.Rationals.Base where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
 
 open import Cubical.Data.Nat as ℕ using (discreteℕ)
 open import Cubical.Data.NatPlusOne
 open import Cubical.Data.Sigma
-open import Cubical.Data.Int.MoreInts.QuoInt
+open import Cubical.Data.Int
 
 open import Cubical.HITs.SetQuotients as SetQuotient
   using ([_]; eq/; discreteSetQuotients) renaming (_/_ to _//_) public
@@ -19,10 +20,6 @@ open BinaryRelation
 ℕ₊₁→ℤ : ℕ₊₁ → ℤ
 ℕ₊₁→ℤ n = pos (ℕ₊₁→ℕ n)
 
-private
-  ℕ₊₁→ℤ-hom : ∀ m n → ℕ₊₁→ℤ (m ·₊₁ n) ≡ ℕ₊₁→ℤ m · ℕ₊₁→ℤ n
-  ℕ₊₁→ℤ-hom _ _ = refl
-
 
 -- ℚ as a set quotient of ℤ × ℕ₊₁ (as in the HoTT book)
 
@@ -43,16 +40,16 @@ isSetℚ = SetQuotient.squash/
 isEquivRel∼ : isEquivRel _∼_
 isEquivRel.reflexive isEquivRel∼ (a , b) = refl
 isEquivRel.symmetric isEquivRel∼ (a , b) (c , d) = sym
-isEquivRel.transitive isEquivRel∼ (a , b) (c , d) (e , f) p q = ·-injʳ _ _ _ r
-  where r = (a · ℕ₊₁→ℤ f) · ℕ₊₁→ℤ d ≡[ i ]⟨ ·-comm a (ℕ₊₁→ℤ f) i · ℕ₊₁→ℤ d ⟩
-            (ℕ₊₁→ℤ f · a) · ℕ₊₁→ℤ d ≡⟨ sym (·-assoc (ℕ₊₁→ℤ f) a (ℕ₊₁→ℤ d)) ⟩
+isEquivRel.transitive isEquivRel∼ (a , b) (c , d) (e , f) p q = ·rCancel _ _ (e · pos (ℕ.suc (ℕ₊₁.n b))) r (ℕ.snotz ∘ injPos)
+  where r = (a · ℕ₊₁→ℤ f) · ℕ₊₁→ℤ d ≡[ i ]⟨ ·Comm a (ℕ₊₁→ℤ f) i · ℕ₊₁→ℤ d ⟩
+            (ℕ₊₁→ℤ f · a) · ℕ₊₁→ℤ d ≡⟨ sym (·Assoc (ℕ₊₁→ℤ f) a (ℕ₊₁→ℤ d)) ⟩
             ℕ₊₁→ℤ f · (a · ℕ₊₁→ℤ d) ≡[ i ]⟨ ℕ₊₁→ℤ f · p i ⟩
-            ℕ₊₁→ℤ f · (c · ℕ₊₁→ℤ b) ≡⟨ ·-assoc (ℕ₊₁→ℤ f) c (ℕ₊₁→ℤ b) ⟩
-            (ℕ₊₁→ℤ f · c) · ℕ₊₁→ℤ b ≡[ i ]⟨ ·-comm (ℕ₊₁→ℤ f) c i · ℕ₊₁→ℤ b ⟩
+            ℕ₊₁→ℤ f · (c · ℕ₊₁→ℤ b) ≡⟨ ·Assoc (ℕ₊₁→ℤ f) c (ℕ₊₁→ℤ b) ⟩
+            (ℕ₊₁→ℤ f · c) · ℕ₊₁→ℤ b ≡[ i ]⟨ ·Comm (ℕ₊₁→ℤ f) c i · ℕ₊₁→ℤ b ⟩
             (c · ℕ₊₁→ℤ f) · ℕ₊₁→ℤ b ≡[ i ]⟨ q i · ℕ₊₁→ℤ b ⟩
-            (e · ℕ₊₁→ℤ d) · ℕ₊₁→ℤ b ≡⟨ sym (·-assoc e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ⟩
-            e · (ℕ₊₁→ℤ d · ℕ₊₁→ℤ b) ≡[ i ]⟨ e · ·-comm (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b) i ⟩
-            e · (ℕ₊₁→ℤ b · ℕ₊₁→ℤ d) ≡⟨ ·-assoc e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) ⟩
+            (e · ℕ₊₁→ℤ d) · ℕ₊₁→ℤ b ≡⟨ sym (·Assoc e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ⟩
+            e · (ℕ₊₁→ℤ d · ℕ₊₁→ℤ b) ≡[ i ]⟨ e · ·Comm (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b) i ⟩
+            e · (ℕ₊₁→ℤ b · ℕ₊₁→ℤ d) ≡⟨ ·Assoc e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) ⟩
             (e · ℕ₊₁→ℤ b) · ℕ₊₁→ℤ d ∎
 
 eq/⁻¹ : ∀ x y → Path ℚ [ x ] [ y ] → x ∼ y

Cubical/Data/Rationals/MoreRationals/QuoQ.agda

@@ -0,0 +1,6 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.Rationals.MoreRationals.QuoQ where
+
+open import Cubical.Data.Rationals.MoreRationals.QuoQ.Base public
+
+open import Cubical.Data.Rationals.MoreRationals.QuoQ.Properties public

Cubical/Data/Rationals/MoreRationals/QuoQ/Base.agda

@@ -0,0 +1,75 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.Rationals.MoreRationals.QuoQ.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+
+open import Cubical.Data.Nat as ℕ using (discreteℕ)
+open import Cubical.Data.NatPlusOne
+open import Cubical.Data.Sigma
+open import Cubical.Data.Int.MoreInts.QuoInt
+
+open import Cubical.HITs.SetQuotients as SetQuotient
+  using ([_]; eq/; discreteSetQuotients) renaming (_/_ to _//_) public
+
+open import Cubical.Relation.Nullary
+open import Cubical.Relation.Binary.Base
+open BinaryRelation
+
+ℕ₊₁→ℤ : ℕ₊₁ → ℤ
+ℕ₊₁→ℤ n = pos (ℕ₊₁→ℕ n)
+
+private
+  ℕ₊₁→ℤ-hom : ∀ m n → ℕ₊₁→ℤ (m ·₊₁ n) ≡ ℕ₊₁→ℤ m · ℕ₊₁→ℤ n
+  ℕ₊₁→ℤ-hom _ _ = refl
+
+
+-- ℚ as a set quotient of ℤ × ℕ₊₁ (as in the HoTT book)
+
+_∼_ : ℤ × ℕ₊₁ → ℤ × ℕ₊₁ → Type₀
+(a , b) ∼ (c , d) = a · ℕ₊₁→ℤ d ≡ c · ℕ₊₁→ℤ b
+
+ℚ : Type₀
+ℚ = (ℤ × ℕ₊₁) // _∼_
+
+
+isSetℚ : isSet ℚ
+isSetℚ = SetQuotient.squash/
+
+[_/_] : ℤ → ℕ₊₁ → ℚ
+[ a / b ] = [ a , b ]
+
+
+isEquivRel∼ : isEquivRel _∼_
+isEquivRel.reflexive isEquivRel∼ (a , b) = refl
+isEquivRel.symmetric isEquivRel∼ (a , b) (c , d) = sym
+isEquivRel.transitive isEquivRel∼ (a , b) (c , d) (e , f) p q = ·-injʳ _ _ _ r
+  where r = (a · ℕ₊₁→ℤ f) · ℕ₊₁→ℤ d ≡[ i ]⟨ ·-comm a (ℕ₊₁→ℤ f) i · ℕ₊₁→ℤ d ⟩
+            (ℕ₊₁→ℤ f · a) · ℕ₊₁→ℤ d ≡⟨ sym (·-assoc (ℕ₊₁→ℤ f) a (ℕ₊₁→ℤ d)) ⟩
+            ℕ₊₁→ℤ f · (a · ℕ₊₁→ℤ d) ≡[ i ]⟨ ℕ₊₁→ℤ f · p i ⟩
+            ℕ₊₁→ℤ f · (c · ℕ₊₁→ℤ b) ≡⟨ ·-assoc (ℕ₊₁→ℤ f) c (ℕ₊₁→ℤ b) ⟩
+            (ℕ₊₁→ℤ f · c) · ℕ₊₁→ℤ b ≡[ i ]⟨ ·-comm (ℕ₊₁→ℤ f) c i · ℕ₊₁→ℤ b ⟩
+            (c · ℕ₊₁→ℤ f) · ℕ₊₁→ℤ b ≡[ i ]⟨ q i · ℕ₊₁→ℤ b ⟩
+            (e · ℕ₊₁→ℤ d) · ℕ₊₁→ℤ b ≡⟨ sym (·-assoc e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ⟩
+            e · (ℕ₊₁→ℤ d · ℕ₊₁→ℤ b) ≡[ i ]⟨ e · ·-comm (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b) i ⟩
+            e · (ℕ₊₁→ℤ b · ℕ₊₁→ℤ d) ≡⟨ ·-assoc e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) ⟩
+            (e · ℕ₊₁→ℤ b) · ℕ₊₁→ℤ d ∎
+
+eq/⁻¹ : ∀ x y → Path ℚ [ x ] [ y ] → x ∼ y
+eq/⁻¹ = SetQuotient.effective (λ _ _ → isSetℤ _ _) isEquivRel∼
+
+discreteℚ : Discrete ℚ
+discreteℚ = discreteSetQuotients isEquivRel∼ (λ _ _ → discreteℤ _ _)
+
+
+-- Natural number and negative integer literals for ℚ
+
+open import Cubical.Data.Nat.Literals public
+
+instance
+  fromNatℚ : HasFromNat ℚ
+  fromNatℚ = record { Constraint = λ _ → Unit ; fromNat = λ n → [ pos n / 1 ] }
+
+instance
+  fromNegℚ : HasFromNeg ℚ
+  fromNegℚ = record { Constraint = λ _ → Unit ; fromNeg = λ n → [ neg n / 1 ] }