Add _≥_ and _>_ to HasPreorder

src/Interface/HasOrder.agda

@@ -11,13 +11,16 @@ module _ {a} {A : Set a} where
   module _ {_≈_ : Rel A a} where
 
     record HasPreorder : Set (sucˡ a) where
-      infix 4 _≤_ _<_
+      infix 4 _≤_ _<_ _≥_ _>_
       field
         _≤_ _<_       : Rel A a
         ≤-isPreorder  : IsPreorder _≈_ _≤_
         <-irrefl      : Irreflexive _≈_ _<_
         ≤⇔<∨≈         : ∀ {x y} → x ≤ y ⇔ (x < y ⊎ x ≈ y)
 
+      _≥_ = flip _≤_
+      _>_ = flip _<_
+
       open IsPreorder ≤-isPreorder public
         using ()
         renaming (isEquivalence to ≈-isEquivalence; refl to ≤-refl; trans to ≤-trans)

src/Interface/HasOrder/Instance.agda

@@ -23,3 +23,13 @@ instance
     ⊎.[ <⇒≤ , ≤-reflexive ] }
   ℤ-hasPartialOrder = HasPartialOrder ∋ record { ≤-antisym = Int.≤-antisym }
   ℤ-hasDecPartialOrder = HasDecPartialOrder {A = ℤ} ∋ record {}
+
+  open import Data.Rational using (ℚ)
+  import Data.Rational.Properties as Rat hiding (_≟_)
+
+  ℚ-Dec-≤ = ⁇² Rat._≤?_
+  ℚ-Dec-< = ⁇² Rat._<?_
+
+  ℚ-hasPreorder = hasPreorderFromNonStrict Rat.≤-isPreorder _≟_
+  ℚ-hasPartialOrder = HasPartialOrder ∋ record { ≤-antisym = Rat.≤-antisym }
+  ℚ-hasDecPartialOrder = HasDecPartialOrder {A = ℚ} ∋ record {}

src/Prelude.agda

@@ -29,7 +29,7 @@ open import Data.Sum public
 open import Data.Product public
   hiding (assocʳ; assocˡ; map; map₁; map₂; map₂′; swap; _<*>_)
 open import Data.Nat public
-  hiding (_≟_; _≤_; _≤?_; _<_; _<?_; _≤ᵇ_; _≡ᵇ_; less-than-or-equal)
+  hiding (_≟_; _≤_; _≤?_; _<_; _<?_; _≤ᵇ_; _≡ᵇ_; _≥_; _>_; less-than-or-equal)
   renaming (_+_ to _+ℕ_)
 open import Data.Integer as ℤ public
   using (ℤ; _⊖_)