Add (Is)DecPreorder to Relation.Binary.* (#2488)

* fix issue #2482

* add `isDecPreorder` manifest fields to `IsDec*Order` structures

* refactored derived sub-`Bundles`

* fixed knock-on consequences

CHANGELOG.md

@@ -322,17 +322,35 @@ Additions to existing modules
   _≡?_ : DecidableEquality (Vec A n)
   ```
 
+* In `Relation.Binary.Bundles`:
+  ```agda
+  record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂))
+  ```
+  plus associated sub-bundles.
+
 * In `Relation.Binary.Construct.Interior.Symmetric`:
   ```agda
   decidable         : Decidable R → Decidable (SymInterior R)
   ```
   and for `Reflexive` and `Transitive` relations `R`:
   ```agda
   isDecEquivalence  : Decidable R → IsDecEquivalence (SymInterior R)
+  isDecPreorder     : Decidable R → IsDecPreorder (SymInterior R) R
   isDecPartialOrder : Decidable R → IsDecPartialOrder (SymInterior R) R
+  decPreorder       : Decidable R → DecPreorder _ _ _
   decPoset          : Decidable R → DecPoset _ _ _
   ```
 
+* In `Relation.Binary.Structures`:
+  ```agda
+  record IsDecPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+    field
+      isPreorder : IsPreorder _≲_
+      _≟_        : Decidable _≈_
+      _≲?_       : Decidable _≲_
+  ```
+  plus associated `isDecPreorder` fields in each higher `IsDec*Order` structure.
+
 * In `Relation.Nullary.Decidable`:
   ```agda
   does-⇔  : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b?

src/Relation/Binary/Bundles.agda

@@ -132,6 +132,36 @@ record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   open Preorder preorder public
     hiding (Carrier; _≈_; _≲_; isPreorder)
 
+
+record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  field
+    Carrier         : Set c
+    _≈_             : Rel Carrier ℓ₁  -- The underlying equality.
+    _≲_             : Rel Carrier ℓ₂  -- The relation.
+    isDecPreorder   : IsDecPreorder _≈_ _≲_
+
+  private module DPO = IsDecPreorder isDecPreorder
+
+  open DPO public
+    using (_≟_; _≲?_; isPreorder)
+
+  preorder : Preorder c ℓ₁ ℓ₂
+  preorder = record
+    { isPreorder = isPreorder
+    }
+
+  open Preorder preorder public
+    hiding (Carrier; _≈_; _≲_; isPreorder; module Eq)
+
+  module Eq where
+    decSetoid : DecSetoid c ℓ₁
+    decSetoid = record
+      { isDecEquivalence = DPO.Eq.isDecEquivalence
+      }
+
+    open DecSetoid decSetoid public
+
+
 ------------------------------------------------------------------------
 -- Partial orders
 ------------------------------------------------------------------------
@@ -173,7 +203,7 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   private module DPO = IsDecPartialOrder isDecPartialOrder
 
   open DPO public
-    using (_≟_; _≤?_; isPartialOrder)
+    using (_≟_; _≤?_; isPartialOrder; isDecPreorder)
 
   poset : Poset c ℓ₁ ℓ₂
   poset = record
@@ -183,13 +213,11 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   open Poset poset public
     hiding (Carrier; _≈_; _≤_; isPartialOrder; module Eq)
 
-  module Eq where
-    decSetoid : DecSetoid c ℓ₁
-    decSetoid = record
-      { isDecEquivalence = DPO.Eq.isDecEquivalence
-      }
+  decPreorder : DecPreorder c ℓ₁ ℓ₂
+  decPreorder = record { isDecPreorder = isDecPreorder }
 
-    open DecSetoid decSetoid public
+  open DecPreorder decPreorder public
+    using (module Eq)
 
 
 record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where

src/Relation/Binary/Construct/Interior/Symmetric.agda

@@ -100,12 +100,6 @@ module _ {R : Rel A ℓ} (refl : Reflexive R) (trans : Transitive R) where
 
   module _ (R? : Decidable R) where
 
-    isDecEquivalence : IsDecEquivalence (SymInterior R)
-    isDecEquivalence = record
-      { isEquivalence = isEquivalence
-      ; _≟_ = decidable R?
-      }
-
     isDecPartialOrder : IsDecPartialOrder (SymInterior R) R
     isDecPartialOrder = record
       { isPartialOrder = isPartialOrder
@@ -115,3 +109,10 @@ module _ {R : Rel A ℓ} (refl : Reflexive R) (trans : Transitive R) where
 
     decPoset : DecPoset _ ℓ ℓ
     decPoset = record { isDecPartialOrder = isDecPartialOrder }
+
+    open DecPoset public
+      using (isDecPreorder; decPreorder)
+
+    isDecEquivalence : IsDecEquivalence (SymInterior R)
+    isDecEquivalence = DecPoset.Eq.isDecEquivalence decPoset
+

src/Relation/Binary/Structures.agda

@@ -119,6 +119,26 @@ record IsTotalPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
   open IsPreorder isPreorder public
 
 
+record IsDecPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+  field
+    isPreorder : IsPreorder _≲_
+    _≟_        : Decidable _≈_
+    _≲?_       : Decidable _≲_
+
+  open IsPreorder isPreorder public
+    hiding (module Eq)
+
+  module Eq where
+
+    isDecEquivalence : IsDecEquivalence
+    isDecEquivalence = record
+      { isEquivalence = isEquivalence
+      ; _≟_           = _≟_
+      }
+
+    open IsDecEquivalence isDecEquivalence public
+
+
 ------------------------------------------------------------------------
 -- Partial orders
 ------------------------------------------------------------------------
@@ -146,15 +166,15 @@ record IsDecPartialOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) whe
   open IsPartialOrder isPartialOrder public
     hiding (module Eq)
 
-  module Eq where
-
-    isDecEquivalence : IsDecEquivalence
-    isDecEquivalence = record
-      { isEquivalence = isEquivalence
-      ; _≟_           = _≟_
-      }
+  isDecPreorder : IsDecPreorder _≤_
+  isDecPreorder = record
+    { isPreorder = isPreorder
+    ; _≟_ = _≟_
+    ; _≲?_ = _≤?_
+    }
 
-    open IsDecEquivalence isDecEquivalence public
+  open IsDecPreorder isDecPreorder public
+    using (module Eq)
 
 
 record IsStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
@@ -234,16 +254,8 @@ record IsDecTotalOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
     ; _≤?_           = _≤?_
     }
 
-  module Eq where
-
-    isDecEquivalence : IsDecEquivalence
-    isDecEquivalence = record
-      { isEquivalence = isEquivalence
-      ; _≟_           = _≟_
-      }
-
-    open IsDecEquivalence isDecEquivalence public
-
+  open IsDecPartialOrder isDecPartialOrder public
+    using (isDecPreorder; module Eq)
 
 -- Note that these orders are decidable. The current implementation
 -- of `Trichotomous` subsumes irreflexivity and asymmetry. See