Standardised the binary relation hierarchy (#886)

CHANGELOG.md

@@ -122,6 +122,11 @@ match the one for `Vec`:
   ```
 
 
+#### Other
+
+* The proofs `isPreorder` and `preorder` have been moved from the `Setoid`
+  record to the module `Relation.Binary.Properties.Setoid`.
+
 New modules
 -----------
 The following new modules have been added to the library:

src/Algebra/Solver/Ring.agda

@@ -19,7 +19,7 @@
 
 open import Algebra
 open import Algebra.Solver.Ring.AlmostCommutativeRing
-open import Relation.Binary.Core using (WeaklyDecidable)
+open import Relation.Binary.Definitions using (WeaklyDecidable)
 
 module Algebra.Solver.Ring
   {r₁ r₂ r₃}

src/Axiom/UniquenessOfIdentityProofs.agda

@@ -11,6 +11,7 @@ module Axiom.UniquenessOfIdentityProofs where
 open import Data.Empty
 open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Binary.Core
+open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality.Core
 
 ------------------------------------------------------------------------

src/Category/Monad/Partiality.agda

@@ -18,6 +18,7 @@ open import Function.Core
 open import Function.Equivalence using (_⇔_; equivalence)
 open import Level using (_⊔_)
 open import Relation.Binary as B hiding (Rel)
+import Relation.Binary.Properties.Setoid as SetoidProperties
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Nullary
 open import Relation.Nullary.Decidable hiding (map)
@@ -280,7 +281,7 @@ module _ {a ℓ} {A : Set a} {_∼_ : A → A → Set ℓ} where
   private
     preorder′ : IsEquivalence _∼_ → Kind → Preorder _ _ _
     preorder′ equiv =
-      preorder (Setoid.isPreorder (record { isEquivalence = equiv }))
+      preorder (SetoidProperties.isPreorder (record { isEquivalence = equiv }))
 
   -- The two equalities are equivalence relations.
 

src/Data/Rational/Properties.agda

@@ -62,7 +62,7 @@ mkℚ n₁ d₁ _ ≟ mkℚ n₂ d₂ _ with n₁ ℤ.≟ n₂ | d₁ ℕ.≟ d
 ≡⇒≃ refl = refl
 
 ≃⇒≡ : _≃_ ⇒ _≡_
-≃⇒≡ {i = mkℚ n₁ d₁ c₁} {j = mkℚ n₂ d₂ c₂} eq = helper
+≃⇒≡ {x = mkℚ n₁ d₁ c₁} {y = mkℚ n₂ d₂ c₂} eq = helper
   where
   open ≡-Reasoning