diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1a6315c7e2..132a9bd594 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -243,7 +243,12 @@ Additions to existing modules
   map-downFrom : ∀ (f : ℕ → A) n → map f (downFrom n) ≡ applyDownFrom f n
   ```
 
-* In `Data.List.Relation.Binary.Permutation.PropositionalProperties`:
+* In `Data.List.Relation.Binary.Permutation.Propositional`:
+  ```agda
+  ↭⇒↭ₛ′ : IsEquivalence _≈_ → _↭_ ⇒ _↭ₛ′_
+  ```
+
+* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
   ```agda
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
   ```
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional.agda b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
index 0e13a5e3ba..9a1dc781cf 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
@@ -88,19 +88,32 @@ data _↭_ : Rel (List A) a where
   }
 
 ------------------------------------------------------------------------
--- _↭_ is equivalent to `Setoid`-based permutation
+-- _↭_ is finer than `Setoid`-based permutation for any equivalence on A
+
+module _ {ℓ} {_≈_ : Rel A ℓ} (isEquivalence : IsEquivalence _≈_) where
+
+  private
+    open module ↭ₛ′ = Permutation record { isEquivalence = isEquivalence }
+      using ()
+      renaming (_↭_ to _↭ₛ′_)
+
+  ↭⇒↭ₛ′ : _↭_ ⇒ _↭ₛ′_
+  ↭⇒↭ₛ′ refl         = ↭ₛ′.↭-refl
+  ↭⇒↭ₛ′ (prep x p)   = ↭ₛ′.↭-prep x (↭⇒↭ₛ′ p)
+  ↭⇒↭ₛ′ (swap x y p) = ↭ₛ′.↭-swap x y (↭⇒↭ₛ′ p)
+  ↭⇒↭ₛ′ (trans p q)  = ↭ₛ′.↭-trans′ (↭⇒↭ₛ′ p) (↭⇒↭ₛ′ q)
+
+
+------------------------------------------------------------------------
+-- _↭_ is equivalent to `Setoid`-based permutation on `≡.setoid A`
 
 private
   open module ↭ₛ = Permutation (≡.setoid A)
     using ()
     renaming (_↭_ to _↭ₛ_)
 
-↭⇒↭ₛ : xs ↭ ys → xs ↭ₛ ys
-↭⇒↭ₛ refl         = ↭ₛ.↭-refl
-↭⇒↭ₛ (prep x p)   = ↭ₛ.↭-prep x (↭⇒↭ₛ p)
-↭⇒↭ₛ (swap x y p) = ↭ₛ.↭-swap x y (↭⇒↭ₛ p)
-↭⇒↭ₛ (trans p q)  = ↭ₛ.↭-trans′ (↭⇒↭ₛ p) (↭⇒↭ₛ q)
-
+↭⇒↭ₛ : _↭_ ⇒ _↭ₛ_
+↭⇒↭ₛ = ↭⇒↭ₛ′ ≡.isEquivalence
 
 ↭ₛ⇒↭ : _↭ₛ_ ⇒ _↭_
 ↭ₛ⇒↭ (↭ₛ.refl xs≋ys)       = ↭-reflexive-≋ xs≋ys