diff --git a/CHANGELOG.md b/CHANGELOG.md
index bbc65af5d7..07a7499a30 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -30,6 +30,15 @@ Non-backwards compatible changes
 Other major improvements
 ------------------------
 
+* Module `Data.List.Relation.Binary.Permutation.Homogeneous` has
+  been comprehensively refactored, introducing
+  ```agda
+  Data.List.Relation.Binary.Permutation.Homogeneous.Properties
+  Data.List.Relation.Binary.Permutation.Homogeneous.Properties.Core
+  ```
+  which then re-export to `Data.List.Relation.Binary.Permutation.Setoid.Properties`
+  and `Data.List.Relation.Binary.Permutation.Propositional.Properties`
+
 Deprecated modules
 ------------------
 
diff --git a/doc/README/Data/List/Relation/Binary/Permutation.agda b/doc/README/Data/List/Relation/Binary/Permutation.agda
index e9141d89c7..5a640b4a7b 100644
--- a/doc/README/Data/List/Relation/Binary/Permutation.agda
+++ b/doc/README/Data/List/Relation/Binary/Permutation.agda
@@ -26,18 +26,18 @@ open import Relation.Binary.PropositionalEquality
 open import Data.List.Relation.Binary.Permutation.Propositional
 
 -- The permutation relation is written as `_↭_` and has four
--- constructors. The first `refl` says that a list is always
--- a permutation of itself, the second `prep` says that if the
+-- *smart* constructors. The first `↭-refl` says that a list is
+-- a permutation of itself, the second `↭-prep` says that if the
 -- heads of the lists are the same they can be skipped, the third
--- `swap` says that the first two elements of the lists can be
--- swapped and the fourth `trans` says that permutation proofs
+-- `↭-swap` says that the first two elements of the lists can be
+-- swapped and the fourth `↭-trans` says that permutation proofs
 -- can be chained transitively.
 
 -- For example a proof that two lists are a permutation of one
 -- another can be written as follows:
 
 lem₁ : 1 ∷ 2 ∷ 3 ∷ [] ↭ 3 ∷ 1 ∷ 2 ∷ []
-lem₁ = trans (prep 1 (swap 2 3 refl)) (swap 1 3 refl)
+lem₁ = ↭-trans (↭-prep 1 (↭-swap 2 3 ↭-refl)) (↭-swap 1 3 ↭-refl)
 
 -- In practice it is difficult to parse the constructors in the
 -- proof above and hence understand why it holds. The
@@ -48,10 +48,21 @@ open PermutationReasoning
 
 lem₂ : 1 ∷ 2 ∷ 3 ∷ [] ↭ 3 ∷ 1 ∷ 2 ∷ []
 lem₂ = begin
-  1 ∷ 2 ∷ 3 ∷ []  ↭⟨ prep 1 (swap 2 3 refl) ⟩
-  1 ∷ 3 ∷ 2 ∷ []  ↭⟨ swap 1 3 refl ⟩
+  1 ∷ 2 ∷ 3 ∷ []  ↭⟨ ↭-prep 1 (↭-swap 2 3 ↭-refl) ⟩
+  1 ∷ 3 ∷ 2 ∷ []  ↭⟨ ↭-swap 1 3 ↭-refl ⟩
   3 ∷ 1 ∷ 2 ∷ []  ∎
 
+-- In practice it is further useful to extend `PermutationReasoning`
+-- with specialised combinators `<⟨_⟩` and `<<⟨_⟩` to support the
+-- distinguished use of the `↭-prep ` and `↭-swap` steps, allowing
+-- the above proof to be recast in the following form:
+
+lem₂ᵣ : 1 ∷ 2 ∷ 3 ∷ [] ↭ 3 ∷ 1 ∷ 2 ∷ []
+lem₂ᵣ = begin
+  1 ∷ (2 ∷ (3 ∷ [])) <⟨ ↭-swap 2 3 ↭-refl ⟩
+  1 ∷ 3 ∷ (2 ∷ [])   <<⟨ ↭-refl ⟩
+  3 ∷ 1 ∷ (2 ∷ [])   ∎
+
 -- As might be expected, properties of the permutation relation may be
 -- found in:
 
diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index 389721d4c5..40964d151e 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -22,7 +22,6 @@ open import Data.List.Membership.Propositional using (_∈_)
 open import Data.List.Membership.Propositional.Properties
 open import Data.List.Relation.Binary.Subset.Propositional.Properties
   using (⊆-preorder)
-open import Data.List.Relation.Binary.Permutation.Propositional
 open import Data.List.Relation.Binary.Permutation.Propositional.Properties
 open import Data.Product.Base as Prod hiding (map)
 import Data.Product.Function.Dependent.Propositional as Σ
@@ -31,7 +30,7 @@ open import Data.Sum.Properties hiding (map-cong)
 open import Data.Sum.Function.Propositional using (_⊎-cong_)
 open import Data.Unit.Polymorphic.Base
 open import Function.Base
-open import Function.Bundles using (_↔_; Inverse; Equivalence; mk↔ₛ′; mk⇔)
+open import Function.Bundles using (_↔_; Inverse; Equivalence; mk↔ₛ′; mk↔; mk⇔)
 open import Function.Related.Propositional as Related
   using (↔⇒; ⌊_⌋; ⌊_⌋→; ⇒→; K-refl; SK-sym)
 open import Function.Related.TypeIsomorphisms
@@ -538,25 +537,32 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
 
   lemma : ∀ {xs ys} (inv : x ∷ xs ∼[ bag ] x ∷ ys) {z} →
           Well-behaved (Inverse.to (∼→⊎↔⊎ inv {z}))
-  lemma {xs} inv {b = z∈xs} {a = p} {a′ = q} hyp₁ hyp₂ with
-    zero                                                                  ≡⟨⟩
-    index-of {xs = x ∷ xs} (here p)                                       ≡⟨⟩
-    index-of {xs = x ∷ xs} (to (∷↔ _) $ inj₁ p)                         ≡⟨ ≡.cong (index-of ∘ (to (∷↔ (_ ≡_)))) $ ≡.sym $
-                                                                               to-from (∼→⊎↔⊎ inv) {x = inj₁ p} hyp₂ ⟩
-    index-of {xs = x ∷ xs} (to (∷↔ _) $ (from (∼→⊎↔⊎ inv) $ inj₁ q))  ≡⟨ ≡.cong index-of $
-                                                                               strictlyInverseˡ (∷↔ _) (from inv (here q)) ⟩
-    index-of {xs = x ∷ xs} (to (SK-sym inv) $ here q)                   ≡⟨ index-equality-preserved (SK-sym inv) refl ⟩
-    index-of {xs = x ∷ xs} (to (SK-sym inv) $ here p)                   ≡⟨ ≡.cong index-of $ ≡.sym $
-                                                                               strictlyInverseˡ (∷↔ _) (from inv (here p)) ⟩
-    index-of {xs = x ∷ xs} (to (∷↔ _) (from (∼→⊎↔⊎ inv) $ inj₁ p))  ≡⟨ ≡.cong (index-of ∘ (to (∷↔ (_ ≡_)))) $
-                                                                               to-from (∼→⊎↔⊎ inv) {x = inj₂ z∈xs} hyp₁ ⟩
-    index-of {xs = x ∷ xs} (to (∷↔ _) $ inj₂ z∈xs)                      ≡⟨⟩
-    index-of {xs = x ∷ xs} (there z∈xs)                                   ≡⟨⟩
-    suc (index-of {xs = xs} z∈xs)                                         ∎
+  lemma {xs} inv {b = z∈xs} {a = p} {a′ = q} hyp₁ hyp₂ = case contra of λ ()
     where
     open Inverse
     open ≡-Reasoning
-  ... | ()
+    contra : zero ≡ suc (index-of {xs = xs} z∈xs)
+    contra = begin
+      zero
+        ≡⟨⟩
+      index-of {xs = x ∷ xs} (here p)
+        ≡⟨⟩
+      index-of {xs = x ∷ xs} (to (∷↔ _) $ inj₁ p)
+        ≡⟨ ≡.cong (index-of ∘ (to (∷↔ (_ ≡_)))) $ to-from (∼→⊎↔⊎ inv) {x = inj₁ p} hyp₂ ⟨
+      index-of {xs = x ∷ xs} (to (∷↔ _) $ (from (∼→⊎↔⊎ inv) $ inj₁ q))
+        ≡⟨ ≡.cong index-of $ strictlyInverseˡ (∷↔ _) (from inv (here q)) ⟩
+      index-of {xs = x ∷ xs} (to (SK-sym inv) $ here q)
+        ≡⟨ index-equality-preserved (SK-sym inv) refl ⟩
+      index-of {xs = x ∷ xs} (to (SK-sym inv) $ here p)
+        ≡⟨ ≡.cong index-of $ strictlyInverseˡ (∷↔ _) (from inv (here p)) ⟨
+      index-of {xs = x ∷ xs} (to (∷↔ _) (from (∼→⊎↔⊎ inv) $ inj₁ p))
+        ≡⟨ ≡.cong (index-of ∘ (to (∷↔ (_ ≡_)))) $ to-from (∼→⊎↔⊎ inv) {x = inj₂ z∈xs} hyp₁ ⟩
+      index-of {xs = x ∷ xs} (to (∷↔ _) $ inj₂ z∈xs)
+        ≡⟨⟩
+      index-of {xs = x ∷ xs} (there z∈xs)
+        ≡⟨⟩
+      suc (index-of {xs = xs} z∈xs)
+        ∎
 
 ------------------------------------------------------------------------
 -- Relationships to other relations
@@ -564,36 +570,27 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
 ↭⇒∼bag : _↭_ {A = A} ⇒ _∼[ bag ]_
 ↭⇒∼bag {A = A} xs↭ys {v} = mk↔ₛ′ (to xs↭ys) (from xs↭ys) (to∘from xs↭ys) (from∘to xs↭ys)
   where
-  to : ∀ {xs ys} → xs ↭ ys → v ∈ xs → v ∈ ys
-  to xs↭ys = Any-resp-↭ {A = A} xs↭ys
-
-  from : ∀ {xs ys} → xs ↭ ys → v ∈ ys → v ∈ xs
-  from xs↭ys = Any-resp-↭ (↭-sym xs↭ys)
-
-  from∘to : ∀ {xs ys} (p : xs ↭ ys) (q : v ∈ xs) → from p (to p q) ≡ q
-  from∘to refl          v∈xs                 = refl
-  from∘to (prep _ _)    (here refl)          = refl
-  from∘to (prep _ p)    (there v∈xs)         = ≡.cong there (from∘to p v∈xs)
-  from∘to (swap x y p)  (here refl)          = refl
-  from∘to (swap x y p)  (there (here refl))  = refl
-  from∘to (swap x y p)  (there (there v∈xs)) = ≡.cong (there ∘ there) (from∘to p v∈xs)
-  from∘to (trans p₁ p₂) v∈xs
-    rewrite from∘to p₂ (Any-resp-↭ p₁ v∈xs)
-          | from∘to p₁ v∈xs                  = refl
-
-  to∘from : ∀ {xs ys} (p : xs ↭ ys) (q : v ∈ ys) → to p (from p q) ≡ q
-  to∘from p with from∘to (↭-sym p)
-  ... | res rewrite ↭-sym-involutive p = res
+
+  to : xs ↭ ys → v ∈ xs → v ∈ ys
+  to = ∈-resp-↭
+
+  from : xs ↭ ys → v ∈ ys → v ∈ xs
+  from = ∈-resp-↭ ∘ ↭-sym
+
+  from∘to : (p : xs ↭ ys) (ix : v ∈ xs) → from p (to p ix) ≡ ix
+  from∘to p _ = ∈-resp-↭-sym p
+
+  to∘from : (p : xs ↭ ys) (iy : v ∈ ys) → to p (from p iy) ≡ iy
+  to∘from p _ = ∈-resp-↭-sym⁻¹ p
 
 ∼bag⇒↭ : _∼[ bag ]_ ⇒ _↭_ {A = A}
-∼bag⇒↭ {A = A} {[]} eq with empty-unique (↔-sym eq)
-... | refl = refl
-∼bag⇒↭ {A = A} {x ∷ xs} eq with ∈-∃++ (Inverse.to (eq {x}) (here ≡.refl))
-... | zs₁ , zs₂ , p rewrite p = begin
-  x ∷ xs           <⟨ ∼bag⇒↭ (drop-cons (↔-trans eq (comm zs₁ (x ∷ zs₂)))) ⟩
-  x ∷ (zs₂ ++ zs₁) <⟨ ++-comm zs₂ zs₁ ⟩
-  x ∷ (zs₁ ++ zs₂) ↭⟨ shift x zs₁ zs₂ ⟨
-  zs₁ ++ x ∷ zs₂   ∎
+∼bag⇒↭ {A = A} {[]}     eq with refl ← empty-unique (↔-sym eq)      = ↭-refl
+∼bag⇒↭ {A = A} {x ∷ xs} eq
+  with zs₁ , zs₂ , refl ← ∈-∃++ (Inverse.to (eq {x}) (here ≡.refl)) = begin
+    x ∷ xs           <⟨ ∼bag⇒↭ (drop-cons (↔-trans eq (comm zs₁ (x ∷ zs₂)))) ⟩
+    x ∷ (zs₂ ++ zs₁) <⟨ ++-comm zs₂ zs₁ ⟩
+    x ∷ (zs₁ ++ zs₂) ↭⟨ ↭-shift zs₁ ⟨
+    zs₁ ++ x ∷ zs₂   ∎
   where
   open CommutativeMonoid (commutativeMonoid bag A)
   open PermutationReasoning
diff --git a/src/Data/List/Relation/Binary/Equality/Propositional.agda b/src/Data/List/Relation/Binary/Equality/Propositional.agda
index ffae515086..553348a920 100644
--- a/src/Data/List/Relation/Binary/Equality/Propositional.agda
+++ b/src/Data/List/Relation/Binary/Equality/Propositional.agda
@@ -14,7 +14,7 @@ open import Relation.Binary.Core using (_⇒_)
 
 module Data.List.Relation.Binary.Equality.Propositional {a} {A : Set a} where
 
-open import Data.List.Base
+import Data.List.Base as List
 import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 import Relation.Binary.PropositionalEquality.Properties as ≡
@@ -29,7 +29,7 @@ open SetoidEquality (≡.setoid A) public
 
 ≋⇒≡ : _≋_ ⇒ _≡_
 ≋⇒≡ []             = refl
-≋⇒≡ (refl ∷ xs≈ys) = cong (_ ∷_) (≋⇒≡ xs≈ys)
+≋⇒≡ (refl ∷ xs≈ys) = cong (_ List.∷_) (≋⇒≡ xs≈ys)
 
 ≡⇒≋ : _≡_ ⇒ _≋_
 ≡⇒≋ refl = ≋-refl
diff --git a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
index 12015b3076..ee331d82cb 100644
--- a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
@@ -8,54 +8,59 @@
 
 module Data.List.Relation.Binary.Permutation.Homogeneous where
 
