diff --git a/CHANGELOG.md b/CHANGELOG.md
index ee056ad8c9..44f80722d1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -27,6 +27,13 @@ Non-backwards compatible changes
 * The definitions in `Algebra.Module.Morphism.Construct.Identity` are now
   parametrized by _raw_ bundles, and as such take a proof of reflexivity.
 
+* In `Data.List.Relation.Binary.Permutation.Homogeneous`, the explicit use of `Pointwise`
+  has been removed in favour of an additional relation on lists. This enables us to keep
+  using `Pointwise _≈_` in the setoid case but use the more convenient `_≡_` instead in
+  the propositional one.
+  Correspondingly, `Data.List.Relation.Binary.Permutation.Propositional` has been refactored
+  as an instance of the generic data structure.
+
 Other major improvements
 ------------------------
 
@@ -79,7 +86,7 @@ New modules
   ```agda
   Algebra.Module.Construct.Idealization
   ```
-  
+
 * `Function.Relation.Binary.Equality`
   ```agda
   setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _
@@ -155,7 +162,7 @@ Additions to existing modules
   quasigroup      : Quasigroup _ _
   isLoop          : IsLoop _∙_ _\\_ _//_ ε
   loop            : Loop _ _
-  
+
   \\-leftDividesˡ  : LeftDividesˡ _∙_ _\\_
   \\-leftDividesʳ  : LeftDividesʳ _∙_ _\\_
   \\-leftDivides   : LeftDivides _∙_ _\\_
@@ -174,7 +181,7 @@ Additions to existing modules
   identityʳ-unique : x ∙ y ≈ x → y ≈ ε
   identity-unique  : Identity x _∙_ → x ≈ ε
   ```
- 
+
 * In `Algebra.Construct.Terminal`:
   ```agda
   rawNearSemiring : RawNearSemiring c ℓ
@@ -203,7 +210,7 @@ Additions to existing modules
   _\\_ : Op₂ A
   x \\ y = (x ⁻¹) ∙ y
   ```
- 
+
 * In `Data.Container.Indexed.Core`:
   ```agda
   Subtrees o c = (r : Response c) → X (next c r)
@@ -305,7 +312,7 @@ Additions to existing modules
   pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
   pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
   ```
