Add (Is)DecPreorder to Relation.Binary.*

CHANGELOG.md

@@ -270,6 +270,11 @@ Additions to existing modules
   _≡?_ : DecidableEquality (Vec A n)
   ```
 
+* In `Relation.Binary.Bundles`:
+  ```agda
+  record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂))
+  ```
+
 * In `Relation.Binary.Construct.Interior.Symmetric`:
   ```agda
   decidable         : Decidable R → Decidable (SymInterior R)
@@ -281,6 +286,15 @@ Additions to existing modules
   decPoset          : Decidable R → DecPoset _ _ _
   ```
 
+* In `Relation.Binary.Structures`:
+  ```agda
+  record IsDecPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+    field
+      isPreorder : IsPreorder _≲_
+      _≟_        : Decidable _≈_
+      _≲?_       : Decidable _≲_
+  ```
+
 * 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,26 @@ 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 _≈_ _≲_
+
+  open IsDecPreorder isDecPreorder public
+    using (_≲?_; isPreorder)
+
+  preorder : Preorder c ℓ₁ ℓ₂
+  preorder = record
+    { isPreorder = isPreorder
+    }
+
+  open Preorder preorder public
+    hiding (Carrier; _≈_; _≲_; isPreorder)
+
+
 ------------------------------------------------------------------------
 -- Partial orders
 ------------------------------------------------------------------------

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
 ------------------------------------------------------------------------