-open import Data.List.Base using (List; _∷_)
-open import Data.List.Relation.Binary.Pointwise.Base as Pointwise
-  using (Pointwise)
-open import Data.List.Relation.Binary.Pointwise.Properties as Pointwise
-  using (symmetric)
+open import Data.List.Base as List using (List; []; _∷_)
+open import Data.List.Relation.Binary.Pointwise as Pointwise
+  using (Pointwise; []; _∷_)
+open import Data.Nat.Base using (ℕ; suc; _+_; _<_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (Rel; _⇒_)
-open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Structures using (IsEquivalence)
-open import Relation.Binary.Definitions using (Reflexive; Symmetric)
 
 private
   variable
     a r s : Level
     A : Set a
+    xs ys zs : List A
+    x y x′ y′ : A
 
-data Permutation {A : Set a} (R : Rel A r) : Rel (List A) (a ⊔ r) where
-  refl  : ∀ {xs ys} → Pointwise R xs ys → Permutation R xs ys
-  prep  : ∀ {xs ys x y} (eq : R x y) → Permutation R xs ys → Permutation R (x ∷ xs) (y ∷ ys)
-  swap  : ∀ {xs ys x y x′ y′} (eq₁ : R x x′) (eq₂ : R y y′) → Permutation R xs ys → Permutation R (x ∷ y ∷ xs) (y′ ∷ x′ ∷ ys)
-  trans : ∀ {xs ys zs} → Permutation R xs ys → Permutation R ys zs → Permutation R xs zs
 
 ------------------------------------------------------------------------
--- The Permutation relation is an equivalence
-
-module _ {R : Rel A r}  where
-
-  sym : Symmetric R → Symmetric (Permutation R)
-  sym R-sym (refl xs∼ys)           = refl (Pointwise.symmetric R-sym xs∼ys)
-  sym R-sym (prep x∼x′ xs↭ys)      = prep (R-sym x∼x′) (sym R-sym xs↭ys)
-  sym R-sym (swap x∼x′ y∼y′ xs↭ys) = swap (R-sym y∼y′) (R-sym x∼x′) (sym R-sym xs↭ys)
-  sym R-sym (trans xs↭ys ys↭zs)    = trans (sym R-sym ys↭zs) (sym R-sym xs↭ys)
-
-  isEquivalence : Reflexive R → Symmetric R → IsEquivalence (Permutation R)
-  isEquivalence R-refl R-sym = record
-    { refl  = refl (Pointwise.refl R-refl)
-    ; sym   = sym R-sym
-    ; trans = trans
-    }
-
-  setoid : Reflexive R → Symmetric R → Setoid _ _
-  setoid R-refl R-sym = record
-    { isEquivalence = isEquivalence R-refl R-sym
-    }
-
-map : ∀ {R : Rel A r} {S : Rel A s} →
-      (R ⇒ S) → (Permutation R ⇒ Permutation S)
-map R⇒S (refl xs∼ys)         = refl (Pointwise.map R⇒S xs∼ys)
-map R⇒S (prep e xs∼ys)       = prep (R⇒S e) (map R⇒S xs∼ys)
-map R⇒S (swap e₁ e₂ xs∼ys)   = swap (R⇒S e₁) (R⇒S e₂) (map R⇒S xs∼ys)
-map R⇒S (trans xs∼ys ys∼zs)  = trans (map R⇒S xs∼ys) (map R⇒S ys∼zs)
+-- Definition
+
+module _ {A : Set a} (R : Rel A r) where
+
+  data Permutation : Rel (List A) (a ⊔ r) where
+    refl  : Pointwise R xs ys → Permutation xs ys
+    prep  : (eq : R x y) → Permutation xs ys → Permutation (x ∷ xs) (y ∷ ys)
+    swap  : (eq₁ : R x x′) (eq₂ : R y y′) → Permutation xs ys →
+            Permutation (x ∷ y ∷ xs) (y′ ∷ x′ ∷ ys)
+    trans : Permutation xs ys → Permutation ys zs → Permutation xs zs
+
+------------------------------------------------------------------------
+-- Map
+
+module _ {R : Rel A r} {S : Rel A s} where
+
+  map : (R ⇒ S) → (Permutation R ⇒ Permutation S)
+  map R⇒S (refl xs∼ys)         = refl (Pointwise.map R⇒S xs∼ys)
+  map R⇒S (prep e xs∼ys)       = prep (R⇒S e) (map R⇒S xs∼ys)
+  map R⇒S (swap e₁ e₂ xs∼ys)   = swap (R⇒S e₁) (R⇒S e₂) (map R⇒S xs∼ys)
+  map R⇒S (trans xs∼ys ys∼zs)  = trans (map R⇒S xs∼ys) (map R⇒S ys∼zs)
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.1
+
+steps : {R : Rel A r} → Permutation R xs ys → ℕ
+steps (refl _)            = 1
+steps (prep _ xs↭ys)      = suc (steps xs↭ys)
+steps (swap _ _ xs↭ys)    = suc (steps xs↭ys)
+steps (trans xs↭ys ys↭zs) = steps xs↭ys + steps ys↭zs
+
+{-# WARNING_ON_USAGE steps
+"Warning: steps was deprecated in v2.1."
+#-}
diff --git a/src/Data/List/Relation/Binary/Permutation/Homogeneous/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Homogeneous/Properties.agda
new file mode 100644
index 0000000000..43cada1872
--- /dev/null
+++ b/src/Data/List/Relation/Binary/Permutation/Homogeneous/Properties.agda
@@ -0,0 +1,322 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of the `Homogeneous` definition of permutation
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --warn=noUserWarning #-} -- for deprecated function `steps`
+
+module Data.List.Relation.Binary.Permutation.Homogeneous.Properties where
+
+open import Algebra.Bundles using (CommutativeMonoid)
+open import Data.List.Base as List using (List; []; _∷_; [_]; _++_; length)
+open import Data.List.Relation.Binary.Pointwise as Pointwise
+  using (Pointwise; []; _∷_)
+open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
+open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
+import Data.List.Relation.Unary.Any.Properties as Any
+open import Data.Nat.Base using (ℕ; suc; _+_; _<_)
+import Data.Nat.Properties as ℕ
+open import Data.Product.Base using (_,_; _×_; ∃)
+open import Function.Base using (_∘_; flip)
+open import Level using (Level; _⊔_)
+open import Relation.Binary.Core using (Rel; _Preserves_⟶_)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+open import Relation.Binary.Definitions
+  using ( Reflexive; Symmetric; Transitive
+        ; _Respects_; _Respects₂_; _Respectsˡ_; _Respectsʳ_)
+open import Relation.Binary.PropositionalEquality.Core as ≡
+  using (_≡_ ; cong; cong₂)
+open import Relation.Nullary.Decidable using (yes; no; does)
+open import Relation.Nullary.Negation using (¬_; contradiction)
+open import Relation.Unary using (Pred; Decidable)
+
+open import Data.List.Relation.Binary.Permutation.Homogeneous
+import Data.List.Relation.Binary.Permutation.Homogeneous.Properties.Core as Properties
+
+private
+  variable
+    a p r s : Level
+    A B : Set a
+    xs ys zs : List A
+    x y z v w : A
+    P : Pred A p
+    R : Rel A r
+    S : Rel A s
+
+------------------------------------------------------------------------
+-- Re-export `Core` properties
+------------------------------------------------------------------------
+
+open Properties public
+
+------------------------------------------------------------------------
+-- Inversion principles
+------------------------------------------------------------------------
+
+
+↭-[]-invˡ : Permutation R [] xs → xs ≡ []
+↭-[]-invˡ (refl [])           = ≡.refl
+↭-[]-invˡ (trans xs↭ys ys↭zs) with ≡.refl ← ↭-[]-invˡ xs↭ys = ↭-[]-invˡ ys↭zs
+
+↭-[]-invʳ : Permutation R xs [] → xs ≡ []
+↭-[]-invʳ (refl [])           = ≡.refl
+↭-[]-invʳ (trans xs↭ys ys↭zs) with ≡.refl ← ↭-[]-invʳ ys↭zs = ↭-[]-invʳ xs↭ys
+
+¬x∷xs↭[]ˡ : ¬ (Permutation R [] (x ∷ xs))
+¬x∷xs↭[]ˡ (trans xs↭ys ys↭zs) with ≡.refl ← ↭-[]-invˡ xs↭ys = ¬x∷xs↭[]ˡ ys↭zs
+
+¬x∷xs↭[]ʳ : ¬ (Permutation R (x ∷ xs) [])
+¬x∷xs↭[]ʳ (trans xs↭ys ys↭zs) with ≡.refl ← ↭-[]-invʳ ys↭zs = ¬x∷xs↭[]ʳ xs↭ys
+
+module _ (R-trans : Transitive R) where
+
+  ↭-singleton-invˡ : Permutation R [ x ] xs → ∃ λ y → xs ≡ [ y ] × R x y
+  ↭-singleton-invˡ (refl (xRy ∷ [])) = _ , ≡.refl , xRy
+  ↭-singleton-invˡ (prep xRy p)
+    with ≡.refl ← ↭-[]-invˡ p     = _ , ≡.refl , xRy
+  ↭-singleton-invˡ (trans r s)
+    with _ , ≡.refl , xRy ← ↭-singleton-invˡ r
+    with _ , ≡.refl , yRz ← ↭-singleton-invˡ s
+    = _ , ≡.refl , R-trans xRy yRz
+
+  ↭-singleton-invʳ : Permutation R xs [ x ] → ∃ λ y → xs ≡ [ y ] × R y x
+  ↭-singleton-invʳ (refl (yRx ∷ [])) = _ , ≡.refl , yRx
+  ↭-singleton-invʳ (prep yRx p)
+    with ≡.refl ← ↭-[]-invʳ p     = _ , ≡.refl , yRx
+  ↭-singleton-invʳ (trans r s)
+    with _ , ≡.refl , yRx ← ↭-singleton-invʳ s
+    with _ , ≡.refl , zRy ← ↭-singleton-invʳ r
+    = _ , ≡.refl , R-trans zRy yRx
+
+
+------------------------------------------------------------------------
+-- Properties of List functions, possibly depending on properties of R
+------------------------------------------------------------------------
+
+-- length
+
+↭-length : Permutation R xs ys → length xs ≡ length ys
+↭-length (refl xs≋ys)        = Pointwise.Pointwise-length xs≋ys
+↭-length (prep _ xs↭ys)      = cong suc (↭-length xs↭ys)
+↭-length (swap _ _ xs↭ys)    = cong (suc ∘ suc) (↭-length xs↭ys)
+↭-length (trans xs↭ys ys↭zs) = ≡.trans (↭-length xs↭ys) (↭-length ys↭zs)
+
+-- map
+
+module _ {f} (pres : f Preserves R ⟶ S) where
+
+  map⁺ : Permutation R xs ys → Permutation S (List.map f xs) (List.map f ys)
+
+  map⁺ (refl xs≋ys)        = refl (Pointwise.map⁺ _ _ (Pointwise.map pres xs≋ys))
+  map⁺ (prep x xs↭ys)      = prep (pres x) (map⁺ xs↭ys)
+  map⁺ (swap x y xs↭ys)    = swap (pres x) (pres y) (map⁺ xs↭ys)
+  map⁺ (trans xs↭ys ys↭zs) = trans (map⁺ xs↭ys) (map⁺ ys↭zs)
+
+
+-- _++_
+
+module _ (R-refl : Reflexive R) where
+
+  ++⁺ʳ : ∀ zs → Permutation R xs ys →
+         Permutation R (xs List.++ zs) (ys List.++ zs)
+  ++⁺ʳ zs (refl xs≋ys)        = refl (Pointwise.++⁺ xs≋ys (Pointwise.refl R-refl))
+  ++⁺ʳ zs (prep x xs↭ys)      = prep x (++⁺ʳ zs xs↭ys)
+  ++⁺ʳ zs (swap x y xs↭ys)    = swap x y (++⁺ʳ zs xs↭ys)
+  ++⁺ʳ zs (trans xs↭ys ys↭zs) = trans (++⁺ʳ zs xs↭ys) (++⁺ʳ zs ys↭zs)
+
+
+-- filter
+
+module _ (R-sym : Symmetric R)
+         (P? : Decidable P) (P≈ : P Respects R) where
+
+  filter⁺ : Permutation R xs ys →
+            Permutation R (List.filter P? xs) (List.filter P? ys)
+  filter⁺ (refl xs≋ys)        = refl (Pointwise.filter⁺ P? P? P≈ (P≈ ∘ R-sym) xs≋ys)
+  filter⁺ (trans xs↭zs zs↭ys) = trans (filter⁺ xs↭zs) (filter⁺ zs↭ys)
+  filter⁺ {x ∷ xs} {y ∷ ys} (prep x≈y xs↭ys) with P? x | P? y
+  ... | yes _  | yes _  = prep x≈y (filter⁺ xs↭ys)
+  ... | yes Px | no ¬Py = contradiction (P≈ x≈y Px) ¬Py
+  ... | no ¬Px | yes Py = contradiction (P≈ (R-sym x≈y) Py) ¬Px
+  ... | no  _  | no  _  = filter⁺ xs↭ys
+  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) with P? x | P? y
+  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | no ¬Px | no ¬Py
+    with P? z | P? w
+  ... | _      | yes Pw = contradiction (P≈ w≈y Pw) ¬Py
+  ... | yes Pz | _      = contradiction (P≈ (R-sym x≈z) Pz) ¬Px
+  ... | no _   | no  _  = filter⁺ xs↭ys
+  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | no ¬Px | yes Py
+    with P? z | P? w
+  ... | _      | no ¬Pw = contradiction (P≈ (R-sym w≈y) Py) ¬Pw
+  ... | yes Pz | _      = contradiction (P≈ (R-sym x≈z) Pz) ¬Px
+  ... | no _   | yes _  = prep w≈y (filter⁺ xs↭ys)
+  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys)  | yes Px | no ¬Py
+    with P? z | P? w
+  ... | no ¬Pz | _      = contradiction (P≈ x≈z Px) ¬Pz
+  ... | _      | yes Pw = contradiction (P≈ w≈y Pw) ¬Py
+  ... | yes _  | no _   = prep x≈z (filter⁺ xs↭ys)
+  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | yes Px | yes Py
+    with P? z | P? w
+  ... | no ¬Pz | _      = contradiction (P≈ x≈z Px) ¬Pz
+  ... | _      | no ¬Pw = contradiction (P≈ (R-sym w≈y) Py) ¬Pw
+  ... | yes _  | yes _  = swap x≈z w≈y (filter⁺ xs↭ys)
+
+
+------------------------------------------------------------------------
+-- foldr over a Commutative Monoid
+
+module _ (commutativeMonoid : CommutativeMonoid a r) where
+
+  private
+    foldr = List.foldr
+    open module CM = CommutativeMonoid commutativeMonoid
+
+  foldr-commMonoid : Permutation _≈_ xs ys → foldr _∙_ ε xs ≈ foldr _∙_ ε ys
+  foldr-commMonoid (refl xs≋ys) = Pointwise.foldr⁺ ∙-cong CM.refl xs≋ys
+  foldr-commMonoid (prep x≈y xs↭ys) = ∙-cong x≈y (foldr-commMonoid xs↭ys)
+  foldr-commMonoid (swap {x} {x′} {y} {y′} {xs} {ys} x≈x′ y≈y′ xs↭ys) = begin
+    x ∙ (y ∙ foldr _∙_ ε xs)   ≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩
+    x ∙ (y ∙ foldr _∙_ ε ys)   ≈⟨ assoc x y (foldr _∙_ ε ys) ⟨
+    (x ∙ y) ∙ foldr _∙_ ε ys   ≈⟨ ∙-congʳ (comm x y) ⟩
+    (y ∙ x) ∙ foldr _∙_ ε ys   ≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩
+    (y′ ∙ x′) ∙ foldr _∙_ ε ys ≈⟨ assoc y′ x′ (foldr _∙_ ε ys) ⟩
+    y′ ∙ (x′ ∙ foldr _∙_ ε ys) ∎
+    where open ≈-Reasoning CM.setoid
+  foldr-commMonoid (trans xs↭ys ys↭zs) =
+    CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs)
+
+
+------------------------------------------------------------------------
+-- Relationships to other predicates
+------------------------------------------------------------------------
+
+-- All and Any
+
+module _ (resp : P Respects R) where
+
+  All-resp-↭ : (All P) Respects (Permutation R)
+  All-resp-↭ (refl xs≋ys)   pxs             = Pointwise.All-resp-Pointwise resp xs≋ys pxs
+  All-resp-↭ (prep x≈y p)   (px ∷ pxs)      = resp x≈y px ∷ All-resp-↭ p pxs
+  All-resp-↭ (swap ≈₁ ≈₂ p) (px ∷ py ∷ pxs) = resp ≈₂ py ∷ resp ≈₁ px ∷ All-resp-↭ p pxs
+  All-resp-↭ (trans p₁ p₂)  pxs             = All-resp-↭ p₂ (All-resp-↭ p₁ pxs)
+
+  Any-resp-↭ : (Any P) Respects (Permutation R)
+  Any-resp-↭ (refl xs≋ys) pxs                   = Pointwise.Any-resp-Pointwise resp xs≋ys pxs
+  Any-resp-↭ (prep x≈y p) (here px)             = here (resp x≈y px)
+  Any-resp-↭ (prep x≈y p) (there pxs)           = there (Any-resp-↭ p pxs)
+  Any-resp-↭ (swap ≈₁ ≈₂ p) (here px)           = there (here (resp ≈₁ px))
+  Any-resp-↭ (swap ≈₁ ≈₂ p) (there (here px))   = here (resp ≈₂ px)
+  Any-resp-↭ (swap ≈₁ ≈₂ p) (there (there pxs)) = there (there (Any-resp-↭ p pxs))
+  Any-resp-↭ (trans p₁ p₂) pxs                  = Any-resp-↭ p₂ (Any-resp-↭ p₁ pxs)
+
+-- Membership
+
+module _ {_≈_ : Rel A r} (≈-trans : Transitive _≈_) where
+
+  private
+    ∈-resp : ∀ {x} → (x ≈_) Respects _≈_
+    ∈-resp = flip ≈-trans
+
+  ∈-resp-Pointwise : (Any (x ≈_)) Respects (Pointwise _≈_)
+  ∈-resp-Pointwise = Pointwise.Any-resp-Pointwise ∈-resp
+
+  ∈-resp-↭ : (Any (x ≈_)) Respects (Permutation _≈_)
+  ∈-resp-↭ = Any-resp-↭ ∈-resp
+
+-- AllPairs
+
+module _ (sym : Symmetric S) (resp@(rʳ , rˡ) : S Respects₂ R) where
+
+  AllPairs-resp-↭ : (AllPairs S) Respects (Permutation R)
+  AllPairs-resp-↭ (refl xs≋ys)     pxs             =
+    Pointwise.AllPairs-resp-Pointwise resp xs≋ys pxs
+  AllPairs-resp-↭ (prep x≈y p)     (∼ ∷ pxs)       =
+    All-resp-↭ rʳ p (All.map (rˡ x≈y) ∼) ∷ AllPairs-resp-↭ p pxs
+  AllPairs-resp-↭ (swap eq₁ eq₂ p) ((∼₁ ∷ ∼₂) ∷ ∼₃ ∷ pxs) =
+    (sym (rʳ eq₂ (rˡ eq₁ ∼₁)) ∷ All-resp-↭ rʳ p (All.map (rˡ eq₂) ∼₃)) ∷
+    All-resp-↭ rʳ p (All.map (rˡ eq₁) ∼₂) ∷ AllPairs-resp-↭ p pxs
+  AllPairs-resp-↭ (trans p₁ p₂)    pxs             =
+    AllPairs-resp-↭ p₂ (AllPairs-resp-↭ p₁ pxs)
+
+
+------------------------------------------------------------------------
+-- Properties of steps, and related properties of Permutation
+-- previously required for proofs by well-founded induction
+-- rendered obsolete/deprecatable by Core.↭-transˡ-≋ , Core.↭-transʳ-≋
+------------------------------------------------------------------------
+
+module Steps {R : Rel A r} where
+
+-- Basic property
+
+  0<steps : (xs↭ys : Permutation R xs ys) → 0 < steps xs↭ys
+  0<steps (refl _)             = ℕ.n<1+n 0
+  0<steps (prep eq xs↭ys)      = ℕ.m<n⇒m<1+n (0<steps xs↭ys)
+  0<steps (swap eq₁ eq₂ xs↭ys) = ℕ.m<n⇒m<1+n (0<steps xs↭ys)
+  0<steps (trans xs↭ys ys↭zs) =
+    ℕ.<-≤-trans (0<steps xs↭ys) (ℕ.m≤m+n (steps xs↭ys) (steps ys↭zs))
+
+  module _ (R-trans : Transitive R) where
+
+    private
+      ≋-trans : Transitive (Pointwise R)
+      ≋-trans = Pointwise.transitive R-trans
+
+    ↭-respʳ-≋ : (Permutation R) Respectsʳ (Pointwise R)
+    ↭-respʳ-≋ xs≋ys               (refl zs≋xs)         = refl (≋-trans zs≋xs xs≋ys)
+    ↭-respʳ-≋ (x≈y ∷ xs≋ys)       (prep eq zs↭xs)      = prep (R-trans eq x≈y) (↭-respʳ-≋ xs≋ys zs↭xs)
+    ↭-respʳ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ zs↭xs) = swap (R-trans eq₁ w≈z) (R-trans eq₂ x≈y) (↭-respʳ-≋ xs≋ys zs↭xs)
+    ↭-respʳ-≋ xs≋ys               (trans ws↭zs zs↭xs)  = trans ws↭zs (↭-respʳ-≋ xs≋ys zs↭xs)
+
+    steps-respʳ : (xs≋ys : Pointwise R xs ys) (zs↭xs : Permutation R zs xs) →
+                  steps (↭-respʳ-≋ xs≋ys zs↭xs) ≡ steps zs↭xs
+    steps-respʳ _               (refl _)            = ≡.refl
+    steps-respʳ (_ ∷ ys≋xs)     (prep _ ys↭zs)      = cong suc (steps-respʳ ys≋xs ys↭zs)
+    steps-respʳ (_ ∷ _ ∷ ys≋xs) (swap _ _ ys↭zs)    = cong suc (steps-respʳ ys≋xs ys↭zs)
+    steps-respʳ ys≋xs           (trans ys↭ws ws↭zs) = cong (steps ys↭ws +_) (steps-respʳ ys≋xs ws↭zs)
+
+    module _ (R-sym : Symmetric R) where
+
+      private
+        ≋-sym : Symmetric (Pointwise R)
+        ≋-sym = Pointwise.symmetric R-sym
+
+      ↭-respˡ-≋ : (Permutation R) Respectsˡ (Pointwise R)
+      ↭-respˡ-≋ xs≋ys               (refl ys≋zs)         = refl (≋-trans (≋-sym xs≋ys) ys≋zs)
+      ↭-respˡ-≋ (x≈y ∷ xs≋ys)       (prep eq zs↭xs)      = prep (R-trans (R-sym x≈y) eq) (↭-respˡ-≋ xs≋ys zs↭xs)
+      ↭-respˡ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ zs↭xs) = swap (R-trans (R-sym x≈y) eq₁) (R-trans (R-sym w≈z) eq₂) (↭-respˡ-≋ xs≋ys zs↭xs)
+      ↭-respˡ-≋ xs≋ys               (trans ws↭zs zs↭xs)  = trans (↭-respˡ-≋ xs≋ys ws↭zs) zs↭xs
+
+      steps-respˡ : (ys≋xs : Pointwise R ys xs) (ys↭zs : Permutation R ys zs) →
+                    steps (↭-respˡ-≋ ys≋xs ys↭zs) ≡ steps ys↭zs
+      steps-respˡ _               (refl _)            = ≡.refl
+      steps-respˡ (_ ∷ ys≋xs)     (prep _ ys↭zs)      = cong suc (steps-respˡ ys≋xs ys↭zs)
+      steps-respˡ (_ ∷ _ ∷ ys≋xs) (swap _ _ ys↭zs)    = cong suc (steps-respˡ ys≋xs ys↭zs)
+      steps-respˡ ys≋xs           (trans ys↭ws ws↭zs) = cong (_+ steps ws↭zs) (steps-respˡ ys≋xs ys↭ws)
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.1
+
+¬x∷xs↭[] = ¬x∷xs↭[]ʳ
+{-# WARNING_ON_USAGE ¬x∷xs↭[]
+"Warning: ¬x∷xs↭[] was deprecated in v2.1.
+Please use ¬x∷xs↭[]ʳ instead."
+#-}
+
+↭-singleton⁻¹ : Transitive R →
+                ∀ {xs x} → Permutation R xs [ x ] → ∃ λ y → xs ≡ [ y ] × R y x
+↭-singleton⁻¹ = ↭-singleton-invʳ
+{-# WARNING_ON_USAGE ↭-singleton⁻¹
+"Warning: ↭-singleton⁻¹ was deprecated in v2.1.
+Please use ↭-singleton-invʳ instead."
+#-}
+
diff --git a/src/Data/List/Relation/Binary/Permutation/Homogeneous/Properties/Core.agda b/src/Data/List/Relation/Binary/Permutation/Homogeneous/Properties/Core.agda
new file mode 100644
index 0000000000..764475c4ad
--- /dev/null
+++ b/src/Data/List/Relation/Binary/Permutation/Homogeneous/Properties/Core.agda
@@ -0,0 +1,242 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Core properties of the `Homogeneous` definition of permutation
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Core using (Rel; _⇒_; _Preserves_⟶_)
+
+module Data.List.Relation.Binary.Permutation.Homogeneous.Properties.Core
+  {a r} {A : Set a} {R : Rel A r} where
+
+open import Data.List.Base as List using (List; []; _∷_; [_]; _++_)
+open import Data.List.Relation.Binary.Pointwise as Pointwise
+  using (Pointwise; []; _∷_)
+open import Data.Product.Base using (_,_; _×_; ∃; ∃₂)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions
+  using (Reflexive; Symmetric; Transitive; LeftTrans; RightTrans)
+open import Relation.Binary.Structures using (IsEquivalence)
+
+open import Data.List.Relation.Binary.Permutation.Homogeneous public
+  using (Permutation; refl; prep; swap; trans)
+
+private
+  variable
+    xs ys zs : List A
+    x y z v w : A
+
+  _++[_]++_ = λ xs (z : A) ys → xs ++ [ z ] ++ ys
+
+_≋_ _↭_ : Rel (List A) _
+_≋_ = Pointwise R
+_↭_ = Permutation R
+
+
+------------------------------------------------------------------------
+-- Properties of _↭_ depending on suitable assumptions on R
+
+-- Constructor alias
+
+↭-pointwise : _≋_ ⇒ _↭_
+↭-pointwise = refl
+
+------------------------------------------------------------------------
+-- Reflexivity and its consequences
+
+module Reflexivity (R-refl : Reflexive R) where
+
+  ≋-refl : Reflexive _≋_
+  ≋-refl = Pointwise.refl R-refl
+
+  ↭-refl : Reflexive _↭_
+  ↭-refl = ↭-pointwise ≋-refl
+
+  ↭-prep : ∀ {x} {xs ys} → xs ↭ ys → (x ∷ xs) ↭ (x ∷ ys)
+  ↭-prep xs↭ys = prep R-refl xs↭ys
+
+  ↭-swap : ∀ x y {xs ys} → xs ↭ ys → (x ∷ y ∷ xs) ↭ (y ∷ x ∷ ys)
+  ↭-swap _ _ xs↭ys = swap R-refl R-refl xs↭ys
+
+  ↭-shift : ∀ {v w} → R v w → ∀ xs {ys zs} → ys ↭ zs →
+            (xs ++ v ∷ ys) ↭ (w ∷ xs ++ zs)
+  ↭-shift {v} {w} v≈w []       rel = prep v≈w rel
+  ↭-shift {v} {w} v≈w (x ∷ xs) rel
+    = trans (↭-prep (↭-shift v≈w xs rel)) (↭-swap x w ↭-refl)
+
+  shift : ∀ {v w} → R v w → ∀ xs {ys} → (xs ++[ v ]++ ys) ↭ (w ∷ xs ++ ys)
+  shift v≈w xs = ↭-shift v≈w xs ↭-refl
+
+  shift≈ : ∀ x xs {ys} → (xs ++[ x ]++ ys) ↭ (x ∷ xs ++ ys)
+  shift≈ x xs = shift R-refl xs
+
+------------------------------------------------------------------------
+-- Symmetry and its consequences
+
+module Symmetry (R-sym : Symmetric R) where
+
+  ≋-sym : Symmetric _≋_
+  ≋-sym = Pointwise.symmetric R-sym
+
+  ↭-sym : Symmetric _↭_
+  ↭-sym (refl xs∼ys)           = refl (≋-sym xs∼ys)
+  ↭-sym (prep x∼x′ xs↭ys)      = prep (R-sym x∼x′) (↭-sym xs↭ys)
+  ↭-sym (swap x∼x′ y∼y′ xs↭ys) = swap (R-sym y∼y′) (R-sym x∼x′) (↭-sym xs↭ys)
+  ↭-sym (trans xs↭ys ys↭zs)    = trans (↭-sym ys↭zs) (↭-sym xs↭ys)
+
+------------------------------------------------------------------------
+-- Transitivity and its consequences
+
+-- A smart version of trans that pushes `refl`s to the leaves (see #1113).
+
+module LRTransitivity
+       (↭-transˡ-≋ : LeftTrans _≋_ _↭_)
+       (↭-transʳ-≋ : RightTrans _↭_ _≋_)
+
+  where
+
+  ↭-trans : Transitive _↭_
+  ↭-trans (refl xs≋ys) ys↭zs = ↭-transˡ-≋ xs≋ys ys↭zs
+  ↭-trans xs↭ys (refl ys≋zs) = ↭-transʳ-≋ xs↭ys ys≋zs
+  ↭-trans xs↭ys ys↭zs        = trans xs↭ys ys↭zs
+
+------------------------------------------------------------------------
+-- Two important inversion properties of ↭, which *no longer*
+-- require `steps` or  well-founded induction... but which
+-- follow from ↭-transˡ-≋, ↭-transʳ-≋ and properties of R
+------------------------------------------------------------------------
+
+-- first inversion: split on a 'middle' element
+
+  module Split (R-refl : Reflexive R) (R-trans : Transitive R) where
+
+    private
+      ≋-trans : Transitive (Pointwise R)
+      ≋-trans = Pointwise.transitive R-trans
+
+      open Reflexivity R-refl using (≋-refl; ↭-refl; ↭-prep; ↭-swap)
+
+      helper : ∀ as bs {xs ys} (p : xs ↭ ys) →
+               ys ≋ (as ++[ v ]++ bs) →
+               ∃₂ λ ps qs → xs ≋ (ps ++[ v ]++ qs)
+                          × (ps ++ qs) ↭ (as ++ bs)
+      helper as           bs (trans xs↭ys ys↭zs) zs≋as++[v]++ys
+        with ps , qs , eq , ↭ ← helper as bs ys↭zs zs≋as++[v]++ys
+        with ps′ , qs′ , eq′ , ↭′ ← helper ps qs xs↭ys eq
+        = ps′ , qs′ , eq′ , ↭-trans ↭′ ↭
+      helper []           _  (refl (x≈v ∷ xs≋vs)) (v≈y ∷ vs≋ys)
+        = [] , _ , R-trans x≈v v≈y ∷ ≋-refl , refl (≋-trans xs≋vs vs≋ys)
+      helper (a ∷ as)     bs (refl (x≈v ∷ xs≋vs)) (v≈y ∷ vs≋ys)
+        = _ ∷ as , bs , R-trans x≈v v≈y ∷ ≋-trans xs≋vs vs≋ys , ↭-refl
+      helper []           bs (prep {xs = xs} x≈v xs↭vs) (v≈y ∷ vs≋ys)
+        = [] , xs , R-trans x≈v v≈y ∷ ≋-refl , ↭-transʳ-≋ xs↭vs vs≋ys
+      helper (a ∷ as)     bs (prep x≈v as↭vs) (v≈y ∷ vs≋ys)
+        with ps , qs , eq , ↭ ← helper as bs as↭vs vs≋ys
+        = a ∷ ps , qs , R-trans x≈v v≈y ∷ eq , prep R-refl ↭
+      helper []           [] (swap _ _ _) (_ ∷ ())
+      helper []      (b ∷ _) (swap x≈v y≈w xs↭vs) (w≈z ∷ v≈y ∷ vs≋ys)
+        = b ∷ [] , _ , R-trans x≈v v≈y ∷ R-trans y≈w w≈z ∷ ≋-refl
+                     , ↭-prep (↭-transʳ-≋ xs↭vs vs≋ys)
+      helper (a ∷ [])     bs (swap x≈v y≈w xs↭vs)  (w≈z ∷ v≈y ∷ vs≋ys)
+        = []     , a ∷ _ , R-trans x≈v v≈y ∷ R-trans y≈w w≈z ∷ ≋-refl
+                         , ↭-prep (↭-transʳ-≋ xs↭vs vs≋ys)
+      helper (a ∷ b ∷ as) bs (swap x≈v y≈w as↭vs) (w≈a ∷ v≈b ∷ vs≋ys)
+        with ps , qs , eq , ↭ ← helper as bs as↭vs vs≋ys
+        = b ∷ a ∷ ps , qs , R-trans x≈v v≈b ∷ R-trans y≈w w≈a ∷ eq
+                          , ↭-swap _ _ ↭
+
+    ↭-split : ∀ v as bs {xs} → xs ↭ (as ++[ v ]++ bs) →
+              ∃₂ λ ps qs → xs ≋ (ps ++[ v ]++ qs)
+                         × (ps ++ qs) ↭ (as ++ bs)
+    ↭-split v as bs p = helper as bs p ≋-refl
+
+
+-- second inversion: using ↭-split, drop the middle element
+
+  module DropMiddle (R-≈ : IsEquivalence R) where
+
+    private
+      module ≈ = IsEquivalence R-≈
+      open Reflexivity ≈.refl using (shift)
+      open Symmetry ≈.sym using (↭-sym)
+      open Split ≈.refl ≈.trans
+
+    dropMiddleElement-≋ : ∀ {x} ws xs {ys} {zs} →
+                          (ws ++[ x ]++ ys) ≋ (xs ++[ x ]++ zs) →
+                          (ws ++ ys) ↭ (xs ++ zs)
+    dropMiddleElement-≋ []       []       (_   ∷ eq)
+      = ↭-pointwise eq
+    dropMiddleElement-≋ []       (x ∷ xs) (w≈v ∷ eq)
+      = ↭-transˡ-≋ eq (shift w≈v xs)
+    dropMiddleElement-≋ (w ∷ ws) []       (w≈x ∷ eq)
+      = ↭-transʳ-≋ (↭-sym (shift (≈.sym w≈x) ws)) eq
+    dropMiddleElement-≋ (w ∷ ws) (x ∷ xs) (w≈x ∷ eq)
+      = prep w≈x (dropMiddleElement-≋ ws xs eq)
+
+    dropMiddleElement : ∀ {x} ws xs {ys zs} →
+                        (ws ++[ x ]++ ys) ↭ (xs ++[ x ]++ zs) →
+                        (ws ++ ys) ↭ (xs ++ zs)
+    dropMiddleElement {x} ws xs {ys} {zs} p
+      with ps , qs , eq , ↭ ← ↭-split x xs zs p
+      = ↭-trans (dropMiddleElement-≋ ws ps eq) ↭
+
+    syntax dropMiddleElement-≋ ws xs ws++x∷ys≋xs++x∷zs
+      = ws ++≋[ ws++x∷ys≋xs++x∷zs ]++ xs
+
+    syntax dropMiddleElement ws xs ws++x∷ys↭xs++x∷zs
+      = ws ++↭[ ws++x∷ys↭xs++x∷zs ]++ xs
+
+
+------------------------------------------------------------------------
+-- Now: Left and Right Transitivity hold outright!
+
+module Transitivity (R-trans : Transitive R) where
+
+  private
+    ≋-trans : Transitive _≋_
+    ≋-trans = Pointwise.transitive R-trans
+
+  ↭-transˡ-≋ : LeftTrans _≋_ _↭_
+  ↭-transˡ-≋ xs≋ys               (refl ys≋zs)
+    = refl (≋-trans xs≋ys ys≋zs)
+  ↭-transˡ-≋ (x≈y ∷ xs≋ys)       (prep y≈z ys↭zs)
+    = prep (R-trans x≈y y≈z) (↭-transˡ-≋ xs≋ys ys↭zs)
+  ↭-transˡ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ ys↭zs)
+    = swap (R-trans x≈y eq₁) (R-trans w≈z eq₂) (↭-transˡ-≋ xs≋ys ys↭zs)
+  ↭-transˡ-≋ xs≋ys               (trans ys↭ws ws↭zs)
+    = trans (↭-transˡ-≋ xs≋ys ys↭ws) ws↭zs
+
+  ↭-transʳ-≋ : RightTrans _↭_ _≋_
+  ↭-transʳ-≋ (refl xs≋ys)         ys≋zs
+    = refl (≋-trans xs≋ys ys≋zs)
+  ↭-transʳ-≋ (prep x≈y xs↭ys)     (y≈z ∷ ys≋zs)
+    = prep (R-trans x≈y y≈z) (↭-transʳ-≋ xs↭ys ys≋zs)
+  ↭-transʳ-≋ (swap eq₁ eq₂ xs↭ys) (x≈w ∷ y≈z ∷ ys≋zs)
+    = swap (R-trans eq₁ y≈z) (R-trans eq₂ x≈w) (↭-transʳ-≋ xs↭ys ys≋zs)
+  ↭-transʳ-≋ (trans xs↭ws ws↭ys)  ys≋zs
+    = trans xs↭ws (↭-transʳ-≋ ws↭ys ys≋zs)
+
+-- Transitivity proper
+
+  ↭-trans : Transitive _↭_
+  ↭-trans = LRTransitivity.↭-trans ↭-transˡ-≋ ↭-transʳ-≋
+
+
+------------------------------------------------------------------------
+-- Permutation is an equivalence (Setoid version)
+
+module _ (R-equiv : IsEquivalence R) where
+
+  private module ≈ = IsEquivalence R-equiv
+
+  isEquivalence : IsEquivalence _↭_
+  isEquivalence = record
+    { refl  = Reflexivity.↭-refl ≈.refl
+    ; sym   = Symmetry.↭-sym ≈.sym
+    ; trans = Transitivity.↭-trans ≈.trans
+    }
+
+  setoid : Setoid _ _
+  setoid = record { isEquivalence = isEquivalence }
diff --git a/src/Data/List/Relation/Binary/Permutation/Homogeneous/Properties/HigherDimensional.agda b/src/Data/List/Relation/Binary/Permutation/Homogeneous/Properties/HigherDimensional.agda
new file mode 100644
index 0000000000..ce4ef34b2f
--- /dev/null
+++ b/src/Data/List/Relation/Binary/Permutation/Homogeneous/Properties/HigherDimensional.agda
@@ -0,0 +1,107 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Higher-dimensional properties of the `Homogeneous` definition of permutation
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Relation.Binary.Permutation.Homogeneous.Properties.HigherDimensional where
+
+open import Data.List.Base as List using (List; []; _∷_)
+open import Data.List.Relation.Binary.Pointwise as Pointwise
+  using (Pointwise; []; _∷_)
+open import Data.List.Relation.Unary.Any as Any
+  using (Any; here; there)
+import Data.List.Relation.Unary.Any.Properties as Any
+open import Function.Base using (_∘_)
+open import Level using (Level; _⊔_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions
+  using (Symmetric; Transitive; _Respects_)
+open import Relation.Binary.PropositionalEquality.Core as ≡
+  using (_≡_ ; cong; cong₂)
+
+import Data.List.Relation.Binary.Permutation.Homogeneous.Properties.Core as Core
+import Data.List.Relation.Binary.Permutation.Homogeneous.Properties as Properties
+
+private
+  variable
+    a r : Level
+    A : Set a
+    x y : A
+    xs ys : List A
+
+------------------------------------------------------------------------
+-- Two higher-dimensional properties useful in the `Propositional` case,
+-- specifically in the equivalence proof between `Bag` equality and `_↭_`
+------------------------------------------------------------------------
+
+module _ {_≈_ : Rel A r} (≈-sym : Symmetric _≈_) where
+
+  open Core {R = _≈_} using (_≋_; _↭_; refl; prep; swap; trans; module Symmetry)
+  open Symmetry ≈-sym using (≋-sym; ↭-sym)
+
+-- involutive symmetry lifts
+
+  module _ (≈-sym-involutive : ∀ {x y} (p : x ≈ y) → ≈-sym (≈-sym p) ≡ p)
+    where
+
+    ↭-sym-involutive : (p : xs ↭ ys) → ↭-sym (↭-sym p) ≡ p
+    ↭-sym-involutive (refl xs≋ys) = cong refl (≋-sym-involutive xs≋ys)
+      where
+      ≋-sym-involutive : (p : xs ≋ ys) → ≋-sym (≋-sym p) ≡ p
+      ≋-sym-involutive [] = ≡.refl
+      ≋-sym-involutive (x≈y ∷ xs≋ys) rewrite ≈-sym-involutive x≈y
+        = cong (_ ∷_) (≋-sym-involutive xs≋ys)
+    ↭-sym-involutive (prep eq p) = cong₂ prep (≈-sym-involutive eq) (↭-sym-involutive p)
+    ↭-sym-involutive (swap eq₁ eq₂ p) rewrite ≈-sym-involutive eq₁ | ≈-sym-involutive eq₂
+      = cong (swap _ _) (↭-sym-involutive p)
+    ↭-sym-involutive (trans p q) = cong₂ trans (↭-sym-involutive p) (↭-sym-involutive q)
+
+    module _ (≈-trans : Transitive _≈_) where
+
+      private
+        ∈-resp-Pointwise : (Any (x ≈_)) Respects  _≋_
+        ∈-resp-Pointwise = Properties.∈-resp-Pointwise ≈-trans
+
+        ∈-resp-↭ : (Any (x ≈_)) Respects _↭_
+        ∈-resp-↭ = Properties.∈-resp-↭ ≈-trans
+
+-- invertible symmetry lifts to equality on proofs of membership
+
+      module _ (≈-trans-trans-sym : ∀ {x y z} (p : x ≈ y) (q : y ≈ z) →
+                                    ≈-trans (≈-trans p q) (≈-sym q) ≡ p) where
+
+        ∈-resp-Pointwise-sym : (p : xs ≋ ys) {ix : Any (x ≈_) xs} →
+                               ∈-resp-Pointwise (≋-sym p) (∈-resp-Pointwise p ix) ≡ ix
+        ∈-resp-Pointwise-sym (x≈y ∷ xs≋ys) {here ix}
+          = cong here (≈-trans-trans-sym ix x≈y)
+        ∈-resp-Pointwise-sym (x≈y ∷ xs≋ys) {there ixs}
+          = cong there (∈-resp-Pointwise-sym xs≋ys)
+
+        ∈-resp-↭-sym′   : (p : ys ↭ xs) {iy : Any (x ≈_) ys} {ix : Any (x ≈_) xs} →
+                           ix ≡ ∈-resp-↭ p iy → ∈-resp-↭ (↭-sym p) ix ≡ iy
+        ∈-resp-↭-sym′ (refl xs≋ys) ≡.refl = ∈-resp-Pointwise-sym xs≋ys
+        ∈-resp-↭-sym′ (prep eq₁ p) {here iy} {here ix} eq
+          with ≡.refl ← eq = cong here (≈-trans-trans-sym iy eq₁)
+        ∈-resp-↭-sym′ (prep eq₁ p) {there iys} {there ixs} eq
+          with ≡.refl ← eq = cong there (∈-resp-↭-sym′ p ≡.refl)
+        ∈-resp-↭-sym′ (swap eq₁ eq₂ p) {here ix} {here iy} ()
+        ∈-resp-↭-sym′ (swap eq₁ eq₂ p) {here ix} {there iys} eq
+          with ≡.refl ← eq = cong here (≈-trans-trans-sym ix eq₁)
+        ∈-resp-↭-sym′ (swap eq₁ eq₂ p) {there (here ix)} {there (here iy)} ()
+        ∈-resp-↭-sym′ (swap eq₁ eq₂ p) {there (here ix)} {here iy} eq
+          with ≡.refl ← eq = cong (there ∘ here) (≈-trans-trans-sym ix eq₂)
+        ∈-resp-↭-sym′ (swap eq₁ eq₂ p) {there (there ixs)} {there (there iys)} eq
+          with ≡.refl ← eq = cong (there ∘ there) (∈-resp-↭-sym′ p ≡.refl)
+        ∈-resp-↭-sym′ (trans p₁ p₂) eq = ∈-resp-↭-sym′ p₁ (∈-resp-↭-sym′ p₂ eq)
+
+        ∈-resp-↭-sym : (p : xs ↭ ys) {ix : Any (x ≈_) xs} →
+                       ∈-resp-↭ (↭-sym p) (∈-resp-↭ p ix) ≡ ix
+        ∈-resp-↭-sym p = ∈-resp-↭-sym′ p ≡.refl
+
+        ∈-resp-↭-sym⁻¹ : (p : xs ↭ ys) {iy : Any (x ≈_) ys} →
+                         ∈-resp-↭ p (∈-resp-↭ (↭-sym p) iy) ≡ iy
+        ∈-resp-↭-sym⁻¹ p with eq′ ← ∈-resp-↭-sym′ (↭-sym p)
+                         rewrite ↭-sym-involutive p = eq′ ≡.refl
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional.agda b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
index c41793d28a..a2e12f1409 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
@@ -10,91 +10,65 @@ module Data.List.Relation.Binary.Permutation.Propositional
   {a} {A : Set a} where
 
 open import Data.List.Base using (List; []; _∷_)
+open import Data.List.Relation.Binary.Equality.Propositional using (_≋_; ≋⇒≡)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence)
-open import Relation.Binary.Definitions using (Reflexive; Transitive)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
-import Relation.Binary.Reasoning.Setoid as EqReasoning
-open import Relation.Binary.Reasoning.Syntax
+open import Relation.Binary.Definitions
+  using (Reflexive; Transitive; LeftTrans; RightTrans)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; setoid)
+
+import Data.List.Relation.Binary.Permutation.Setoid as Permutation
+import Data.List.Relation.Binary.Permutation.Homogeneous.Properties.Core as Core
 
 ------------------------------------------------------------------------
--- An inductive definition of permutation
+-- Definition of permutation
 
--- Note that one would expect that this would be defined in terms of
--- `Permutation.Setoid`. This is not currently the case as it involves
--- adding in a bunch of trivial `_≡_` proofs to the constructors which
--- a) adds noise and b) prevents easy access to the variables `x`, `y`.
--- This may be changed in future when a better solution is found.
+private
+  module ↭ = Permutation (setoid A)
 