-  
+
 * Added new proofs to `Data.Nat.Primality`:
   ```agda
   rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n
diff --git a/doc/README/Data/List/Relation/Binary/Permutation.agda b/doc/README/Data/List/Relation/Binary/Permutation.agda
index e9141d89c7..9e702de285 100644
--- a/doc/README/Data/List/Relation/Binary/Permutation.agda
+++ b/doc/README/Data/List/Relation/Binary/Permutation.agda
@@ -9,8 +9,6 @@ module README.Data.List.Relation.Binary.Permutation where
 open import Algebra.Structures using (IsCommutativeMonoid)
 open import Data.List.Base
 open import Data.Nat using (ℕ; _+_)
-open import Relation.Binary.PropositionalEquality
-  using (_≡_; refl; sym; cong; setoid)
 
 ------------------------------------------------------------------------
 -- Permutations
diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index f014df8b41..b2aa05d60e 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -23,7 +23,9 @@ 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
+  using (_↭_; ↭-refl; ↭-sym; module PermutationReasoning)
 open import Data.List.Relation.Binary.Permutation.Propositional.Properties
+  using (↭-sym-involutive; ∈-resp-↭; ∈-resp-[σ⁻¹∘σ]; ++-comm; ↭-shift)
 open import Data.Product.Base as Prod hiding (map)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum hiding (map)
@@ -54,6 +56,7 @@ private
     x y : A
     ws xs ys zs : List A
 
+
 ------------------------------------------------------------------------
 -- Definitions
 
@@ -142,8 +145,8 @@ module _ {k} {f g : A → B} {xs ys} where
     helper y = mk↔ₛ′
       (λ x≡fy → ≡.trans x≡fy (        f≗g y))
       (λ x≡gy → ≡.trans x≡gy (≡.sym $ f≗g y))
-      (λ { ≡.refl → ≡.trans-symˡ (f≗g y) })
-      λ { ≡.refl → ≡.trans-symʳ (f≗g y) }
+      (λ { refl → ≡.trans-symˡ (f≗g y) })
+      λ { refl → ≡.trans-symʳ (f≗g y) }
 
 ------------------------------------------------------------------------
 -- _++_
@@ -281,7 +284,6 @@ empty-unique {xs = _ ∷ _} ∷∼[] with () ← ⇒→ ∷∼[] (here refl)
                                                 MP.right-distributive xs₁ xs₂ (pure ∘ f)) ⟩
   (fs >>= λ f → (xs₁ >>= pure ∘ f) ++
                 (xs₂ >>= pure ∘ f))       ≈⟨ >>=-left-distributive fs ⟩
-
   (fs >>= λ f → xs₁ >>= pure ∘ f) ++
   (fs >>= λ f → xs₂ >>= pure ∘ f)         ≡⟨ ≡.cong₂ _++_ (Applicative.unfold-⊛ fs xs₁) (Applicative.unfold-⊛ fs xs₂) ⟨
 
@@ -295,7 +297,8 @@ private
 
   ¬-drop-cons : ∀ {x : A} →
     ¬ (∀ {xs ys} → x ∷ xs ∼[ set ] x ∷ ys → xs ∼[ set ] ys)
-  ¬-drop-cons {x = x} drop-cons with Equivalence.to x∼[] (here refl)
+  ¬-drop-cons {x = x} drop-cons
+    with Equivalence.to x∼[] (here refl)
     where
     x,x≈x :  (x ∷ x ∷ []) ∼[ set ] [ x ]
     x,x≈x = ++-idempotent [ x ]
@@ -584,12 +587,12 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
   to∘from p with res ← from∘to (↭-sym p) rewrite ↭-sym-involutive p = res
 
 ∼bag⇒↭ : _∼[ bag ]_ ⇒ _↭_ {A = A}
-∼bag⇒↭ {A = A} {[]} eq with refl ← empty-unique (↔-sym eq) = refl
+∼bag⇒↭ {A = A} {[]} eq with refl ← empty-unique (↔-sym eq) = ↭-refl
 ∼bag⇒↭ {A = A} {x ∷ xs} eq
   with zs₁ , zs₂ , p ← ∈-∃++ (Inverse.to (eq {x}) (here ≡.refl)) 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₂ ⟨
+    x ∷ (zs₁ ++ zs₂) ↭⟨ ↭-shift zs₁ ⟨
     zs₁ ++ x ∷ zs₂   ∎
     where
     open CommutativeMonoid (commutativeMonoid bag A)
diff --git a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
index 12015b3076..77583c730c 100644
--- a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
@@ -9,10 +9,6 @@
 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 Level using (Level; _⊔_)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles using (Setoid)
@@ -21,41 +17,45 @@ open import Relation.Binary.Definitions using (Reflexive; Symmetric)
 
 private
   variable
-    a r s : Level
+    a pr r ps s : Level
     A : Set 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
+-- PR is morally the pointwise lifting of R to lists but it need not be intensionally
+data Permutation {A : Set a} (PR : Rel (List A) pr) (R : Rel A r) : Rel (List A) (a ⊔ pr ⊔ r) where
+  refl  : ∀ {xs ys} → PR xs ys → Permutation PR R xs ys
+  prep  : ∀ {xs ys x y} (eq : R x y) → Permutation PR R xs ys → Permutation PR R (x ∷ xs) (y ∷ ys)
+  swap  : ∀ {xs ys x y x′ y′} (eq₁ : R x x′) (eq₂ : R y y′) → Permutation PR R xs ys → Permutation PR R (x ∷ y ∷ xs) (y′ ∷ x′ ∷ ys)
+  trans : ∀ {xs ys zs} → Permutation PR R xs ys → Permutation PR R ys zs → Permutation PR R xs zs
 
 ------------------------------------------------------------------------
 -- The Permutation relation is an equivalence
 
-module _ {R : Rel A r}  where
+module _ {PR : Rel (List A) pr} {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)
+  sym : Symmetric PR → Symmetric R → Symmetric (Permutation PR R)
+  sym PR-sym R-sym (refl xs∼ys)           = refl (PR-sym xs∼ys)
+  sym PR-sym R-sym (prep x∼x′ xs↭ys)      = prep (R-sym x∼x′) (sym PR-sym R-sym xs↭ys)
+  sym PR-sym R-sym (swap x∼x′ y∼y′ xs↭ys) = swap (R-sym y∼y′) (R-sym x∼x′) (sym PR-sym R-sym xs↭ys)
+  sym PR-sym R-sym (trans xs↭ys ys↭zs)    = trans (sym PR-sym R-sym ys↭zs) (sym PR-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
+  isEquivalence : Reflexive PR →
+                  Symmetric PR → Symmetric R →
+                  IsEquivalence (Permutation PR R)
+  isEquivalence PR-refl PR-sym R-sym = record
+    { refl  = refl PR-refl
+    ; sym   = sym PR-sym R-sym
     ; trans = trans
     }
 
-  setoid : Reflexive R → Symmetric R → Setoid _ _
-  setoid R-refl R-sym = record
-    { isEquivalence = isEquivalence R-refl R-sym
+  setoid : Reflexive PR → Symmetric PR → Symmetric R → Setoid _ _
+  setoid PR-refl PR-sym R-sym = record
+    { isEquivalence = isEquivalence PR-refl PR-sym 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)
+map : ∀ {PR : Rel (List A) pr} {PS : Rel (List A) ps} →
+        {R : Rel A r} {S : Rel A s} →
+        (PR ⇒ PS) → (R ⇒ S) → (Permutation PR R ⇒ Permutation PS S)
+map PR⇒PS R⇒S (refl xs∼ys)         = refl (PR⇒PS xs∼ys)
+map PR⇒PS R⇒S (prep e xs∼ys)       = prep (R⇒S e) (map PR⇒PS R⇒S xs∼ys)
+map PR⇒PS R⇒S (swap e₁ e₂ xs∼ys)   = swap (R⇒S e₁) (R⇒S e₂) (map PR⇒PS R⇒S xs∼ys)
+map PR⇒PS R⇒S (trans xs∼ys ys∼zs)  = trans (map PR⇒PS R⇒S xs∼ys) (map PR⇒PS R⇒S ys∼zs)
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional.agda b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
index c41793d28a..66235b518f 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
@@ -14,41 +14,38 @@ 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
+import Data.List.Relation.Binary.Permutation.Homogeneous as Homogeneous
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 open import Relation.Binary.Reasoning.Syntax
 
-------------------------------------------------------------------------
--- An inductive 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.
+------------------------------------------------------------------------
+-- Definition
 
 infix 3 _↭_
 
-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
+_↭_ : Rel (List A) a
+_↭_ = Homogeneous.Permutation _≡_ _≡_
+
+pattern refl = Homogeneous.refl ≡.refl
+pattern prep {xs} {ys} x tl = Homogeneous.prep {xs = xs} {ys = ys} {x = x} ≡.refl tl
+pattern swap {xs} {ys} x y tl = Homogeneous.swap {xs = xs} {ys = ys} {x = x} {y = y} ≡.refl ≡.refl tl
+
+open Homogeneous public
+  using (trans)
 
 ------------------------------------------------------------------------
 -- _↭_ is an equivalence
 
 ↭-reflexive : _≡_ ⇒ _↭_
-↭-reflexive refl = refl
+↭-reflexive ≡.refl = 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)
+↭-sym = Homogeneous.sym ≡.sym ≡.sym
 
 -- A smart version of trans that avoids unnecessary `refl`s (see #1113).
 ↭-trans : Transitive _↭_
@@ -74,7 +71,7 @@ data _↭_ : Rel (List A) a where
 
 module PermutationReasoning where
 
-  private module Base = EqReasoning ↭-setoid
+  private module Base = ≈-Reasoning ↭-setoid
 
   open Base public
     hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨)
@@ -89,12 +86,12 @@ 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 x 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 x y 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
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index d56bdb7fb3..fc3a3dd821 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -12,8 +12,8 @@ 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.Base using (suc; _*_)
-open import Data.Nat.Properties using (*-assoc; *-comm)
+open import Data.Nat.Base using (suc)
+open import Data.Nat.Properties using (*-1-commutativeMonoid)
 open import Data.Product.Base using (-,_; proj₂)
 open import Data.List.Base as List
 open import Data.List.Relation.Binary.Permutation.Propositional
@@ -21,7 +21,7 @@ open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 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.Product.Base using (_,_; _×_; ∃; ∃₂)
 open import Function.Base using (_∘_; _⟨_⟩_)
 open import Level using (Level)
@@ -29,13 +29,14 @@ open import Relation.Unary using (Pred)
 open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
 open import Relation.Binary.Definitions using (_Respects_; Decidable)
 open import Relation.Binary.PropositionalEquality.Core as ≡
-  using (_≡_ ; refl ; cong; cong₂; _≢_)
+  using (_≡_ ; cong; cong₂; _≢_)
 open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 open import Relation.Nullary
 
 private
   variable
-    a b p : Level
+    a b p r : Level
     A : Set a
     B : Set b
 
@@ -43,23 +44,22 @@ private
 -- 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
+↭-empty-inv refl = ≡.refl
+↭-empty-inv (trans p q) with ≡.refl ← ↭-empty-inv q = ↭-empty-inv p
 
 ¬x∷xs↭[] : ∀ {x} {xs : List A} → ¬ ((x ∷ xs) ↭ [])
-¬x∷xs↭[] (trans s₁ s₂) with ↭-empty-inv s₂
-... | refl = ¬x∷xs↭[] s₁
+¬x∷xs↭[] (trans s₁ s₂) with ≡.refl ← ↭-empty-inv s₂ = ¬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 ρ₁
+↭-singleton-inv refl                                           = ≡.refl
+↭-singleton-inv (prep _ ρ) with ≡.refl ← ↭-empty-inv ρ         = ≡.refl
+↭-singleton-inv (trans ρ₁ ρ₂) with ≡.refl ← ↭-singleton-inv ρ₂ = ↭-singleton-inv ρ₁
 
 ------------------------------------------------------------------------
 -- sym
 
 ↭-sym-involutive : ∀ {xs ys : List A} (p : xs ↭ ys) → ↭-sym (↭-sym p) ≡ p
-↭-sym-involutive refl          = refl
+↭-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 ↭₁ ↭₂) =
@@ -90,20 +90,20 @@ 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-[σ⁻¹∘σ] 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
+  = ≡.refl
 Any-resp-[σ⁻¹∘σ] (prep _ σ)    (there ix)
   rewrite Any-resp-[σ⁻¹∘σ] σ ix
-  = refl
+  = ≡.refl
 Any-resp-[σ⁻¹∘σ] (swap _ _ σ)  (there (there ix))
   rewrite Any-resp-[σ⁻¹∘σ] σ ix
-  = refl
+  = ≡.refl
 
 ∈-resp-[σ⁻¹∘σ] : {xs ys : List A} {x : A} →
                  (σ : xs ↭ ys) →
@@ -126,17 +126,17 @@ module _ (f : A → B) where
   ↭-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 ρ₃ ρ₄
+  ↭-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 ρ₃ ρ₄
 
 ------------------------------------------------------------------------
 -- length
 
 ↭-length : ∀ {xs ys : List A} → xs ↭ ys → length xs ≡ length ys
-↭-length refl            = refl
+↭-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₂)
@@ -174,59 +174,63 @@ shift v (x ∷ xs) ys = begin
   v ∷ x ∷ xs ++ ys        ∎
   where open PermutationReasoning
 
+-- a better parametrisation
+↭-shift : ∀ {v : A} xs {ys} → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
+↭-shift {v = v} xs {ys} = shift v xs ys
+
 drop-mid-≡ : ∀ {x : A} ws xs {ys} {zs} →
              ws ++ [ x ] ++ ys ≡ xs ++ [ x ] ++ 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-≡ []       []       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 List.∷-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 →
            ws ++ ys ↭ xs ++ zs
-drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs refl refl
+drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs ≡.refl ≡.refl
   where
   drop-mid′ : ∀ {l′ l″ : List A} → l′ ↭ l″ →
               ∀ ws xs {ys zs} →
               ws ++ [ x ] ++ ys ≡ l′ →
               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)   []           (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)
-  drop-mid′ (swap y z p) []           []           refl refl = prep _ p
-  drop-mid′ (swap y z p) []           (x ∷ [])     refl eq   with cong {B = List _}
+  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)   []           (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)
+  drop-mid′ (swap y z p) []           []           ≡.refl ≡.refl = prep _ p
+  drop-mid′ (swap y z p) []           (x ∷ [])     ≡.refl eq   with cong {B = List _}
                                                                        (λ { (x ∷ _ ∷ xs) → x ∷ xs
                                                                           ; _            → []
                                                                           })
                                                                        eq
-  drop-mid′ (swap y z p) []           (x ∷ [])     refl eq   | refl = prep _ p
-  drop-mid′ (swap y z p) []           (x ∷ _ ∷ xs) refl refl = prep _ (trans p (shift _ _ _))
-  drop-mid′ (swap y z p) (w ∷ [])     []           refl eq   with cong tail eq
-  drop-mid′ (swap y z p) (w ∷ [])     []           refl eq   | refl = prep _ p
-  drop-mid′ (swap y z p) (w ∷ x ∷ ws) []           refl refl = prep _ (trans (↭-sym (shift _ _ _)) p)
-  drop-mid′ (swap y y p) (y ∷ [])     (y ∷ [])     refl refl = prep _ p
-  drop-mid′ (swap y z p) (y ∷ [])     (z ∷ y ∷ xs) refl refl = begin
+  drop-mid′ (swap y z p) []           (x ∷ [])     ≡.refl eq   | ≡.refl = prep _ p
+  drop-mid′ (swap y z p) []           (x ∷ _ ∷ xs) ≡.refl ≡.refl = prep _ (trans p (shift _ _ _))
+  drop-mid′ (swap y z p) (w ∷ [])     []           ≡.refl eq   with cong tail eq
+  drop-mid′ (swap y z p) (w ∷ [])     []           ≡.refl eq   | ≡.refl = prep _ p
+  drop-mid′ (swap y z p) (w ∷ x ∷ ws) []           ≡.refl ≡.refl = prep _ (trans (↭-sym (shift _ _ _)) p)
+  drop-mid′ (swap y y p) (y ∷ [])     (y ∷ [])     ≡.refl ≡.refl = prep _ p
+  drop-mid′ (swap y z p) (y ∷ [])     (z ∷ y ∷ xs) ≡.refl ≡.refl = begin
       _ ∷ _             <⟨ p ⟩
       _ ∷ (xs ++ _ ∷ _) <⟨ shift _ _ _ ⟩
       _ ∷ _ ∷ xs ++ _   <<⟨ refl ⟩
       _ ∷ _ ∷ xs ++ _   ∎
       where open PermutationReasoning
-  drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ [])     refl refl = begin
+  drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ [])     ≡.refl ≡.refl = begin
       _ ∷ _ ∷ ws ++ _   <<⟨ refl ⟩
       _ ∷ (_ ∷ ws ++ _) <⟨ ↭-sym (shift _ _ _) ⟩
       _ ∷ (ws ++ _ ∷ _) <⟨ p ⟩
       _ ∷ _             ∎
       where open PermutationReasoning
-  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)
+  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
 
@@ -234,13 +238,13 @@ drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs refl refl
 ++-identityˡ xs = refl
 
 ++-identityʳ : RightIdentity {A = List A} _↭_ [] _++_
-++-identityʳ xs = ↭-reflexive (Lₚ.++-identityʳ xs)
+++-identityʳ xs = ↭-reflexive (List.++-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)
+++-assoc xs ys zs = ↭-reflexive (List.++-assoc xs ys zs)
 
 ++-comm : Commutative {A = List A} _↭_ _++_
 ++-comm []       ys = ↭-sym (++-identityʳ ys)
@@ -318,7 +322,7 @@ 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 ++ []  ≡⟨ List.++-identityʳ _ ⟩
   x ∷ xs        ∎)
   where open PermutationReasoning
 
@@ -335,7 +339,7 @@ drop-∷ = drop-mid [] []
 ↭-reverse : (xs : List A) → reverse xs ↭ xs
 ↭-reverse [] = ↭-refl
 ↭-reverse (x ∷ xs) = begin
-  reverse (x ∷ xs) ≡⟨ Lₚ.unfold-reverse x xs ⟩
+  reverse (x ∷ xs) ≡⟨ List.unfold-reverse x xs ⟩
   reverse xs ∷ʳ x ↭⟨ ∷↭∷ʳ x (reverse xs) ⟨
   x ∷ reverse xs   ↭⟨ prep x (↭-reverse xs) ⟩
   x ∷ xs ∎
@@ -356,20 +360,31 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where
   ... | 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       ≡⟨ List.++-assoc [ x ] xs (y ∷ ys) ⟨
     x ∷ xs ++ y ∷ ys         ∎
     where open PermutationReasoning
 
+------------------------------------------------------------------------
+-- foldr of Commutative Monoid
+
+module _ (commutativeMonoid : CommutativeMonoid a r) where
+
+  open module CM = CommutativeMonoid commutativeMonoid
+
+  foldr-commMonoid : ∀ {xs ys} → xs ↭ ys → List.foldr _∙_ ε xs ≈ List.foldr _∙_ ε ys
+  foldr-commMonoid refl = CM.refl
+  foldr-commMonoid (prep x xs↭ys) = ∙-congˡ (foldr-commMonoid xs↭ys)
+  foldr-commMonoid (swap {xs} {ys} x 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  ≈⟨ 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)
+
 ------------------------------------------------------------------------
 -- product
 
 product-↭ : product Preserves _↭_ ⟶ _≡_
-product-↭ refl = refl
-product-↭ (prep x r) = cong (x *_) (product-↭ r)
-product-↭ (trans r s) = ≡.trans (product-↭ r) (product-↭ s)
-product-↭ (swap {xs} {ys} x y r) = begin
-  x * (y * product xs) ≡˘⟨ *-assoc x y (product xs) ⟩
-  (x * y) * product xs ≡⟨ cong₂ _*_ (*-comm x y) (product-↭ r) ⟩
-  (y * x) * product ys ≡⟨ *-assoc y x (product ys) ⟩
-  y * (x * product ys) ∎
-  where open ≡-Reasoning
+product-↭ = foldr-commMonoid *-1-commutativeMonoid
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
index 4409e78cc4..f630f546f4 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
@@ -19,16 +19,16 @@ 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)
-open import Data.List.Relation.Binary.Equality.Setoid S
+open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise)
+open import Data.List.Relation.Binary.Equality.Setoid S using (_≋_; ≋-refl; ≋-sym)
 open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 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
@@ -39,7 +39,7 @@ open Homogeneous public
 infix 3 _↭_
 
 _↭_ : Rel (List A) (a ⊔ ℓ)
-_↭_ = Homogeneous.Permutation _≈_
+_↭_ = Homogeneous.Permutation _≋_ _≈_
 
 ------------------------------------------------------------------------
 -- Constructor aliases
@@ -48,10 +48,10 @@ _↭_ = Homogeneous.Permutation _≈_
 -- swapped or prepended are propositionally equal
 
 ↭-prep : ∀ x {xs ys} → xs ↭ ys → x ∷ xs ↭ x ∷ ys
-↭-prep x xs↭ys = prep Eq.refl xs↭ys
+↭-prep x xs↭ys = prep ≈-refl xs↭ys
 
 ↭-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 x y xs↭ys = swap ≈-refl ≈-refl xs↭ys
 
 ------------------------------------------------------------------------
 -- Functions over permutations
@@ -65,23 +65,26 @@ steps (trans xs↭ys ys↭zs) = steps xs↭ys + steps ys↭zs
 ------------------------------------------------------------------------
 -- _↭_ is an equivalence
 
-↭-reflexive : _≡_ ⇒ _↭_
-↭-reflexive refl = refl (Pointwise.refl Eq.refl)
+↭-pointwise : _≋_ ⇒ _↭_
+↭-pointwise = refl
 
 ↭-refl : Reflexive _↭_
-↭-refl = ↭-reflexive refl
+↭-refl = ↭-pointwise ≋-refl
+
+↭-reflexive : _≡_ ⇒ _↭_
+↭-reflexive refl = ↭-refl
 
 ↭-sym : Symmetric _↭_
-↭-sym = Homogeneous.sym Eq.sym
+↭-sym = Homogeneous.sym ≋-sym ≈-sym
 
 ↭-trans : Transitive _↭_
-↭-trans = trans
+↭-trans = Homogeneous.trans
 
 ↭-isEquivalence : IsEquivalence _↭_
-↭-isEquivalence = Homogeneous.isEquivalence Eq.refl Eq.sym
+↭-isEquivalence = Homogeneous.isEquivalence ≋-refl ≋-sym ≈-sym
 
 ↭-setoid : Setoid _ _
-↭-setoid = Homogeneous.setoid {R = _≈_} Eq.refl Eq.sym
+↭-setoid = Homogeneous.setoid {PR = Pointwise _≈_} {R = _≈_} ≋-refl ≋-sym ≈-sym
 
 ------------------------------------------------------------------------
 -- A reasoning API to chain permutation proofs
@@ -95,7 +98,7 @@ module PermutationReasoning where
     renaming (≈-go to ↭-go)
 
   open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public
-  open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ refl) ≋-sym public
+  open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ ↭-pointwise) ≋-sym public
 
   -- Some extra combinators that allow us to skip certain elements
 
@@ -104,12 +107,12 @@ 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
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index 3af753e826..39d0f34778 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -16,7 +16,6 @@ module Data.List.Relation.Binary.Permutation.Setoid.Properties
   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.Relation.Binary.Pointwise as Pointwise
@@ -29,7 +28,7 @@ open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
 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
@@ -37,7 +36,7 @@ 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
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 open import Relation.Binary.Properties.Setoid S using (≉-resp₂)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_)
@@ -48,13 +47,15 @@ private
   variable
     b p r : Level
 
-open Setoid S using (_≈_) renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans)
+open Setoid S
+  using (_≈_)
+  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
+
 
 ------------------------------------------------------------------------
 -- Relationships to other predicates
@@ -98,7 +99,7 @@ Unique-resp-↭ = AllPairs-resp-↭ (_∘ ≈-sym) ≉-resp₂
 ------------------------------------------------------------------------
 
 ≋⇒↭ : _≋_ ⇒ _↭_
-≋⇒↭ = refl
+≋⇒↭ = ↭-pointwise
 
 ↭-respʳ-≋ : _↭_ Respectsʳ _≋_
 ↭-respʳ-≋ xs≋ys               (refl zs≋xs)         = refl (≋-trans zs≋xs xs≋ys)
@@ -165,6 +166,7 @@ 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        ∎
+  where open PermutationReasoning
 
 ↭-shift : ∀ {v} (xs ys : List A) → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
 ↭-shift = shift ≈-refl
@@ -188,13 +190,13 @@ 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)
@@ -202,6 +204,7 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin
   x ∷ xs ++ ys   <⟨ ++-comm xs ys ⟩
   x ∷ ys ++ xs   ↭⟨ ↭-shift ys xs ⟨
   ys ++ (x ∷ xs) ∎
+  where open PermutationReasoning
 
 -- Structures
 
@@ -266,6 +269,7 @@ shifts xs ys {zs} = begin
   (xs ++ ys) ++ zs ↭⟨ ++⁺ʳ zs (++-comm xs ys) ⟩
   (ys ++ xs) ++ zs ↭⟨ ++-assoc ys xs zs ⟩
    ys ++ xs  ++ zs ∎
+   where open PermutationReasoning
 
 dropMiddleElement-≋ : ∀ {x} ws xs {ys} {zs} →
            ws ++ [ x ] ++ ys ≋ xs ++ [ x ] ++ zs →
@@ -456,17 +460,23 @@ module _ {ℓ} {R : Rel A ℓ} (R? : B.Decidable R) where
   ... | 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       ≡⟨ List.++-assoc [ x ] xs (y ∷ ys) ⟨
     x ∷ xs ++ y ∷ ys         ∎
     where open PermutationReasoning
 
+------------------------------------------------------------------------
+-- _∷_
+
+drop-∷ : ∀ {x : A} {xs ys} → x ∷ xs ↭ x ∷ ys → xs ↭ ys
+drop-∷ = dropMiddleElement [] []
+
 ------------------------------------------------------------------------
 -- _∷ʳ_
 
 ∷↭∷ʳ : ∀ (x : A) xs → x ∷ xs ↭ xs ∷ʳ x
 ∷↭∷ʳ x xs = ↭-sym (begin
   xs ++ [ x ]   ↭⟨ ↭-shift xs [] ⟩
-  x ∷ xs ++ []  ≡⟨ Lₚ.++-identityʳ _ ⟩
+  x ∷ xs ++ []  ≡⟨ List.++-identityʳ _ ⟩
   x ∷ xs        ∎)
   where open PermutationReasoning
 
@@ -477,6 +487,18 @@ module _ {ℓ} {R : Rel A ℓ} (R? : B.Decidable R) where
 ++↭ʳ++ []       ys = ↭-refl
 ++↭ʳ++ (x ∷ xs) ys = ↭-trans (↭-sym (↭-shift xs ys)) (++↭ʳ++ xs (x ∷ ys))
 
+------------------------------------------------------------------------
+-- reverse
+
+↭-reverse : (xs : List A) → 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
+
 ------------------------------------------------------------------------
 -- foldr of Commutative Monoid
 
@@ -484,22 +506,20 @@ module _ {_∙_ : Op₂ A} {ε : A} (isCmonoid : IsCommutativeMonoid _≈_ _∙_
   open module CM = IsCommutativeMonoid isCmonoid
 
   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 (swap {xs} {ys} {x} {y} {x′} {y′} 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 setoid
   foldr-commMonoid (trans xs↭ys ys↭zs) = CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs)
diff --git a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
index 3e91679bb2..7fcb72ed58 100644
--- a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
@@ -24,6 +24,7 @@ open import Data.List.Membership.Propositional.Properties
 import Data.List.Relation.Binary.Subset.Setoid.Properties as Subset
 open import Data.List.Relation.Binary.Subset.Propositional
 open import Data.List.Relation.Binary.Permutation.Propositional
+  using (_↭_; ↭-sym; ↭-isEquivalence)
 import Data.List.Relation.Binary.Permutation.Propositional.Properties as Permutation
 open import Data.Nat using (ℕ; _≤_)
 import Data.Product.Base as Product
@@ -36,8 +37,8 @@ open import Relation.Nullary using (¬_; yes; no)
 open import Relation.Unary using (Decidable; Pred) renaming (_⊆_ to _⋐_)
 open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.Bundles using (Preorder)
-open import Relation.Binary.PropositionalEquality
-  using (_≡_; _≗_; isEquivalence; subst; resp; refl; setoid; module ≡-Reasoning)
+open import Relation.Binary.PropositionalEquality as ≡
+  using (_≡_; _≗_; isEquivalence; resp; refl; setoid; module ≡-Reasoning)
 import Relation.Binary.Reasoning.Preorder as ≲-Reasoning
 
 private
@@ -117,10 +118,10 @@ module ⊆-Reasoning (A : Set a) where
 ------------------------------------------------------------------------
 
 Any-resp-⊆ : ∀ {P : Pred A p} → (Any P) Respects _⊆_
-Any-resp-⊆ = Subset.Any-resp-⊆ (setoid _) (subst _)
+Any-resp-⊆ = Subset.Any-resp-⊆ (setoid _) (resp _)
 
 All-resp-⊇ : ∀ {P : Pred A p} → (All P) Respects _⊇_
-All-resp-⊇ = Subset.All-resp-⊇ (setoid _) (subst _)
+All-resp-⊇ = Subset.All-resp-⊇ (setoid _) (resp _)
 
 ------------------------------------------------------------------------
 -- Properties relating _⊆_ to various list functions
diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda
index fed89d7d45..f6414f2d65 100644
--- a/src/Data/Nat/Primality/Factorisation.agda
+++ b/src/Data/Nat/Primality/Factorisation.agda
@@ -8,7 +8,6 @@
 
 module Data.Nat.Primality.Factorisation where
 
-open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base
 open import Data.Nat.Divisibility
 open import Data.Nat.Properties
@@ -21,15 +20,17 @@ open import Data.List.Membership.Propositional.Properties using (∈-∃++)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (here; there)
 open import Data.List.Relation.Binary.Permutation.Propositional
-  using (_↭_; prep; swap; ↭-reflexive; ↭-refl; ↭-trans; refl; module PermutationReasoning)
-open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (product-↭; All-resp-↭; shift)
+  using (_↭_; ↭-refl; module PermutationReasoning)
+open import Data.List.Relation.Binary.Permutation.Propositional.Properties
+  using (product-↭; All-resp-↭; ↭-shift)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_$_; _∘_; _|>_; flip)
 open import Induction using (build)
 open import Induction.Lexicographic using (_⊗_; [_⊗_])
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; module ≡-Reasoning)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; sym; trans; cong; module ≡-Reasoning)
 
 private
   variable
@@ -139,7 +140,7 @@ factorisationHasAllPrimeFactors {a ∷ as} {p} pPrime p∣aΠas (aPrime ∷ asPr
 
 private
   factorisationUnique′ : (as bs : List ℕ) → product as ≡ product bs → All Prime as → All Prime bs → as ↭ bs
-  factorisationUnique′ [] [] Πas≡Πbs asPrime bsPrime = refl
+  factorisationUnique′ [] [] Πas≡Πbs asPrime bsPrime = ↭-refl
   factorisationUnique′ [] (b@(2+ _) ∷ bs) Πas≡Πbs prime[as] (_ ∷ prime[bs]) =
     contradiction Πas≡Πbs (<⇒≢ Πas<Πbs)
     where
@@ -163,8 +164,9 @@ private
         where open ≡-Reasoning
 
       shuffle : ∃[ bs′ ] bs ↭ a ∷ bs′
-      shuffle with ys , zs , p ← ∈-∃++ (factorisationHasAllPrimeFactors prime[a] a∣Πbs prime[bs])
-        = ys ++ zs , ↭-trans (↭-reflexive p) (shift a ys zs)
+      shuffle
+        with ys , zs , refl ← ∈-∃++ (factorisationHasAllPrimeFactors prime[a] a∣Πbs prime[bs])
+        = ys ++ zs , ↭-shift ys
 
       bs′ = proj₁ shuffle
       bs↭a∷bs′ = proj₂ shuffle