Add DecEq-Refinement

Contributed by @HeinrichApfelmus

Author: WhatisRT

Class/DecEq/Instances.agda

@@ -26,6 +26,7 @@ private
   ∷-injective : ∀ {x y xs ys} →
     (List⁺ A ∋ x ∷ xs) ≡ y ∷ ys → x ≡ y × xs ≡ ys
   ∷-injective refl = (refl , refl)
+
 module _ ⦃ _ : DecEq A ⦄ where instance
   DecEq-List⁺ : DecEq (List⁺ A)
   DecEq-List⁺ ._≟_ (x ∷ xs) (y ∷ ys)
@@ -44,6 +45,15 @@ module _ ⦃ _ : DecEq A ⦄ where instance
   DecEq-Maybe ._≟_ = M.≡-dec _≟_
     where import Data.Maybe.Properties as M
 
+  open import Data.Refinement
+
+  -- Equality for a Refinement type is decide if the equality
+  -- for the type to be refined is decidable.
+  DecEq-Refinement : ∀ {p} {P : A → Set p} → DecEq (Refinement A P)
+  DecEq-Refinement ._≟_ (x , px) (y , py) with x ≟ y
+  ... | no neq = no (neq ∘ cong value)
+  ... | yes refl = yes refl
+
 module _ ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq B ⦄ where
 
   -- Not exported as instance so that users can also choose `Class.DecEq.WithK.DecEq-Σ`