-infix 3 _↭_
+-- Note that this is now defined in terms of `Permutation.Setoid` (#2317)
 
-data _↭_ : Rel (List A) a where
-  refl  : ∀ {xs}        → xs ↭ xs
-  prep  : ∀ {xs ys} x   → xs ↭ ys → x ∷ xs ↭ x ∷ ys
-  swap  : ∀ {xs ys} x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
-  trans : ∀ {xs ys zs}  → xs ↭ ys → ys ↭ zs → xs ↭ zs
+open ↭ public
+  hiding ( ↭-reflexive; ↭-pointwise; ↭-trans; ↭-isEquivalence
+         ; module PermutationReasoning; ↭-setoid
+         )
 
 ------------------------------------------------------------------------
 -- _↭_ is an equivalence
 
 ↭-reflexive : _≡_ ⇒ _↭_
-↭-reflexive refl = refl
-
-↭-refl : Reflexive _↭_
-↭-refl = refl
+↭-reflexive refl = ↭-refl
 
-↭-sym : ∀ {xs ys} → xs ↭ ys → ys ↭ xs
-↭-sym refl                = refl
-↭-sym (prep x xs↭ys)      = prep x (↭-sym xs↭ys)
-↭-sym (swap x y xs↭ys)    = swap y x (↭-sym xs↭ys)
-↭-sym (trans xs↭ys ys↭zs) = trans (↭-sym ys↭zs) (↭-sym xs↭ys)
+↭-pointwise : _≋_ ⇒ _↭_
+↭-pointwise xs≋ys = ↭-reflexive (≋⇒≡ xs≋ys)
 
 -- A smart version of trans that avoids unnecessary `refl`s (see #1113).
+↭-transˡ-≋ : LeftTrans _≋_ _↭_
+↭-transˡ-≋ xs≋ys ys↭zs with refl ← ≋⇒≡ xs≋ys = ys↭zs
+
+↭-transʳ-≋ : RightTrans _↭_ _≋_
+↭-transʳ-≋ xs↭ys ys≋zs with refl ← ≋⇒≡ ys≋zs = xs↭ys
+
 ↭-trans : Transitive _↭_
-↭-trans refl ρ₂ = ρ₂
-↭-trans ρ₁ refl = ρ₁
-↭-trans ρ₁ ρ₂   = trans ρ₁ ρ₂
+↭-trans = Core.LRTransitivity.↭-trans ↭-transˡ-≋ ↭-transʳ-≋
 
 ↭-isEquivalence : IsEquivalence _↭_
 ↭-isEquivalence = record
-  { refl  = refl
+  { refl  = ↭-refl
   ; sym   = ↭-sym
   ; trans = ↭-trans
   }
 
-↭-setoid : Setoid _ _
-↭-setoid = record
-  { isEquivalence = ↭-isEquivalence
-  }
-
 ------------------------------------------------------------------------
 -- A reasoning API to chain permutation proofs and allow "zooming in"
--- to localised reasoning.
-
-module PermutationReasoning where
+-- to localised reasoning. For details of the axiomatisation, and
+-- in particular the refactored dependencies,
+-- see `Data.List.Relation.Binary.Permutation.Setoid.↭-Reasoning`. 
 
-  private module Base = EqReasoning ↭-setoid
+module PermutationReasoning = ↭-Reasoning ↭-isEquivalence ↭-pointwise
 
-  open Base public
-    hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨)
-    renaming (≈-go to ↭-go)
-
-  open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public
-
-  -- Some extra combinators that allow us to skip certain elements
-
-  infixr 2 step-swap step-prep
-
-  -- Skip reasoning on the first element
-  step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs →
-              xs ↭ ys → (x ∷ xs) IsRelatedTo zs
-  step-prep x xs rel xs↭ys = relTo (trans (prep x xs↭ys) (begin rel))
-
-  -- Skip reasoning about the first two elements
-  step-swap : ∀ x y xs {ys zs : List A} → (y ∷ x ∷ ys) IsRelatedTo zs →
-              xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs
-  step-swap x y xs rel xs↭ys = relTo (trans (swap x y xs↭ys) (begin rel))
+------------------------------------------------------------------------
+-- Bundle export
 
-  syntax step-prep x xs y↭z x↭y = x ∷ xs <⟨ x↭y ⟩ y↭z
-  syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z
+open PermutationReasoning public using (↭-setoid)
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index 781de1cc36..efce2cd07b 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -1,190 +1,149 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Properties of permutation
+-- Properties of permutation in the Propositional case
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-module Data.List.Relation.Binary.Permutation.Propositional.Properties where
+module Data.List.Relation.Binary.Permutation.Propositional.Properties {a} {A : Set a} where
 
 open import Algebra.Bundles
 open import Algebra.Definitions
 open import Algebra.Structures
 open import Data.Bool.Base using (Bool; true; false)
-open import Data.Nat using (suc)
 open import Data.Product.Base using (-,_; proj₂)
-open import Data.List.Base as List
-open import Data.List.Relation.Binary.Permutation.Propositional
-open import Data.List.Relation.Unary.Any using (Any; here; there)
-open import Data.List.Relation.Unary.All using (All; []; _∷_)
+open import Data.List.Base as List using (List; []; _∷_; [_]; _++_)
 open import Data.List.Membership.Propositional
 open import Data.List.Membership.Propositional.Properties
-import Data.List.Properties as Lₚ
+import Data.List.Properties as List
+open import Data.List.Relation.Unary.All using (All; []; _∷_)
+open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.Product.Base using (_,_; _×_; ∃; ∃₂)
 open import Function.Base using (_∘_; _⟨_⟩_)
 open import Level using (Level)
-open import Relation.Unary using (Pred)
 open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_)
 open import Relation.Binary.Definitions using (_Respects_; Decidable)
-open import Relation.Binary.PropositionalEquality.Core as ≡
-  using (_≡_ ; refl ; cong; cong₂; _≢_)
+open import Relation.Binary.PropositionalEquality as ≡
+  using (_≡_ ; refl ; cong; setoid)
 open import Relation.Nullary
+open import Relation.Unary using (Pred)
 
-open PermutationReasoning
+import Data.List.Relation.Binary.Permutation.Propositional as Propositional
+import Data.List.Relation.Binary.Permutation.Setoid.Properties as Permutation
 
 private
   variable
-    a b p : Level
-    A : Set a
+    b p r : Level
     B : Set b
+    v x y z : A
+    ws xs ys zs : List A
+    vs : List B
+    P : Pred A p
+    R : Rel A r
 
-------------------------------------------------------------------------
--- Permutations of empty and singleton lists
-
-↭-empty-inv : ∀ {xs : List A} → xs ↭ [] → xs ≡ []
-↭-empty-inv refl = refl
-↭-empty-inv (trans p q) with refl ← ↭-empty-inv q = ↭-empty-inv p
+  module ↭ = Permutation (setoid A)
 
-¬x∷xs↭[] : ∀ {x} {xs : List A} → ¬ ((x ∷ xs) ↭ [])
-¬x∷xs↭[] (trans s₁ s₂) with ↭-empty-inv s₂
-... | refl = ¬x∷xs↭[] s₁
-
-↭-singleton-inv : ∀ {x} {xs : List A} → xs ↭ [ x ] → xs ≡ [ x ]
-↭-singleton-inv refl                                             = refl
-↭-singleton-inv (prep _ ρ) with refl ← ↭-empty-inv ρ             = refl
-↭-singleton-inv (trans ρ₁ ρ₂) with refl ← ↭-singleton-inv ρ₂ = ↭-singleton-inv ρ₁
 
 ------------------------------------------------------------------------
--- sym
+-- Export all Setoid lemmas which hold unchanged in the case _≈_ = _≡_
+------------------------------------------------------------------------
 
-↭-sym-involutive : ∀ {xs ys : List A} (p : xs ↭ ys) → ↭-sym (↭-sym p) ≡ p
-↭-sym-involutive refl          = refl
-↭-sym-involutive (prep x ↭)    = cong (prep x) (↭-sym-involutive ↭)
-↭-sym-involutive (swap x y ↭)  = cong (swap x y) (↭-sym-involutive ↭)
-↭-sym-involutive (trans ↭₁ ↭₂) =
-  cong₂ trans (↭-sym-involutive ↭₁) (↭-sym-involutive ↭₂)
+open Propositional {A = A} public
+open ↭ public
+-- POSSIBLE DEPRECATION: legacy variations in naming
+  renaming (dropMiddleElement-≋ to drop-mid-≡; dropMiddleElement to drop-mid)
+-- DEPRECATION: legacy variation in implicit/explicit parametrisation
+  hiding (shift)
+-- more efficient versions defined in `Propositional`
+  hiding (↭-transˡ-≋; ↭-transʳ-≋)
+-- needing to specialise to ≡, where `Respects` and `Preserves` etc. are trivial
+  hiding ( map⁺; All-resp-↭; Any-resp-↭; ∈-resp-↭; ↭-sym-involutive
+         ; ∈-resp-↭-sym⁻¹; ∈-resp-↭-sym)
 
 ------------------------------------------------------------------------
--- Relationships to other predicates
+-- Additional/specialised properties which hold in the case _≈_ = _≡_
+------------------------------------------------------------------------
 
-All-resp-↭ : ∀ {P : Pred A p} → (All P) Respects _↭_
-All-resp-↭ refl wit                     = wit
-All-resp-↭ (prep x p) (px ∷ wit)        = px ∷ All-resp-↭ p wit
-All-resp-↭ (swap x y p) (px ∷ py ∷ wit) = py ∷ px ∷ All-resp-↭ p wit
-All-resp-↭ (trans p₁ p₂) wit            = All-resp-↭ p₂ (All-resp-↭ p₁ wit)
-
-Any-resp-↭ : ∀ {P : Pred A p} → (Any P) Respects _↭_
-Any-resp-↭ refl         wit                 = wit
-Any-resp-↭ (prep x p)   (here px)           = here px
-Any-resp-↭ (prep x p)   (there wit)         = there (Any-resp-↭ p wit)
-Any-resp-↭ (swap x y p) (here px)           = there (here px)
-Any-resp-↭ (swap x y p) (there (here px))   = here px
-Any-resp-↭ (swap x y p) (there (there wit)) = there (there (Any-resp-↭ p wit))
-Any-resp-↭ (trans p p₁) wit                 = Any-resp-↭ p₁ (Any-resp-↭ p wit)
-
-∈-resp-↭ : ∀ {x : A} → (x ∈_) Respects _↭_
-∈-resp-↭ = Any-resp-↭
-
-Any-resp-[σ⁻¹∘σ] : {xs ys : List A} {P : Pred A p} →
-                   (σ : xs ↭ ys) →
-                   (ix : Any P xs) →
-                   Any-resp-↭ (trans σ (↭-sym σ)) ix ≡ ix
-Any-resp-[σ⁻¹∘σ] refl          ix               = refl
-Any-resp-[σ⁻¹∘σ] (prep _ _)    (here _)         = refl
-Any-resp-[σ⁻¹∘σ] (swap _ _ _)  (here _)         = refl
-Any-resp-[σ⁻¹∘σ] (swap _ _ _)  (there (here _)) = refl
-Any-resp-[σ⁻¹∘σ] (trans σ₁ σ₂) ix
-  rewrite Any-resp-[σ⁻¹∘σ] σ₂ (Any-resp-↭ σ₁ ix)
-  rewrite Any-resp-[σ⁻¹∘σ] σ₁ ix
-  = refl
-Any-resp-[σ⁻¹∘σ] (prep _ σ)    (there ix)
-  rewrite Any-resp-[σ⁻¹∘σ] σ ix
-  = refl
-Any-resp-[σ⁻¹∘σ] (swap _ _ σ)  (there (there ix))
-  rewrite Any-resp-[σ⁻¹∘σ] σ ix
-  = refl
-
-∈-resp-[σ⁻¹∘σ] : {xs ys : List A} {x : A} →
-                 (σ : xs ↭ ys) →
-                 (ix : x ∈ xs) →
-                 ∈-resp-↭ (trans σ (↭-sym σ)) ix ≡ ix
-∈-resp-[σ⁻¹∘σ] = Any-resp-[σ⁻¹∘σ]
+sym-involutive : (p : x ≡ y) → ≡.sym (≡.sym p) ≡ p
+sym-involutive refl = refl
+
+trans-trans-sym : (p : x ≡ y) (q : y ≡ z) → ≡.trans (≡.trans p q) (≡.sym q) ≡ p
+trans-trans-sym refl refl = refl
 
 ------------------------------------------------------------------------
--- map
+-- Permutations of singleton lists
 
-module _ (f : A → B) where
+↭-singleton-inv : xs ↭ [ x ] → xs ≡ [ x ]
+↭-singleton-inv ρ with _ , refl , refl ← ↭-singleton⁻¹ ρ = refl
 
-  map⁺ : ∀ {xs ys} → xs ↭ ys → map f xs ↭ map f ys
-  map⁺ refl          = refl
-  map⁺ (prep x p)    = prep _ (map⁺ p)
-  map⁺ (swap x y p)  = swap _ _ (map⁺ p)
-  map⁺ (trans p₁ p₂) = trans (map⁺ p₁) (map⁺ p₂)
+------------------------------------------------------------------------
+-- sym
 
-  -- permutations preserve 'being a mapped list'
-  ↭-map-inv : ∀ {xs ys} → map f xs ↭ ys → ∃ λ ys′ → ys ≡ map f ys′ × xs ↭ ys′
-  ↭-map-inv {[]}     ρ                                                  = -, ↭-empty-inv (↭-sym ρ) , ↭-refl
-  ↭-map-inv {x ∷ []} ρ                                                  = -, ↭-singleton-inv (↭-sym ρ) , ↭-refl
-  ↭-map-inv {_ ∷ _ ∷ _} refl                                            = -, refl , ↭-refl
-  ↭-map-inv {_ ∷ _ ∷ _} (prep _ ρ)    with _ , refl , ρ′ ← ↭-map-inv ρ  = -, refl , prep _ ρ′
-  ↭-map-inv {_ ∷ _ ∷ _} (swap _ _ ρ)  with _ , refl , ρ′ ← ↭-map-inv ρ  = -, refl , swap _ _ ρ′
-  ↭-map-inv {_ ∷ _ ∷ _} (trans ρ₁ ρ₂) with _ , refl , ρ₃ ← ↭-map-inv ρ₁
-                                      with _ , refl , ρ₄ ← ↭-map-inv ρ₂ = -, refl , trans ρ₃ ρ₄
+↭-sym-involutive : (p : xs ↭ ys) → ↭-sym (↭-sym p) ≡ p
+↭-sym-involutive = ↭.↭-sym-involutive sym-involutive
 
 ------------------------------------------------------------------------
--- length
+-- Relationships to other predicates
+------------------------------------------------------------------------
 
-↭-length : ∀ {xs ys : List A} → xs ↭ ys → length xs ≡ length ys
-↭-length refl            = refl
-↭-length (prep x lr)     = cong suc (↭-length lr)
-↭-length (swap x y lr)   = cong (suc ∘ suc) (↭-length lr)
-↭-length (trans lr₁ lr₂) = ≡.trans (↭-length lr₁) (↭-length lr₂)
+All-resp-↭ : (All P) Respects _↭_
+All-resp-↭ = ↭.All-resp-↭ (≡.resp _)
 
-------------------------------------------------------------------------
--- _++_
+Any-resp-↭ : (Any P) Respects _↭_
+Any-resp-↭ = ↭.Any-resp-↭ (≡.resp _)
+
+∈-resp-↭ : (x ∈_) Respects _↭_
+∈-resp-↭ = ↭.∈-resp-↭
 
-++⁺ˡ : ∀ xs {ys zs : List A} → ys ↭ zs → xs ++ ys ↭ xs ++ zs
-++⁺ˡ []       ys↭zs = ys↭zs
-++⁺ˡ (x ∷ xs) ys↭zs = prep x (++⁺ˡ xs ys↭zs)
+∈-resp-↭-sym⁻¹ : (p : xs ↭ ys) {iy : v ∈ ys} →
+                 ∈-resp-↭ p (∈-resp-↭ (↭-sym p) iy) ≡ iy
+∈-resp-↭-sym⁻¹ = ↭.∈-resp-↭-sym⁻¹ sym-involutive trans-trans-sym
 
-++⁺ʳ : ∀ {xs ys : List A} zs → xs ↭ ys → xs ++ zs ↭ ys ++ zs
-++⁺ʳ zs refl          = refl
-++⁺ʳ zs (prep x ↭)    = prep x (++⁺ʳ zs ↭)
-++⁺ʳ zs (swap x y ↭)  = swap x y (++⁺ʳ zs ↭)
-++⁺ʳ zs (trans ↭₁ ↭₂) = trans (++⁺ʳ zs ↭₁) (++⁺ʳ zs ↭₂)
+∈-resp-↭-sym : (p : xs ↭ ys) {ix : v ∈ xs} →
+               ∈-resp-↭ (↭-sym p) (∈-resp-↭ p ix) ≡ ix
+∈-resp-↭-sym = ↭.∈-resp-↭-sym sym-involutive trans-trans-sym
 
-++⁺ : _++_ {A = A} Preserves₂ _↭_ ⟶ _↭_ ⟶ _↭_
-++⁺ ws↭xs ys↭zs = trans (++⁺ʳ _ ws↭xs) (++⁺ˡ _ ys↭zs)
+------------------------------------------------------------------------
+-- map
 
--- Some useful lemmas
+module _  {B : Set b} (f : A → B) where
 
-zoom : ∀ h {t xs ys : List A} → xs ↭ ys → h ++ xs ++ t ↭ h ++ ys ++ t
-zoom h {t} = ++⁺ˡ h ∘ ++⁺ʳ t
+  open Propositional {A = B} using () renaming (_↭_ to _↭′_)
 
-inject : ∀  (v : A) {ws xs ys zs} → ws ↭ ys → xs ↭ zs →
-        ws ++ [ v ] ++ xs ↭ ys ++ [ v ] ++ zs
-inject v ws↭ys xs↭zs = trans (++⁺ˡ _ (prep v xs↭zs)) (++⁺ʳ _ ws↭ys)
+  map⁺ : xs ↭ ys → List.map f xs ↭′ List.map f ys
+  map⁺ = ↭.map⁺ (setoid B) (cong f)
+{-
+  -- permutations preserve 'being a mapped list'
+  ↭-map-inv : List.map f xs ↭′ vs → ∃ λ ys → vs ≡ List.map f ys × xs ↭ ys
+  ↭-map-inv {xs = []} f*xs↭vs
+    with ≡.refl ← ↭′.↭-[]-invˡ f*xs↭vs  = [] , ≡.refl , ↭-refl
+  ↭-map-inv {xs = x ∷ []} (Properties.refl f*xs≋vs) = {!f*xs≋vs!}
+  ↭-map-inv {xs = x ∷ []} (Properties.prep eq p) = {!!}
+  ↭-map-inv {xs = x ∷ []} (Properties.trans p p₁) = {!!}
+  ↭-map-inv {xs = x ∷ y ∷ xs} (Properties.refl x₁) = {!!}
+  ↭-map-inv {xs = x ∷ y ∷ xs} (Properties.prep eq p) = {!!}
+  ↭-map-inv {xs = x ∷ y ∷ xs} (Properties.swap eq₁ eq₂ p) = {!!}
+  ↭-map-inv {xs = x ∷ y ∷ xs} (Properties.trans p p₁) = {!!}
+-}
 
-shift : ∀ v (xs ys : List A) → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
-shift v []       ys = refl
-shift v (x ∷ xs) ys = begin
-  x ∷ (xs ++ [ v ] ++ ys) <⟨ shift v xs ys ⟩
-  x ∷ v ∷ xs ++ ys        <<⟨ refl ⟩
-  v ∷ x ∷ xs ++ ys        ∎
+------------------------------------------------------------------------
+-- Some other useful lemmas, optimised for the Propositional case
+{- not sure we need these for their proofs? so renamed on import above
 
-drop-mid-≡ : ∀ {x : A} ws xs {ys} {zs} →
-             ws ++ [ x ] ++ ys ≡ xs ++ [ x ] ++ zs →
+drop-mid-≡ : ∀ {v : A} ws xs {ys} {zs} →
+             ws ++ [ x ] ++ ys ≡ xs ++ [ v ] ++ zs →
              ws ++ ys ↭ xs ++ zs
-drop-mid-≡ []       []       eq   with cong tail eq
-drop-mid-≡ []       []       eq   | refl = refl
-drop-mid-≡ []       (x ∷ xs) refl = shift _ xs _
-drop-mid-≡ (w ∷ ws) []       refl = ↭-sym (shift _ ws _)
-drop-mid-≡ (w ∷ ws) (x ∷ xs) eq with Lₚ.∷-injective eq
-... | refl , eq′ = prep w (drop-mid-≡ ws xs eq′)
-
-drop-mid : ∀ {x : A} ws xs {ys zs} →
-           ws ++ [ x ] ++ ys ↭ xs ++ [ x ] ++ zs →
+drop-mid-≡ []       []       ys≡zs
+  with refl ← cong List.tail ys≡zs = refl
+drop-mid-≡ []       (x ∷ xs) refl  = ↭-shift xs
+drop-mid-≡ (w ∷ ws) []       refl  = ↭-sym (↭-shift ws)
+drop-mid-≡ (w ∷ ws) (x ∷ xs) w∷ws[v]ys≡x∷xs[v]zs
+  with refl , ws[v]ys≡xs[v]zs ← List.∷-injective eq
+  = prep w (drop-mid-≡ ws xs ws[v]ys≡xs[v]zs)
+
+drop-mid : ∀ {v : A} ws xs {ys zs} →
+           ws ++ [ v ] ++ ys ↭ xs ++ [ v ] ++ zs →
            ws ++ ys ↭ xs ++ zs
 drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs refl refl
   where
@@ -194,8 +153,7 @@ drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs refl refl
               xs ++ [ x ] ++ zs ≡ l″ →
               ws ++ ys ↭ xs ++ zs
   drop-mid′ refl         ws           xs           refl eq   = drop-mid-≡ ws xs (≡.sym eq)
-  drop-mid′ (prep x p)   []           []           refl eq   with cong tail eq
-  drop-mid′ (prep x p)   []           []           refl eq   | refl = p
+  drop-mid′ (prep x p)   []           []           refl eq   with refl ← cong tail eq = p
   drop-mid′ (prep x p)   []           (x ∷ xs)     refl refl = trans p (shift _ _ _)
   drop-mid′ (prep x p)   (w ∷ ws)     []           refl refl = trans (↭-sym (shift _ _ _)) p
   drop-mid′ (prep x p)   (w ∷ ws)     (x ∷ xs)     refl refl = prep _ (drop-mid′ p ws xs refl refl)
@@ -218,138 +176,34 @@ drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs refl refl
       _ ∷ _ ∷ xs ++ _   ∎
   drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ [])     refl refl = begin
       _ ∷ _ ∷ ws ++ _   <<⟨ refl ⟩
+-- *** NB the next step can't be replaced with <⟨ shift _ _ _ ⟨ for some reason? ***
       _ ∷ (_ ∷ ws ++ _) <⟨ ↭-sym (shift _ _ _) ⟩
+-- *** because of parsing problems for that use of the `Reasoning` combinators!? ***
       _ ∷ (ws ++ _ ∷ _) <⟨ p ⟩
       _ ∷ _             ∎
   drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ y ∷ xs) refl refl = swap y z (drop-mid′ p _ _ refl refl)
   drop-mid′ (trans p₁ p₂) ws  xs refl refl with ∈-∃++ (∈-resp-↭ p₁ (∈-insert ws))
   ... | (h , t , refl) = trans (drop-mid′ p₁ ws h refl refl) (drop-mid′ p₂ h xs refl refl)
-
--- Algebraic properties
-
-++-identityˡ : LeftIdentity {A = List A} _↭_ [] _++_
-++-identityˡ xs = refl
-
-++-identityʳ : RightIdentity {A = List A} _↭_ [] _++_
-++-identityʳ xs = ↭-reflexive (Lₚ.++-identityʳ xs)
-
-++-identity : Identity {A = List A} _↭_ [] _++_
-++-identity = ++-identityˡ , ++-identityʳ
-
-++-assoc : Associative {A = List A} _↭_ _++_
-++-assoc xs ys zs = ↭-reflexive (Lₚ.++-assoc xs ys zs)
-
-++-comm : Commutative {A = List A} _↭_ _++_
-++-comm []       ys = ↭-sym (++-identityʳ ys)
-++-comm (x ∷ xs) ys = begin
-  x ∷ xs ++ ys   <⟨ ++-comm xs ys ⟩
-  x ∷ ys ++ xs   ↭⟨ shift x ys xs ⟨
-  ys ++ (x ∷ xs) ∎
-
-++-isMagma : IsMagma {A = List A} _↭_ _++_
-++-isMagma = record
-  { isEquivalence = ↭-isEquivalence
-  ; ∙-cong        = ++⁺
-  }
-
-++-isSemigroup : IsSemigroup {A = List A} _↭_ _++_
-++-isSemigroup = record
-  { isMagma = ++-isMagma
-  ; assoc   = ++-assoc
-  }
-
-++-isMonoid : IsMonoid {A = List A} _↭_ _++_ []
-++-isMonoid = record
-  { isSemigroup = ++-isSemigroup
-  ; identity    = ++-identity
-  }
-
-++-isCommutativeMonoid : IsCommutativeMonoid {A = List A} _↭_ _++_ []
-++-isCommutativeMonoid = record
-  { isMonoid = ++-isMonoid
-  ; comm     = ++-comm
-  }
-
-module _ {a} {A : Set a} where
-
-  ++-magma : Magma _ _
-  ++-magma = record
-    { isMagma = ++-isMagma {A = A}
-    }
-
-  ++-semigroup : Semigroup a _
-  ++-semigroup = record
-    { isSemigroup = ++-isSemigroup {A = A}
-    }
-
-  ++-monoid : Monoid a _
-  ++-monoid = record
-    { isMonoid = ++-isMonoid {A = A}
-    }
-
-  ++-commutativeMonoid : CommutativeMonoid _ _
-  ++-commutativeMonoid = record
-    { isCommutativeMonoid = ++-isCommutativeMonoid {A = A}
-    }
-
--- Another useful lemma
-
-shifts : ∀ xs ys {zs : List A} → xs ++ ys ++ zs ↭ ys ++ xs ++ zs
-shifts xs ys {zs} = begin
-   xs ++ ys  ++ zs ↭⟨ ++-assoc xs ys zs ⟨
-  (xs ++ ys) ++ zs ↭⟨ ++⁺ʳ zs (++-comm xs ys) ⟩
-  (ys ++ xs) ++ zs ↭⟨ ++-assoc ys xs zs ⟩
-   ys ++ xs  ++ zs ∎
+-}
 
 ------------------------------------------------------------------------
--- _∷_
-
-drop-∷ : ∀ {x : A} {xs ys} → x ∷ xs ↭ x ∷ ys → xs ↭ ys
-drop-∷ = drop-mid [] []
-
-------------------------------------------------------------------------
--- _∷ʳ_
-
-∷↭∷ʳ : ∀ (x : A) xs → x ∷ xs ↭ xs ∷ʳ x
-∷↭∷ʳ x xs = ↭-sym (begin
-  xs ++ [ x ]   ↭⟨ shift x xs [] ⟩
-  x ∷ xs ++ []  ≡⟨ Lₚ.++-identityʳ _ ⟩
-  x ∷ xs        ∎)
-
-------------------------------------------------------------------------
--- ʳ++
-
-++↭ʳ++ : ∀ (xs ys : List A) → xs ++ ys ↭ xs ʳ++ ys
-++↭ʳ++ []       ys = ↭-refl
-++↭ʳ++ (x ∷ xs) ys = ↭-trans (↭-sym (shift x xs ys)) (++↭ʳ++ xs (x ∷ ys))
-
-------------------------------------------------------------------------
--- reverse
-
-↭-reverse : (xs : List A) → reverse xs ↭ xs
-↭-reverse [] = ↭-refl
-↭-reverse (x ∷ xs) = begin
-  reverse (x ∷ xs) ≡⟨ Lₚ.unfold-reverse x xs ⟩
-  reverse xs ∷ʳ x ↭⟨ ∷↭∷ʳ x (reverse xs) ⟨
-  x ∷ reverse xs   ↭⟨ prep x (↭-reverse xs) ⟩
-  x ∷ xs ∎
-  where open PermutationReasoning
-
+-- DEPRECATED NAMES
 ------------------------------------------------------------------------
--- merge
-
-module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where
-
-  merge-↭ : ∀ xs ys → merge R? xs ys ↭ xs ++ ys
-  merge-↭ []       []       = ↭-refl
-  merge-↭ []       (y ∷ ys) = ↭-refl
-  merge-↭ (x ∷ xs) []       = ↭-sym (++-identityʳ (x ∷ xs))
-  merge-↭ (x ∷ xs) (y ∷ ys)
-    with does (R? x y) | merge-↭ xs (y ∷ ys) | merge-↭ (x ∷ xs) ys
-  ... | true  | rec | _   = prep x rec
-  ... | false | _   | rec = begin
-    y ∷ merge R? (x ∷ xs) ys <⟨ rec ⟩
-    y ∷ x ∷ xs ++ ys         ↭⟨ shift y (x ∷ xs) ys ⟨
-    (x ∷ xs) ++ y ∷ ys       ≡⟨ Lₚ.++-assoc [ x ] xs (y ∷ ys) ⟨
-    x ∷ xs ++ y ∷ ys         ∎
-    where open PermutationReasoning
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.1
+
+↭-empty-inv = ↭-[]-invʳ
+{-# WARNING_ON_USAGE ↭-empty-inv
+"Warning: ↭-empty-inv was deprecated in v2.1.
+Please use ↭-[]-invʳ instead."
+#-}
+
+shift : ∀ v xs ys → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
+shift v xs ys = ↭-shift {v = v} xs {ys}
+{-# WARNING_ON_USAGE shift
+"Warning: shift was deprecated in v2.1.
+Please use ↭-shift instead. \\
+NB. Parametrisation has changed to make v and ys implicit."
+#-}
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
index 4409e78cc4..f4513a9bf8 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
@@ -5,13 +5,14 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --warn=noUserWarning #-} -- for deprecated function `steps`
 
 open import Function.Base using (_∘′_)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence)
 open import Relation.Binary.Definitions
-  using (Reflexive; Symmetric; Transitive)
+  using (Reflexive; Symmetric; Transitive; LeftTrans; RightTrans)
 open import Relation.Binary.Reasoning.Syntax
 
 module Data.List.Relation.Binary.Permutation.Setoid
@@ -19,83 +20,88 @@ module Data.List.Relation.Binary.Permutation.Setoid
 
 open import Data.List.Base using (List; _∷_)
 import Data.List.Relation.Binary.Permutation.Homogeneous as Homogeneous
-import Data.List.Relation.Binary.Pointwise.Properties as Pointwise using (refl)
+import Data.List.Relation.Binary.Permutation.Homogeneous.Properties.Core as Core
 open import Data.List.Relation.Binary.Equality.Setoid S
-open import Data.Nat.Base using (ℕ; zero; suc; _+_)
+open import Data.Nat.Base using (ℕ)
 open import Level using (_⊔_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
-private
-  module Eq = Setoid S
-open Eq using (_≈_) renaming (Carrier to A)
+open Setoid S
+  using (_≈_)
+  renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans)
 
 ------------------------------------------------------------------------
 -- Definition
 
-open Homogeneous public
-  using (refl; prep; swap; trans)
-
 infix 3 _↭_
 
 _↭_ : Rel (List A) (a ⊔ ℓ)
-_↭_ = Homogeneous.Permutation _≈_
+_↭_ = Core._↭_ {R = _≈_}
 
 ------------------------------------------------------------------------
--- Constructor aliases
+-- Smart constructor aliases
+
+-- These provide aliases for the `Homogeneous` smart constructors, in
+-- particular for `swap` and `prep` when the elements being swapped or
+-- prepended are *propositionally* equal
 
--- These provide aliases for `swap` and `prep` when the elements being
--- swapped or prepended are propositionally equal
+↭-pointwise : _≋_ ⇒ _↭_
+↭-pointwise = Core.↭-pointwise
 
 ↭-prep : ∀ x {xs ys} → xs ↭ ys → x ∷ xs ↭ x ∷ ys
-↭-prep x xs↭ys = prep Eq.refl xs↭ys
+↭-prep _ = Core.Reflexivity.↭-prep ≈-refl
 
 ↭-swap : ∀ x y {xs ys} → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
-↭-swap x y xs↭ys = swap Eq.refl Eq.refl xs↭ys
+↭-swap = Core.Reflexivity.↭-swap ≈-refl
+
+↭-trans′ : LeftTrans _≋_ _↭_ → RightTrans _↭_ _≋_ → Transitive _↭_
+↭-trans′ = Core.LRTransitivity.↭-trans
 
 ------------------------------------------------------------------------
--- Functions over permutations
+-- Functions over permutations (retained for legacy)
 
 steps : ∀ {xs ys} → xs ↭ ys → ℕ
-steps (refl _)            = 1
-steps (prep _ xs↭ys)      = suc (steps xs↭ys)
-steps (swap _ _ xs↭ys)    = suc (steps xs↭ys)
-steps (trans xs↭ys ys↭zs) = steps xs↭ys + steps ys↭zs
+steps = Homogeneous.steps
 
 ------------------------------------------------------------------------
 -- _↭_ is an equivalence
 
 ↭-reflexive : _≡_ ⇒ _↭_
-↭-reflexive refl = refl (Pointwise.refl Eq.refl)
+↭-reflexive refl = Core.Reflexivity.↭-refl ≈-refl
 
 ↭-refl : Reflexive _↭_
 ↭-refl = ↭-reflexive refl
 
 ↭-sym : Symmetric _↭_
-↭-sym = Homogeneous.sym Eq.sym
+↭-sym = Core.Symmetry.↭-sym ≈-sym
 
 ↭-trans : Transitive _↭_
-↭-trans = trans
+↭-trans = Core.Transitivity.↭-trans ≈-trans
 
 ↭-isEquivalence : IsEquivalence _↭_
-↭-isEquivalence = Homogeneous.isEquivalence Eq.refl Eq.sym
-
-↭-setoid : Setoid _ _
-↭-setoid = Homogeneous.setoid {R = _≈_} Eq.refl Eq.sym
+↭-isEquivalence = record { refl = ↭-refl ; sym = ↭-sym ; trans = ↭-trans }
 
 ------------------------------------------------------------------------
 -- A reasoning API to chain permutation proofs
 
-module PermutationReasoning where
+module ↭-Reasoning (↭-isEquivalence : IsEquivalence _↭_)
+                   (↭-pointwise : _≋_ ⇒ _↭_)
+                   where
+
+  ↭-setoid : Setoid _ _
+  ↭-setoid = record { isEquivalence = ↭-isEquivalence }
 
-  private module Base = ≈-Reasoning ↭-setoid
+  private
+    open IsEquivalence ↭-isEquivalence using () renaming (sym to ↭-sym′)
+    module Base = ≈-Reasoning ↭-setoid
 
   open Base public
     hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨)
     renaming (≈-go to ↭-go)
 
-  open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public
-  open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ refl) ≋-sym public
+  open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym′ public
+  open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ ↭-pointwise) ≋-sym public
 
   -- Some extra combinators that allow us to skip certain elements
 
@@ -104,12 +110,20 @@ module PermutationReasoning where
   -- Skip reasoning on the first element
   step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs →
               xs ↭ ys → (x ∷ xs) IsRelatedTo zs
-  step-prep x xs rel xs↭ys = relTo (trans (prep Eq.refl xs↭ys) (begin rel))
+  step-prep x xs rel xs↭ys = ↭-go (↭-prep x xs↭ys) rel
 
   -- Skip reasoning about the first two elements
   step-swap : ∀ x y xs {ys zs : List A} → (y ∷ x ∷ ys) IsRelatedTo zs →
               xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs
-  step-swap x y xs rel xs↭ys = relTo (trans (swap Eq.refl Eq.refl xs↭ys) (begin rel))
+  step-swap x y xs rel xs↭ys = ↭-go (↭-swap x y xs↭ys) rel
 
   syntax step-prep x xs y↭z x↭y = x ∷ xs <⟨ x↭y ⟩ y↭z
   syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z
+
+module PermutationReasoning = ↭-Reasoning ↭-isEquivalence ↭-pointwise
+
+------------------------------------------------------------------------
+-- Bundle export
+
+open PermutationReasoning public using (↭-setoid)
+
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index 3af753e826..7e3f9b3341 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -6,89 +6,75 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core
-  using (Rel; _⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Definitions as B hiding (Decidable)
 
 module Data.List.Relation.Binary.Permutation.Setoid.Properties
   {a ℓ} (S : Setoid a ℓ)
   where
 
 open import Algebra
-import Algebra.Properties.CommutativeMonoid as ACM
 open import Data.Bool.Base using (true; false)
-open import Data.List.Base as List hiding (head; tail)
+open import Data.List.Base
 open import Data.List.Relation.Binary.Pointwise as Pointwise
-  using (Pointwise; head; tail)
-import Data.List.Relation.Binary.Equality.Setoid as Equality
-import Data.List.Relation.Binary.Permutation.Setoid as Permutation
-open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
+  using (Pointwise)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 import Data.List.Relation.Unary.Unique.Setoid as Unique
 import Data.List.Membership.Setoid as Membership
-open import Data.List.Membership.Setoid.Properties using (∈-∃++; ∈-insert)
-import Data.List.Properties as Lₚ
+import Data.List.Properties as List
 open import Data.Nat hiding (_⊔_)
-open import Data.Nat.Induction
-open import Data.Nat.Properties
 open import Data.Product.Base using (_,_; _×_; ∃; ∃₂; proj₁; proj₂)
 open import Function.Base using (_∘_; _⟨_⟩_; flip)
 open import Level using (Level; _⊔_)
-open import Relation.Unary using (Pred; Decidable)
-import Relation.Binary.Reasoning.Setoid as RelSetoid
+open import Relation.Binary.Core
+  using (Rel; _⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
+open import Relation.Binary.Definitions as B hiding (Decidable)
 open import Relation.Binary.Properties.Setoid S using (≉-resp₂)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 open import Relation.Nullary.Decidable using (yes; no; does)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Negation using (¬_; contradiction)
+open import Relation.Unary using (Pred; Decidable)
 
-private
-  variable
-    b p r : Level
+import Data.List.Relation.Binary.Equality.Setoid as Equality
+import Data.List.Relation.Binary.Permutation.Setoid as Permutation
+import Data.List.Relation.Binary.Permutation.Homogeneous.Properties as Properties
+--import Data.List.Relation.Binary.Permutation.Homogeneous.Properties.Core as Core
 
-open Setoid S using (_≈_) renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans)
+open Setoid S
+  using (_≈_; isEquivalence)
+  renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans)
 open Permutation S
 open Membership S
 open Unique S using (Unique)
 open module ≋ = Equality S
-  using (_≋_; []; _∷_; ≋-refl; ≋-sym; ≋-trans; All-resp-≋; Any-resp-≋; AllPairs-resp-≋)
-open PermutationReasoning
+  using (_≋_; []; _∷_; ≋-refl; ≋-sym; ≋-trans)
+
+private
+  variable
+    b p r : Level
+    xs ys zs : List A
+    x y z v w : A
+    P : Pred A p
+    R : Rel A r
 
 ------------------------------------------------------------------------
 -- Relationships to other predicates
 ------------------------------------------------------------------------
 
-All-resp-↭ : ∀ {P : Pred A p} → P Respects _≈_ → (All P) Respects _↭_
-All-resp-↭ resp (refl xs≋ys)   pxs             = All-resp-≋ resp xs≋ys pxs
-All-resp-↭ resp (prep x≈y p)   (px ∷ pxs)      = resp x≈y px ∷ All-resp-↭ resp p pxs
-All-resp-↭ resp (swap ≈₁ ≈₂ p) (px ∷ py ∷ pxs) = resp ≈₂ py ∷ resp ≈₁ px ∷ All-resp-↭ resp p pxs
-All-resp-↭ resp (trans p₁ p₂)  pxs             = All-resp-↭ resp p₂ (All-resp-↭ resp p₁ pxs)
-
-Any-resp-↭ : ∀ {P : Pred A p} → P Respects _≈_ → (Any P) Respects _↭_
-Any-resp-↭ resp (refl xs≋ys) pxs                 = Any-resp-≋ resp xs≋ys pxs
-Any-resp-↭ resp (prep x≈y p) (here px)           = here (resp x≈y px)
-Any-resp-↭ resp (prep x≈y p) (there pxs)         = there (Any-resp-↭ resp p pxs)
-Any-resp-↭ resp (swap x y p) (here px)           = there (here (resp x px))
-Any-resp-↭ resp (swap x y p) (there (here px))   = here (resp y px)
-Any-resp-↭ resp (swap x y p) (there (there pxs)) = there (there (Any-resp-↭ resp p pxs))
-Any-resp-↭ resp (trans p₁ p₂) pxs                = Any-resp-↭ resp p₂ (Any-resp-↭ resp p₁ pxs)
-
-AllPairs-resp-↭ : ∀ {R : Rel A r} → Symmetric R → R Respects₂ _≈_ → (AllPairs R) Respects _↭_
-AllPairs-resp-↭ sym resp (refl xs≋ys)     pxs             = AllPairs-resp-≋ resp xs≋ys pxs
-AllPairs-resp-↭ sym resp (prep x≈y p)     (∼ ∷ pxs)       =
-  All-resp-↭ (proj₁ resp) p (All.map (proj₂ resp x≈y) ∼) ∷
-  AllPairs-resp-↭ sym resp p pxs
-AllPairs-resp-↭ sym resp@(rʳ , rˡ) (swap eq₁ eq₂ p) ((∼₁ ∷ ∼₂) ∷ ∼₃ ∷ pxs) =
-  (sym (rʳ eq₂ (rˡ eq₁ ∼₁)) ∷ All-resp-↭ rʳ p (All.map (rˡ eq₂) ∼₃)) ∷
-  All-resp-↭ rʳ p (All.map (rˡ eq₁) ∼₂) ∷
-  AllPairs-resp-↭ sym resp p pxs
-AllPairs-resp-↭ sym resp (trans p₁ p₂)    pxs             =
-  AllPairs-resp-↭ sym resp p₂ (AllPairs-resp-↭ sym resp p₁ pxs)
-
-∈-resp-↭ : ∀ {x} → (x ∈_) Respects _↭_
-∈-resp-↭ = Any-resp-↭ (flip ≈-trans)
+All-resp-↭ : P Respects _≈_ → (All P) Respects _↭_
+All-resp-↭ = Properties.All-resp-↭
+
+Any-resp-↭ : P Respects _≈_ → (Any P) Respects _↭_
+Any-resp-↭ = Properties.Any-resp-↭
+
+AllPairs-resp-↭ : Symmetric R → R Respects₂ _≈_ → (AllPairs R) Respects _↭_
+AllPairs-resp-↭ = Properties.AllPairs-resp-↭
+
+∈-resp-↭ : (x ∈_) Respects _↭_
+∈-resp-↭ = Properties.∈-resp-↭ ≈-trans
 
 Unique-resp-↭ : Unique Respects _↭_
 Unique-resp-↭ = AllPairs-resp-↭ (_∘ ≈-sym) ≉-resp₂
@@ -98,89 +84,111 @@ Unique-resp-↭ = AllPairs-resp-↭ (_∘ ≈-sym) ≉-resp₂
 ------------------------------------------------------------------------
 
 ≋⇒↭ : _≋_ ⇒ _↭_
-≋⇒↭ = refl
+≋⇒↭ = ↭-pointwise
 
 ↭-respʳ-≋ : _↭_ Respectsʳ _≋_
-↭-respʳ-≋ xs≋ys               (refl zs≋xs)         = refl (≋-trans zs≋xs xs≋ys)
-↭-respʳ-≋ (x≈y ∷ xs≋ys)       (prep eq zs↭xs)      = prep (≈-trans eq x≈y) (↭-respʳ-≋ xs≋ys zs↭xs)
-↭-respʳ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ zs↭xs) = swap (≈-trans eq₁ w≈z) (≈-trans eq₂ x≈y) (↭-respʳ-≋ xs≋ys zs↭xs)
-↭-respʳ-≋ xs≋ys               (trans ws↭zs zs↭xs)  = trans ws↭zs (↭-respʳ-≋ xs≋ys zs↭xs)
+↭-respʳ-≋ = Properties.Steps.↭-respʳ-≋ ≈-trans
 
 ↭-respˡ-≋ : _↭_ Respectsˡ _≋_
-↭-respˡ-≋ xs≋ys               (refl ys≋zs)         = refl (≋-trans (≋-sym xs≋ys) ys≋zs)
-↭-respˡ-≋ (x≈y ∷ xs≋ys)       (prep eq zs↭xs)      = prep (≈-trans (≈-sym x≈y) eq) (↭-respˡ-≋ xs≋ys zs↭xs)
-↭-respˡ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ zs↭xs) = swap (≈-trans (≈-sym x≈y) eq₁) (≈-trans (≈-sym w≈z) eq₂) (↭-respˡ-≋ xs≋ys zs↭xs)
-↭-respˡ-≋ xs≋ys               (trans ws↭zs zs↭xs)  = trans (↭-respˡ-≋ xs≋ys ws↭zs) zs↭xs
+↭-respˡ-≋ = Properties.Steps.↭-respˡ-≋ ≈-trans ≈-sym
+
+↭-transˡ-≋ : LeftTrans _≋_ _↭_
+↭-transˡ-≋ = Properties.Transitivity.↭-transˡ-≋ ≈-trans
 
+↭-transʳ-≋ : RightTrans _↭_ _≋_
+↭-transʳ-≋ = Properties.Transitivity.↭-transʳ-≋ ≈-trans
+{-
+module _ (≈-sym-involutive : ∀ {x y} → (p : x ≈ y) → ≈-sym (≈-sym p) ≡ p)
+
+  where
+
+  ↭-sym-involutive : (p : xs ↭ ys) → ↭-sym (↭-sym p) ≡ p
+  ↭-sym-involutive = Properties.↭-sym-involutive′ ≈-trans ≈-sym ≈-sym-involutive
+
+  module _ (≈-trans-trans-sym : ∀ {x y z} (p : x ≈ y) (q : y ≈ z) →
+                                ≈-trans (≈-trans p q) (≈-sym q) ≡ p)
+    where
+
+    ∈-resp-↭-sym⁻¹ : ∀ (p : xs ↭ ys) {iy : x ∈ ys} →
+                     ∈-resp-↭ p (∈-resp-↭ (↭-sym p) iy) ≡ iy
+    ∈-resp-↭-sym⁻¹ = Properties.∈-resp-↭-sym⁻¹
+      ≈-trans ≈-sym ≈-sym-involutive ≈-trans-trans-sym
+    ∈-resp-↭-sym   : (p : xs ↭ ys) {ix : v ∈ xs} →
+                     ∈-resp-↭ (↭-sym p) (∈-resp-↭ p ix) ≡ ix
+    ∈-resp-↭-sym   = Properties.∈-resp-↭-sym
+      ≈-trans ≈-sym ≈-sym-involutive ≈-trans-trans-sym
+-}
 ------------------------------------------------------------------------
--- Properties of steps
+-- Properties of steps (legacy)
 ------------------------------------------------------------------------
+{-
+0<steps : (xs↭ys : xs ↭ ys) → 0 < steps xs↭ys
+0<steps = Properties.Steps.0<steps
 
-0<steps : ∀ {xs ys} (xs↭ys : xs ↭ ys) → 0 < steps xs↭ys
-0<steps (refl _)             = z<s
-0<steps (prep eq xs↭ys)      = m<n⇒m<1+n (0<steps xs↭ys)
-0<steps (swap eq₁ eq₂ xs↭ys) = m<n⇒m<1+n (0<steps xs↭ys)
-0<steps (trans xs↭ys xs↭ys₁) =
-  <-≤-trans (0<steps xs↭ys) (m≤m+n (steps xs↭ys) (steps xs↭ys₁))
-
-steps-respˡ : ∀ {xs ys zs} (ys≋xs : ys ≋ xs) (ys↭zs : ys ↭ zs) →
+steps-respˡ : (ys≋xs : ys ≋ xs) (ys↭zs : ys ↭ zs) →
               steps (↭-respˡ-≋ ys≋xs ys↭zs) ≡ steps ys↭zs
-steps-respˡ _               (refl _)            = refl
-steps-respˡ (_ ∷ ys≋xs)     (prep _ ys↭zs)      = cong suc (steps-respˡ ys≋xs ys↭zs)
-steps-respˡ (_ ∷ _ ∷ ys≋xs) (swap _ _ ys↭zs)    = cong suc (steps-respˡ ys≋xs ys↭zs)
-steps-respˡ ys≋xs           (trans ys↭ws ws↭zs) = cong (_+ steps ws↭zs) (steps-respˡ ys≋xs ys↭ws)
+steps-respˡ = Properties.Steps.steps-respˡ ≈-trans ≈-sym
 
-steps-respʳ : ∀ {xs ys zs} (xs≋ys : xs ≋ ys) (zs↭xs : zs ↭ xs) →
+steps-respʳ : (xs≋ys : xs ≋ ys) (zs↭xs : zs ↭ xs) →
               steps (↭-respʳ-≋ xs≋ys zs↭xs) ≡ steps zs↭xs
-steps-respʳ _               (refl _)            = refl
-steps-respʳ (_ ∷ ys≋xs)     (prep _ ys↭zs)      = cong suc (steps-respʳ ys≋xs ys↭zs)
-steps-respʳ (_ ∷ _ ∷ ys≋xs) (swap _ _ ys↭zs)    = cong suc (steps-respʳ ys≋xs ys↭zs)
-steps-respʳ ys≋xs           (trans ys↭ws ws↭zs) = cong (steps ys↭ws +_) (steps-respʳ ys≋xs ws↭zs)
-
+steps-respʳ = Properties.Steps.steps-respʳ ≈-trans
+-}
 ------------------------------------------------------------------------
 -- Properties of list functions
 ------------------------------------------------------------------------
 
+------------------------------------------------------------------------
+-- Permutations of empty and singleton lists
+
+↭-[]-invˡ : [] ↭ xs → xs ≡ []
+↭-[]-invˡ = Properties.↭-[]-invˡ
+
+↭-[]-invʳ : xs ↭ [] → xs ≡ []
+↭-[]-invʳ = Properties.↭-[]-invʳ
+
+¬x∷xs↭[] : ¬ ((x ∷ xs) ↭ [])
+¬x∷xs↭[] = Properties.¬x∷xs↭[]ʳ
+
+↭-singleton⁻¹ : xs ↭ [ x ] → ∃ λ y → xs ≡ [ y ] × y ≈ x
+↭-singleton⁻¹ = Properties.↭-singleton-invʳ ≈-trans
+
+------------------------------------------------------------------------
+-- length
+
+↭-length : xs ↭ ys → length xs ≡ length ys
+↭-length = Properties.↭-length
+
 ------------------------------------------------------------------------
 -- map
 
-module _ (T : Setoid b ℓ) where
+module _ (T : Setoid b r) where
 
   open Setoid T using () renaming (_≈_ to _≈′_)
   open Permutation T using () renaming (_↭_ to _↭′_)
 
   map⁺ : ∀ {f} → f Preserves _≈_ ⟶ _≈′_ →
-         ∀ {xs ys} → xs ↭ ys → map f xs ↭′ map f ys
-  map⁺ pres (refl xs≋ys)  = refl (Pointwise.map⁺ _ _ (Pointwise.map pres xs≋ys))
-  map⁺ pres (prep x p)    = prep (pres x) (map⁺ pres p)
-  map⁺ pres (swap x y p)  = swap (pres x) (pres y) (map⁺ pres p)
-  map⁺ pres (trans p₁ p₂) = trans (map⁺ pres p₁) (map⁺ pres p₂)
+         xs ↭ ys → map f xs ↭′ map f ys
+  map⁺ pres = Properties.map⁺ pres
+
 
 ------------------------------------------------------------------------
 -- _++_
 
-shift : ∀ {v w} → v ≈ w → (xs ys : List A) → xs ++ [ v ] ++ ys ↭ w ∷ xs ++ ys
-shift {v} {w} v≈w []       ys = prep v≈w ↭-refl
-shift {v} {w} v≈w (x ∷ xs) ys = begin
-  x ∷ (xs ++ [ v ] ++ ys) <⟨ shift v≈w xs ys ⟩
-  x ∷ w ∷ xs ++ ys        <<⟨ ↭-refl ⟩
-  w ∷ x ∷ xs ++ ys        ∎
+shift : v ≈ w → ∀ xs ys → xs ++ [ v ] ++ ys ↭ w ∷ xs ++ ys
+shift v≈w xs ys = Properties.Reflexivity.shift ≈-refl v≈w xs {ys}
 
-↭-shift : ∀ {v} (xs ys : List A) → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
-↭-shift = shift ≈-refl
+↭-shift : ∀ xs {ys} → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
+↭-shift xs {ys} = shift ≈-refl xs ys
 
-++⁺ˡ : ∀ xs {ys zs : List A} → ys ↭ zs → xs ++ ys ↭ xs ++ zs
-++⁺ˡ []       ys↭zs = ys↭zs
-++⁺ˡ (x ∷ xs) ys↭zs = ↭-prep _ (++⁺ˡ xs ys↭zs)
+++⁺ʳ : ∀  zs → xs ↭ ys → xs ++ zs ↭ ys ++ zs
+++⁺ʳ = Properties.++⁺ʳ ≈-refl
 
-++⁺ʳ : ∀ {xs ys : List A} zs → xs ↭ ys → xs ++ zs ↭ ys ++ zs
-++⁺ʳ zs (refl xs≋ys)  = refl (Pointwise.++⁺ xs≋ys ≋-refl)
-++⁺ʳ zs (prep x ↭)    = prep x (++⁺ʳ zs ↭)
-++⁺ʳ zs (swap x y ↭)  = swap x y (++⁺ʳ zs ↭)
-++⁺ʳ zs (trans ↭₁ ↭₂) = trans (++⁺ʳ zs ↭₁) (++⁺ʳ zs ↭₂)
+++⁺ˡ : ∀ xs {ys zs} → ys ↭ zs → xs ++ ys ↭ xs ++ zs
+++⁺ˡ []       ys↭zs = ys↭zs
+++⁺ˡ (x ∷ xs) ys↭zs = ↭-prep x (++⁺ˡ xs ys↭zs)
 
 ++⁺ : _++_ Preserves₂ _↭_ ⟶ _↭_ ⟶ _↭_
-++⁺ ws↭xs ys↭zs = trans (++⁺ʳ _ ws↭xs) (++⁺ˡ _ ys↭zs)
+++⁺ ws↭xs ys↭zs = ↭-trans (++⁺ʳ _ ws↭xs) (++⁺ˡ _ ys↭zs)
 
 -- Algebraic properties
 
@@ -188,20 +196,21 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin
 ++-identityˡ xs = ↭-refl
 
 ++-identityʳ : RightIdentity _↭_ [] _++_
-++-identityʳ xs = ↭-reflexive (Lₚ.++-identityʳ xs)
+++-identityʳ xs = ↭-reflexive (List.++-identityʳ xs)
 
 ++-identity : Identity _↭_ [] _++_
 ++-identity = ++-identityˡ , ++-identityʳ
 
 ++-assoc : Associative _↭_ _++_
-++-assoc xs ys zs = ↭-reflexive (Lₚ.++-assoc xs ys zs)
+++-assoc xs ys zs = ↭-reflexive (List.++-assoc xs ys zs)
 
 ++-comm : Commutative _↭_ _++_
 ++-comm []       ys = ↭-sym (++-identityʳ ys)
 ++-comm (x ∷ xs) ys = begin
   x ∷ xs ++ ys   <⟨ ++-comm xs ys ⟩
-  x ∷ ys ++ xs   ↭⟨ ↭-shift ys xs ⟨
+  x ∷ ys ++ xs   ↭⟨ ↭-shift ys ⟨
   ys ++ (x ∷ xs) ∎
+  where open PermutationReasoning
 
 -- Structures
 
@@ -253,253 +262,131 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin
 
 -- Some other useful lemmas
 
-zoom : ∀ h {t xs ys : List A} → xs ↭ ys → h ++ xs ++ t ↭ h ++ ys ++ t
+zoom : ∀ h {t xs ys} → xs ↭ ys → h ++ xs ++ t ↭ h ++ ys ++ t
 zoom h {t} = ++⁺ˡ h ∘ ++⁺ʳ t
 
-inject : ∀ (v : A) {ws xs ys zs} → ws ↭ ys → xs ↭ zs →
+inject : ∀ v {ws xs ys zs} → ws ↭ ys → xs ↭ zs →
          ws ++ [ v ] ++ xs ↭ ys ++ [ v ] ++ zs
-inject v ws↭ys xs↭zs = trans (++⁺ˡ _ (↭-prep _ xs↭zs)) (++⁺ʳ _ ws↭ys)
+inject v ws↭ys xs↭zs = ↭-trans (++⁺ˡ _ (↭-prep _ xs↭zs)) (++⁺ʳ _ ws↭ys)
 
-shifts : ∀ xs ys {zs : List A} → xs ++ ys ++ zs ↭ ys ++ xs ++ zs
+shifts : ∀ xs ys {zs} → xs ++ ys ++ zs ↭ ys ++ xs ++ zs
 shifts xs ys {zs} = begin
    xs ++ ys  ++ zs ↭⟨ ++-assoc xs ys zs ⟨
   (xs ++ ys) ++ zs ↭⟨ ++⁺ʳ zs (++-comm xs ys) ⟩
   (ys ++ xs) ++ zs ↭⟨ ++-assoc ys xs zs ⟩
    ys ++ xs  ++ zs ∎
+  where open PermutationReasoning
+
+module _ where
 
-dropMiddleElement-≋ : ∀ {x} ws xs {ys} {zs} →
-           ws ++ [ x ] ++ ys ≋ xs ++ [ x ] ++ zs →
-           ws ++ ys ↭ xs ++ zs
-dropMiddleElement-≋ []       []       (_   ∷ eq) = ≋⇒↭ eq
-dropMiddleElement-≋ []       (x ∷ xs) (w≈v ∷ eq) = ↭-respˡ-≋ (≋-sym eq) (shift w≈v xs _)
-dropMiddleElement-≋ (w ∷ ws) []       (w≈x ∷ eq) = ↭-respʳ-≋ eq (↭-sym (shift (≈-sym w≈x) ws _))
-dropMiddleElement-≋ (w ∷ ws) (x ∷ xs) (w≈x ∷ eq) = prep w≈x (dropMiddleElement-≋ ws xs eq)
+  open Properties.LRTransitivity ↭-transˡ-≋ ↭-transʳ-≋
 
-dropMiddleElement : ∀ {v} ws xs {ys zs} →
+  dropMiddleElement-≋ : ∀ {x} ws xs {ys} {zs} →
+                        ws ++ [ x ] ++ ys ≋ xs ++ [ x ] ++ zs →
+                        ws ++ ys ↭ xs ++ zs
+  dropMiddleElement-≋ = DropMiddle.dropMiddleElement-≋ isEquivalence
+
+  dropMiddleElement : ∀ {v} ws xs {ys zs} →
                     ws ++ [ v ] ++ ys ↭ xs ++ [ v ] ++ zs →
                     ws ++ ys ↭ xs ++ zs
-dropMiddleElement {v} ws xs {ys} {zs} p = helper p ws xs ≋-refl ≋-refl
-  where
-  lemma : ∀ {w x y z} → w ≈ x → x ≈ y → z ≈ y → w ≈ z
-  lemma w≈x x≈y z≈y = ≈-trans (≈-trans w≈x x≈y) (≈-sym z≈y)
-
-  open PermutationReasoning
-
-  -- The l′ & l″ could be eliminated at the cost of making the `trans` case
-  -- much more difficult to prove. At the very least would require using `Acc`.
-  helper : ∀ {l′ l″ : List A} → l′ ↭ l″ →
-           ∀ ws xs {ys zs : List A} →
-           ws ++ [ v ] ++ ys ≋ l′ →
-           xs ++ [ v ] ++ zs ≋ l″ →
-           ws ++ ys ↭ xs ++ zs
-  helper {as}     {bs}     (refl eq3) ws xs {ys} {zs} eq1 eq2 =
-    dropMiddleElement-≋ ws xs (≋-trans (≋-trans eq1 eq3) (≋-sym eq2))
-  helper {_ ∷ as} {_ ∷ bs} (prep _ as↭bs) [] [] {ys} {zs} (_ ∷ ys≋as) (_ ∷ zs≋bs) = begin
-    ys               ≋⟨  ys≋as ⟩
-    as               ↭⟨  as↭bs ⟩
-    bs               ≋⟨ zs≋bs ⟨
-    zs               ∎
-  helper {_ ∷ as} {_ ∷ bs} (prep a≈b as↭bs) [] (x ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    ys               ≋⟨  ≋₁ ⟩
-    as               ↭⟨  as↭bs ⟩
-    bs               ≋⟨ ≋₂ ⟨
-    xs ++ v ∷ zs     ↭⟨  shift (lemma ≈₁ a≈b ≈₂) xs zs ⟩
-    x ∷ xs ++ zs     ∎
-  helper {_ ∷ as} {_ ∷ bs} (prep v≈w p) (w ∷ ws) [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    w ∷ ws ++ ys     ↭⟨  ↭-sym (shift (lemma ≈₂ (≈-sym v≈w) ≈₁) ws ys) ⟩
-    ws ++ v ∷ ys     ≋⟨  ≋₁ ⟩
-    as               ↭⟨  p ⟩
-    bs               ≋⟨ ≋₂ ⟨
-    zs               ∎
-  helper {_ ∷ as} {_ ∷ bs} (prep w≈x p) (w ∷ ws) (x ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    w ∷ ws ++ ys     ↭⟨ prep (lemma ≈₁ w≈x ≈₂) (helper p ws xs ≋₁ ≋₂) ⟩
-    x ∷ xs ++ zs     ∎
-  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈x y≈v p) [] [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    ys               ≋⟨  ≋₁ ⟩
-    a ∷ as           ↭⟨  prep (≈-trans (≈-trans (≈-trans y≈v (≈-sym ≈₂)) ≈₁) v≈x) p ⟩
-    b ∷ bs           ≋⟨ ≋₂ ⟨
-    zs               ∎
-  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈w y≈w p) [] (x ∷ []) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    ys               ≋⟨  ≋₁ ⟩
-    a ∷ as           ↭⟨  prep y≈w p ⟩
-    _ ∷ bs           ≋⟨ ≈₂ ∷ tail ≋₂ ⟨
-    x ∷ zs           ∎
-  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈w y≈x p) [] (x ∷ w ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    ys               ≋⟨ ≋₁ ⟩
-    a ∷ as           ↭⟨ prep y≈x p ⟩
-    _ ∷ bs           ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩
-    x ∷ xs ++ v ∷ zs ↭⟨ prep ≈-refl (shift (lemma ≈₁ v≈w (head ≋₂)) xs zs) ⟩
-    x ∷ w ∷ xs ++ zs ∎
-  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap w≈x _ p) (w ∷ []) [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    w ∷ ys           ≋⟨ ≈₁ ∷ tail (≋₁) ⟩
-    _ ∷ as           ↭⟨ prep w≈x p ⟩
-    b ∷ bs           ≋⟨ ≋-sym ≋₂ ⟩
-    zs               ∎
-  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap w≈y x≈v p) (w ∷ x ∷ ws) [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    w ∷ x ∷ ws ++ ys ↭⟨ prep ≈-refl (↭-sym (shift (lemma ≈₂ (≈-sym x≈v) (head ≋₁)) ws ys)) ⟩
-    w ∷ ws ++ v ∷ ys ≋⟨ ≈₁ ∷ tail ≋₁ ⟩
-    _ ∷ as           ↭⟨ prep w≈y p ⟩
-    b ∷ bs           ≋⟨ ≋-sym ≋₂ ⟩
-    zs               ∎
-  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap x≈v v≈y p) (x ∷ []) (y ∷ []) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    x ∷ ys           ≋⟨ ≈₁ ∷ tail ≋₁ ⟩
-    _ ∷ as           ↭⟨ prep (≈-trans x≈v (≈-trans (≈-sym (head ≋₂)) (≈-trans (head ≋₁) v≈y))) p ⟩
-    _ ∷ bs           ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩
-    y ∷ zs           ∎
-  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap y≈w v≈z p) (y ∷ []) (z ∷ w ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    y ∷ ys           ≋⟨ ≈₁ ∷ tail ≋₁ ⟩
-    _ ∷ as           ↭⟨ prep y≈w p ⟩
-    _ ∷ bs           ≋⟨ ≋-sym ≋₂ ⟩
-    w ∷ xs ++ v ∷ zs ↭⟨ ↭-prep w (↭-shift xs zs) ⟩
-    w ∷ v ∷ xs ++ zs ↭⟨ swap ≈-refl (lemma (head ≋₁) v≈z ≈₂) ↭-refl ⟩
-    z ∷ w ∷ xs ++ zs ∎
-  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap y≈v w≈z p) (y ∷ w ∷ ws) (z ∷ []) {ys} {zs}    (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    y ∷ w ∷ ws ++ ys ↭⟨ swap (lemma ≈₁ y≈v (head ≋₂)) ≈-refl ↭-refl ⟩
-    w ∷ v ∷ ws ++ ys ↭⟨ ↭-prep w (↭-sym (↭-shift ws ys)) ⟩
-    w ∷ ws ++ v ∷ ys ≋⟨ ≋₁ ⟩
-    _ ∷ as           ↭⟨ prep w≈z p ⟩
-    _ ∷ bs           ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩
-    z ∷ zs           ∎
-  helper (swap x≈z y≈w p) (x ∷ y ∷ ws) (w ∷ z ∷ xs) {ys} {zs} (≈₁ ∷ ≈₃ ∷ ≋₁) (≈₂ ∷ ≈₄ ∷ ≋₂) = begin
-    x ∷ y ∷ ws ++ ys ↭⟨ swap (lemma ≈₁ x≈z ≈₄) (lemma ≈₃ y≈w ≈₂) (helper p ws xs ≋₁ ≋₂) ⟩
-    w ∷ z ∷ xs ++ zs ∎
-  helper {as} {bs} (trans p₁ p₂) ws xs eq1 eq2
-    with ∈-∃++ S (∈-resp-↭ (↭-respˡ-≋ (≋-sym eq1) p₁) (∈-insert S ws ≈-refl))
-  ... | (h , t , w , v≈w , eq) = trans
-    (helper p₁ ws h eq1 (≋-trans (≋.++⁺ ≋-refl (v≈w ∷ ≋-refl)) (≋-sym eq)))
-    (helper p₂ h xs (≋-trans (≋.++⁺ ≋-refl (v≈w ∷ ≋-refl)) (≋-sym eq)) eq2)
-
-dropMiddle : ∀ {vs} ws xs {ys zs} →
-             ws ++ vs ++ ys ↭ xs ++ vs ++ zs →
-             ws ++ ys ↭ xs ++ zs
-dropMiddle {[]}     ws xs p = p
-dropMiddle {v ∷ vs} ws xs p = dropMiddle ws xs (dropMiddleElement ws xs p)
-
-split : ∀ (v : A) as bs {xs} → xs ↭ as ++ [ v ] ++ bs → ∃₂ λ ps qs → xs ≋ ps ++ [ v ] ++ qs
-split v as bs p = helper as bs p (<-wellFounded (steps p))
-  where
-  helper : ∀ as bs {xs} (p : xs ↭ as ++ [ v ] ++ bs) → Acc _<_ (steps p) →
-           ∃₂ λ ps qs → xs ≋ ps ++ [ v ] ++ qs
-  helper []           bs (refl eq)    _ = []         , bs , eq
-  helper (a ∷ [])     bs (refl eq)    _ = [ a ]      , bs , eq
-  helper (a ∷ b ∷ as) bs (refl eq)    _ = a ∷ b ∷ as , bs , eq
-  helper []           bs (prep v≈x _) _ = [] , _ , v≈x ∷ ≋-refl
-  helper (a ∷ as)     bs (prep eq as↭xs) (acc rec) with helper as bs as↭xs (rec ≤-refl)
-  ... | (ps , qs , eq₂) = a ∷ ps , qs , eq ∷ eq₂
-  helper [] (b ∷ bs)     (swap x≈b y≈v _) _ = [ b ] , _     , x≈b ∷ y≈v ∷ ≋-refl
-  helper (a ∷ [])     bs (swap x≈v y≈a ↭) _ = []    , a ∷ _ , x≈v ∷ y≈a ∷ ≋-refl
-  helper (a ∷ b ∷ as) bs (swap x≈b y≈a as↭xs) (acc rec) with helper as bs as↭xs (rec ≤-refl)
-  ... | (ps , qs , eq) = b ∷ a ∷ ps , qs , x≈b ∷ y≈a ∷ eq
-  helper as           bs (trans ↭₁ ↭₂) (acc rec) with helper as bs ↭₂ (rec (m<n+m (steps ↭₂) (0<steps ↭₁)))
-  ... | (ps , qs , eq) = helper ps qs (↭-respʳ-≋ eq ↭₁)
-      (rec (subst (_< _) (sym (steps-respʳ eq ↭₁)) (m<m+n (steps ↭₁) (0<steps ↭₂))))
+  dropMiddleElement {v} = DropMiddle.dropMiddleElement isEquivalence {x = v}
+
+  dropMiddle : ∀ {vs} ws xs {ys zs} →
+               ws ++ vs ++ ys ↭ xs ++ vs ++ zs →
+               ws ++ ys ↭ xs ++ zs
+  dropMiddle {[]}     ws xs p = p
+  dropMiddle {v ∷ vs} ws xs p = dropMiddle ws xs (dropMiddleElement ws xs p)
+
+  split-↭ : ∀ v as bs {xs} → xs ↭ as ++ [ v ] ++ bs →
+            ∃₂ λ ps qs → xs ≋ ps ++ [ v ] ++ qs × ps ++ qs ↭ as ++ bs
+  split-↭ v as bs p = Split.↭-split ≈-refl ≈-trans v as bs p
+
+  split : ∀ v as bs {xs} → xs ↭ as ++ [ v ] ++ bs → ∃₂ λ ps qs → xs ≋ ps ++ [ v ] ++ qs
+  split v as bs p with ps , qs , eq , _ ← split-↭ v as bs p = ps , qs , eq
+
+
+------------------------------------------------------------------------
+-- _∷_
+
+drop-∷ : x ∷ xs ↭ x ∷ ys → xs ↭ ys
+drop-∷ = dropMiddleElement [] []
 
 ------------------------------------------------------------------------
 -- filter
 
-module _ {p} {P : Pred A p} (P? : Decidable P) (P≈ : P Respects _≈_) where
-
-  filter⁺ : ∀ {xs ys : List A} → xs ↭ ys → filter P? xs ↭ filter P? ys
-  filter⁺ (refl xs≋ys)        = refl (≋.filter⁺ P? P≈ xs≋ys)
-  filter⁺ (trans xs↭zs zs↭ys) = trans (filter⁺ xs↭zs) (filter⁺ zs↭ys)
-  filter⁺ {x ∷ xs} {y ∷ ys} (prep x≈y xs↭ys) with P? x | P? y
-  ... | yes _  | yes _  = prep x≈y (filter⁺ xs↭ys)
-  ... | yes Px | no ¬Py = contradiction (P≈ x≈y Px) ¬Py
-  ... | no ¬Px | yes Py = contradiction (P≈ (≈-sym x≈y) Py) ¬Px
-  ... | no  _  | no  _  = filter⁺ xs↭ys
-  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) with P? x | P? y
-  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | no ¬Px | no ¬Py
-    with P? z | P? w
-  ... | _      | yes Pw = contradiction (P≈ w≈y Pw) ¬Py
-  ... | yes Pz | _      = contradiction (P≈ (≈-sym x≈z) Pz) ¬Px
-  ... | no _   | no  _  = filter⁺ xs↭ys
-  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | no ¬Px | yes Py
-    with P? z | P? w
-  ... | _      | no ¬Pw = contradiction (P≈ (≈-sym w≈y) Py) ¬Pw
-  ... | yes Pz | _      = contradiction (P≈ (≈-sym x≈z) Pz) ¬Px
-  ... | no _   | yes _  = prep w≈y (filter⁺ xs↭ys)
-  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys)  | yes Px | no ¬Py
-    with P? z | P? w
-  ... | no ¬Pz | _      = contradiction (P≈ x≈z Px) ¬Pz
-  ... | _      | yes Pw = contradiction (P≈ w≈y Pw) ¬Py
-  ... | yes _  | no _   = prep x≈z (filter⁺ xs↭ys)
-  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | yes Px | yes Py
-    with P? z | P? w
-  ... | no ¬Pz | _      = contradiction (P≈ x≈z Px) ¬Pz
-  ... | _      | no ¬Pw = contradiction (P≈ (≈-sym w≈y) Py) ¬Pw
-  ... | yes _  | yes _  = swap x≈z w≈y (filter⁺ xs↭ys)
+module _ (P? : Decidable P) (P≈ : P Respects _≈_) where
+
+  filter⁺ : xs ↭ ys → filter P? xs ↭ filter P? ys
+  filter⁺ = Properties.filter⁺ ≈-sym P? P≈
 
 ------------------------------------------------------------------------
 -- partition
 
-module _ {p} {P : Pred A p} (P? : Decidable P) where
+module _ (P? : Decidable P) where
 
-  partition-↭ : ∀ xs → (let ys , zs = partition P? xs) → xs ↭ ys ++ zs
+  partition-↭ : ∀ xs → let ys , zs = partition P? xs in xs ↭ ys ++ zs
   partition-↭ []       = ↭-refl
   partition-↭ (x ∷ xs) with does (P? x)
   ... | true  = ↭-prep x (partition-↭ xs)
-  ... | false = ↭-trans (↭-prep x (partition-↭ xs)) (↭-sym (↭-shift _ _))
-    where open PermutationReasoning
-
-------------------------------------------------------------------------
--- merge
-
-module _ {ℓ} {R : Rel A ℓ} (R? : B.Decidable R) where
-
-  merge-↭ : ∀ xs ys → merge R? xs ys ↭ xs ++ ys
-  merge-↭ []       []       = ↭-refl
-  merge-↭ []       (y ∷ ys) = ↭-refl
-  merge-↭ (x ∷ xs) []       = ↭-sym (++-identityʳ (x ∷ xs))
-  merge-↭ (x ∷ xs) (y ∷ ys)
-    with does (R? x y) | merge-↭ xs (y ∷ ys) | merge-↭ (x ∷ xs) ys
-  ... | true  | rec | _   = ↭-prep x rec
-  ... | false | _   | rec = begin
-    y ∷ merge R? (x ∷ xs) ys <⟨ rec ⟩
-    y ∷ x ∷ xs ++ ys         ↭⟨ ↭-shift (x ∷ xs) ys ⟨
-    (x ∷ xs) ++ y ∷ ys       ≡⟨ Lₚ.++-assoc [ x ] xs (y ∷ ys) ⟨
-    x ∷ xs ++ y ∷ ys         ∎
-    where open PermutationReasoning
+  ... | false = ↭-trans (↭-prep x (partition-↭ xs)) (↭-sym (↭-shift _))
 
 ------------------------------------------------------------------------
 -- _∷ʳ_
 
-∷↭∷ʳ : ∀ (x : A) xs → x ∷ xs ↭ xs ∷ʳ x
+∷↭∷ʳ : ∀ x xs → x ∷ xs ↭ xs ∷ʳ x
 ∷↭∷ʳ x xs = ↭-sym (begin
-  xs ++ [ x ]   ↭⟨ ↭-shift xs [] ⟩
-  x ∷ xs ++ []  ≡⟨ Lₚ.++-identityʳ _ ⟩
+  xs ++ [ x ]   ↭⟨ ↭-shift xs ⟩
+  x ∷ xs ++ []  ≡⟨ List.++-identityʳ _ ⟩
   x ∷ xs        ∎)
   where open PermutationReasoning
 
 ------------------------------------------------------------------------
 -- ʳ++
 
-++↭ʳ++ : ∀ (xs ys : List A) → xs ++ ys ↭ xs ʳ++ ys
+++↭ʳ++ : ∀ xs ys → xs ++ ys ↭ xs ʳ++ ys
 ++↭ʳ++ []       ys = ↭-refl
-++↭ʳ++ (x ∷ xs) ys = ↭-trans (↭-sym (↭-shift xs ys)) (++↭ʳ++ xs (x ∷ ys))
+++↭ʳ++ (x ∷ xs) ys = ↭-trans (↭-sym (↭-shift xs)) (++↭ʳ++ xs (x ∷ ys))
+
+------------------------------------------------------------------------
+-- reverse
+
+↭-reverse : ∀ xs → reverse xs ↭ xs
+↭-reverse [] = ↭-refl
+↭-reverse (x ∷ xs) = begin
+  reverse (x ∷ xs) ≡⟨ List.unfold-reverse x xs ⟩
+  reverse xs ∷ʳ x  ↭⟨ ∷↭∷ʳ x (reverse xs) ⟨
+  x ∷ reverse xs   <⟨ ↭-reverse xs ⟩
+  x ∷ xs           ∎
+  where open PermutationReasoning
+
+------------------------------------------------------------------------
+-- merge
+
+module _ (R? : B.Decidable R) where
+
+  merge-↭ : ∀ xs ys → merge R? xs ys ↭ xs ++ ys
+  merge-↭ []            []            = ↭-refl
+  merge-↭ []            y∷ys@(_ ∷ _)  = ↭-refl
+  merge-↭ x∷xs@(_ ∷ _)  []            = ↭-sym (++-identityʳ x∷xs)
+  merge-↭ x∷xs@(x ∷ xs) y∷ys@(y ∷ ys)
+    with does (R? x y) | merge-↭ xs y∷ys | merge-↭ x∷xs ys
+  ... | true  | rec | _   = ↭-prep x rec
+  ... | false | _   | rec = begin
+    y ∷ merge R? x∷xs ys <⟨ rec ⟩
+    y ∷ x∷xs ++ ys       ↭⟨ ↭-shift x∷xs ⟨
+    x∷xs ++ y∷ys         ≡⟨ List.++-assoc [ x ] xs y∷ys ⟨
+    x∷xs ++ y∷ys         ∎
+    where open PermutationReasoning
 
 ------------------------------------------------------------------------
 -- foldr of Commutative Monoid
 
-module _ {_∙_ : Op₂ A} {ε : A} (isCmonoid : IsCommutativeMonoid _≈_ _∙_ ε) where
-  open module CM = IsCommutativeMonoid isCmonoid
+module _ {_∙_ : Op₂ A} {ε : A}
+         (isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε) where
 
   private
-    module S = RelSetoid setoid
-
-    cmonoid : CommutativeMonoid _ _
-    cmonoid = record { isCommutativeMonoid = isCmonoid }
-
-  open ACM cmonoid
-
-  foldr-commMonoid : ∀ {xs ys} → xs ↭ ys → foldr _∙_ ε xs ≈ foldr _∙_ ε ys
-  foldr-commMonoid (refl []) = CM.refl
-  foldr-commMonoid (refl (x≈y ∷ xs≈ys)) = ∙-cong x≈y (foldr-commMonoid (Permutation.refl xs≈ys))
-  foldr-commMonoid (prep x≈y xs↭ys) = ∙-cong x≈y (foldr-commMonoid xs↭ys)
-  foldr-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = S.begin
-    x ∙ (y ∙ foldr _∙_ ε xs)   S.≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩
-    x ∙ (y ∙ foldr _∙_ ε ys)   S.≈⟨ assoc x y (foldr _∙_ ε ys) ⟨
-    (x ∙ y) ∙ foldr _∙_ ε ys   S.≈⟨ ∙-congʳ (comm x y) ⟩
-    (y ∙ x) ∙ foldr _∙_ ε ys   S.≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩
-    (y′ ∙ x′) ∙ foldr _∙_ ε ys S.≈⟨ assoc y′ x′ (foldr _∙_ ε ys) ⟩
-    y′ ∙ (x′ ∙ foldr _∙_ ε ys) S.∎
-  foldr-commMonoid (trans xs↭ys ys↭zs) = CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs)
+    commutativeMonoid : CommutativeMonoid _ _
+    commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
+
+  foldr-commMonoid : xs ↭ ys → foldr _∙_ ε xs ≈ foldr _∙_ ε ys
+  foldr-commMonoid = Properties.foldr-commMonoid commutativeMonoid
diff --git a/src/Data/List/Relation/Ternary/Interleaving/Propositional.agda b/src/Data/List/Relation/Ternary/Interleaving/Propositional.agda
index 55515cd447..fd198e20f2 100644
--- a/src/Data/List/Relation/Ternary/Interleaving/Propositional.agda
+++ b/src/Data/List/Relation/Ternary/Interleaving/Propositional.agda
@@ -37,6 +37,6 @@ toPermutation : ∀ {l r as} → Interleaving l r as → as ↭ l ++ r
 toPermutation []         = Perm.refl
 toPermutation (consˡ sp) = Perm.prep _ (toPermutation sp)
 toPermutation {l} {r ∷ rs} {a ∷ as} (consʳ sp) = begin
-  a ∷ as       ↭⟨ Perm.prep a (toPermutation sp) ⟩
-  a ∷ l ++ rs  ↭⟨ Perm.↭-sym (shift a l rs) ⟩
+  a ∷ as       <⟨ toPermutation sp ⟩
+  a ∷ l ++ rs  ↭⟨ shift a l rs ⟨
   l ++ a ∷ rs  ∎