From 7ab1da5a9d67ff90c5fd5a8bf7b3d2c8b970194b Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 08:49:40 +0000
Subject: [PATCH 01/35] move `steps` towards deprecation in `Homogeneous`

---
 .../Relation/Binary/Permutation/Homogeneous.agda  | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
index 12015b3076..6e93c2f7ca 100644
--- a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
@@ -11,8 +11,8 @@ 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)
+import Data.List.Relation.Binary.Pointwise.Properties as 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)
@@ -59,3 +59,14 @@ 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)
+
+------------------------------------------------------------------------
+-- Steps moves here towards eventual deprecation, because it is
+-- * representation-dependent
+-- * now obsolete wrt `Setoid.Properties.{dropMiddleElement,split}`
+
+steps : ∀ {R : Rel A r} {xs ys} → 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

From 4ece6bbf67c79a2c6ca85f1dcdb31523ed9f07ec Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 08:51:17 +0000
Subject: [PATCH 02/35] deprecate `steps`; refactor `Setoid` proofs and
 equaiotnal reasoning combinators

---
 .../Relation/Binary/Permutation/Setoid.agda   | 84 +++++++++++++------
 1 file changed, 60 insertions(+), 24 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
index 4409e78cc4..bac92d5410 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
@@ -11,7 +11,7 @@ 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
@@ -21,14 +21,12 @@ 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.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 module ≈ = Setoid S using (_≈_) renaming (Carrier to A)
 
 ------------------------------------------------------------------------
 -- Definition
@@ -44,44 +42,66 @@ _↭_ = Homogeneous.Permutation _≈_
 ------------------------------------------------------------------------
 -- Constructor aliases
 
+-- Constructor alias
+
+↭-pointwise : _≋_ ⇒ _↭_
+↭-pointwise = refl
+
 -- These provide aliases for `swap` and `prep` when the elements being
 -- 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
-
-------------------------------------------------------------------------
--- Functions over permutations
-
-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
+↭-swap x y xs↭ys = swap ≈.refl ≈.refl xs↭ys
 
 ------------------------------------------------------------------------
 -- _↭_ is an equivalence
 
 ↭-reflexive : _≡_ ⇒ _↭_
-↭-reflexive refl = refl (Pointwise.refl Eq.refl)
+↭-reflexive refl = ↭-pointwise ≋-refl
 
 ↭-refl : Reflexive _↭_
 ↭-refl = ↭-reflexive refl
 
 ↭-sym : Symmetric _↭_
-↭-sym = Homogeneous.sym Eq.sym
+↭-sym = Homogeneous.sym ≈.sym
+
+↭-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 (≈.trans x≈y y≈z) (↭-transˡ-≋ xs≋ys ys↭zs)
+↭-transˡ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ ys↭zs)
+  = swap (≈.trans x≈y eq₁) (≈.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 (≈.trans x≈y y≈z) (↭-transʳ-≋ xs↭ys ys≋zs)
+↭-transʳ-≋ (swap eq₁ eq₂ xs↭ys) (x≈w ∷ y≈z ∷ ys≋zs)
+  = swap (≈.trans eq₁ y≈z) (≈.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)
 
 ↭-trans : Transitive _↭_
-↭-trans = trans
+↭-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
 
 ↭-isEquivalence : IsEquivalence _↭_
-↭-isEquivalence = Homogeneous.isEquivalence Eq.refl Eq.sym
+↭-isEquivalence = record
+    { refl  = ↭-refl
+    ; sym   = ↭-sym
+    ; trans = ↭-trans
+    }
 
 ↭-setoid : Setoid _ _
-↭-setoid = Homogeneous.setoid {R = _≈_} Eq.refl Eq.sym
+↭-setoid = record { isEquivalence = ↭-isEquivalence }
 
 ------------------------------------------------------------------------
 -- A reasoning API to chain permutation proofs
@@ -95,7 +115,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 +124,28 @@ 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
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.1
+
+steps : ∀ {xs ys} → xs ↭ ys → ℕ
+steps = Homogeneous.steps
+{-# WARNING_ON_USAGE steps
+"Warning: steps was deprecated in v2.1.
+Please use Homogeneous.steps explicitly instead."
+#-}
+

From 38f22e40598dfe65aa8f0cf62e38a807323d3209 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 09:41:14 +0000
Subject: [PATCH 03/35] extensive refactoring

---
 .../Binary/Permutation/Setoid/Properties.agda | 523 +++++++++---------
 1 file changed, 260 insertions(+), 263 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index 3af753e826..dc94f88022 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,24 @@ 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
+  using (_≋_; []; _∷_
+        ; ≋-refl; ≋-sym; ≋-trans
+        ; All-resp-≋; Any-resp-≋; AllPairs-resp-≋)
+
+private
+  variable
+    x y z v w : A
+    xs ys zs vs ws : List A
+    P : Pred A p
+    R : Rel A r
+
+  _++[_]++_ = λ xs (z : A) ys → xs ++ [ z ] ++ ys
 
 ------------------------------------------------------------------------
 -- Relationships to other predicates
@@ -94,84 +104,109 @@ Unique-resp-↭ : Unique Respects _↭_
 Unique-resp-↭ = AllPairs-resp-↭ (_∘ ≈-sym) ≉-resp₂
 
 ------------------------------------------------------------------------
--- Relationships to other relations
+-- Core properties depending on the representation of _↭_
 ------------------------------------------------------------------------
 
-≋⇒↭ : _≋_ ⇒ _↭_
-≋⇒↭ = refl
-
-↭-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ˡ-≋ : _↭_ 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
+shift : v ≈ w → ∀ xs ys → 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        ∎
+  where open PermutationReasoning
 
 ------------------------------------------------------------------------
--- Properties of steps
+-- Relationship to `_≋_`
 ------------------------------------------------------------------------
 
-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↭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ʳ : ∀ {xs ys zs} (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)
-
-------------------------------------------------------------------------
--- Properties of list functions
+↭-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
+  where
+    helper : ∀ as bs → 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)
+      = [] , _ , ≈-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 , ≈-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 , ≈-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 , ≈-trans x≈v v≈y ∷ eq , prep ≈-refl ↭
+    helper []           [] (swap _ _ _) (_ ∷ ())
+    helper []      (b ∷ _) (swap x≈v y≈w xs↭vs) (w≈z ∷ v≈y ∷ vs≋ys)
+      = b ∷ [] , _ , ≈-trans x≈v v≈y ∷ ≈-trans y≈w w≈z ∷ ≋-refl
+                   , ↭-prep b (↭-transʳ-≋ xs↭vs vs≋ys)
+    helper (a ∷ [])     bs (swap x≈v y≈w xs↭vs)  (w≈z ∷ v≈y ∷ vs≋ys)
+      = []     , a ∷ _ , ≈-trans x≈v v≈y ∷ ≈-trans y≈w w≈z ∷ ≋-refl
+                       , ↭-prep a (↭-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 , ≈-trans x≈v v≈b ∷ ≈-trans y≈w w≈a ∷ eq
+                        , ↭-swap _ _ ↭
+
+-----------------------------------------------------------
+-- Core properties of lists depending on the representation of _↭_
 ------------------------------------------------------------------------
 
 ------------------------------------------------------------------------
 -- 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⁺ : ∀ {f} → f Preserves _≈_ ⟶ _≈′_ → (map f) Preserves _↭_ ⟶ _↭′_
   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₂)
 
 ------------------------------------------------------------------------
--- _++_
+-- filter
 
-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        ∎
+module _ {p} {P : Pred A p} (P? : Decidable P) (P≈ : P Respects _≈_) where
 
-↭-shift : ∀ {v} (xs ys : List A) → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
-↭-shift = shift ≈-refl
+  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)
 
-++⁺ˡ : ∀ xs {ys zs : List A} → ys ↭ zs → xs ++ ys ↭ xs ++ zs
-++⁺ˡ []       ys↭zs = ys↭zs
-++⁺ˡ (x ∷ xs) ys↭zs = ↭-prep _ (++⁺ˡ xs ys↭zs)
+------------------------------------------------------------------------
+-- _++_
 
 ++⁺ʳ : ∀ {xs ys : List A} zs → xs ↭ ys → xs ++ zs ↭ ys ++ zs
 ++⁺ʳ zs (refl xs≋ys)  = refl (Pointwise.++⁺ xs≋ys ≋-refl)
@@ -179,8 +214,39 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin
 ++⁺ʳ zs (swap x y ↭)  = swap x y (++⁺ʳ zs ↭)
 ++⁺ʳ zs (trans ↭₁ ↭₂) = trans (++⁺ʳ zs ↭₁) (++⁺ʳ zs ↭₂)
 
+------------------------------------------------------------------------
+-- dropMiddleElement-≋
+
+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)
+
+------------------------------------------------------------------------
+-- Properties depending on the core properties of _↭_
+------------------------------------------------------------------------
+
+↭-shift : ∀ {v : A} xs ys → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
+↭-shift = shift ≈-refl
+
+++⁺ˡ : ∀ xs {ys zs} → ys ↭ zs → xs ++ ys ↭ xs ++ zs
+++⁺ˡ []       ys↭zs = ys↭zs
+++⁺ˡ (x ∷ xs) ys↭zs = ↭-prep _ (++⁺ˡ xs ys↭zs)
+
 ++⁺ : _++_ Preserves₂ _↭_ ⟶ _↭_ ⟶ _↭_
-++⁺ ws↭xs ys↭zs = trans (++⁺ʳ _ ws↭xs) (++⁺ˡ _ ys↭zs)
+++⁺ ws↭xs ys↭zs = ↭-trans (++⁺ʳ _ ws↭xs) (++⁺ˡ _ ys↭zs)
+
+-- Some other useful lemmas
+
+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 →
+         ws ++ [ v ] ++ xs ↭ ys ++ [ v ] ++ zs
+inject v ws↭ys xs↭zs = ↭-trans (++⁺ˡ _ (↭-prep _ xs↭zs)) (++⁺ʳ _ ws↭ys)
 
 -- Algebraic properties
 
@@ -188,13 +254,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 +268,17 @@ 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
+
+-- Corollary
+
+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
 
 -- Structures
 
@@ -251,123 +328,15 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin
   { isCommutativeMonoid = ++-isCommutativeMonoid
   }
 
--- Some other useful lemmas
-
-zoom : ∀ h {t xs ys : List A} → xs ↭ ys → h ++ xs ++ t ↭ h ++ ys ++ t
-zoom h {t} = ++⁺ˡ h ∘ ++⁺ʳ t
-
-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 _ xs↭zs)) (++⁺ʳ _ ws↭ys)
-
-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 ∎
-
-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)
+------------------------------------------------------------------------
+-- dropMiddleElelment, dropMiddle, and inversion for _∷_
 
 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)
+dropMiddleElement {v} ws xs {ys} {zs} p
+  with ps , qs , eq , ↭ ← ↭-split v xs zs p
+  = ↭-trans (dropMiddleElement-≋ ws ps eq) ↭
 
 dropMiddle : ∀ {vs} ws xs {ys zs} →
              ws ++ vs ++ ys ↭ xs ++ vs ++ zs →
@@ -375,64 +344,42 @@ dropMiddle : ∀ {vs} ws xs {ys 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 ↭₂))))
+drop-∷ : ∀ {x : A} {xs ys} → x ∷ xs ↭ x ∷ ys → xs ↭ ys
+drop-∷ = dropMiddleElement [] []
 
 ------------------------------------------------------------------------
--- filter
+-- _∷ʳ_
 
-module _ {p} {P : Pred A p} (P? : Decidable P) (P≈ : P Respects _≈_) where
+∷↭∷ʳ : ∀ (x : A) xs → x ∷ xs ↭ xs ∷ʳ x
+∷↭∷ʳ x xs = ↭-sym (begin
+  xs ++ [ x ]   ↭⟨ ↭-shift xs [] ⟩
+  x ∷ xs ++ []  ≡⟨ List.++-identityʳ _ ⟩
+  x ∷ xs        ∎)
+  where open PermutationReasoning
 
-  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)
+------------------------------------------------------------------------
+-- 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   ↭⟨ ↭-prep x (↭-reverse xs) ⟩
+  x ∷ xs           ∎
+  where open PermutationReasoning
+
+------------------------------------------------------------------------
+-- ʳ++
+
+++↭ʳ++ : ∀ (xs ys : List A) → xs ++ ys ↭ xs ʳ++ ys
+++↭ʳ++ []       ys = ↭-refl
+++↭ʳ++ (x ∷ xs) ys = ↭-trans (↭-sym (↭-shift xs ys)) (++↭ʳ++ xs (x ∷ ys))
 
 ------------------------------------------------------------------------
 -- 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-↭ []       = ↭-refl
@@ -444,7 +391,7 @@ module _ {p} {P : Pred A p} (P? : Decidable P) where
 ------------------------------------------------------------------------
 -- merge
 
-module _ {ℓ} {R : Rel A ℓ} (R? : B.Decidable R) where
+module _ (R? : B.Decidable R) where
 
   merge-↭ : ∀ xs ys → merge R? xs ys ↭ xs ++ ys
   merge-↭ []       []       = ↭-refl
@@ -456,50 +403,100 @@ 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
 
 ------------------------------------------------------------------------
--- _∷ʳ_
+-- foldr over a Commutative Monoid
 
-∷↭∷ʳ : ∀ (x : A) xs → x ∷ xs ↭ xs ∷ʳ x
-∷↭∷ʳ x xs = ↭-sym (begin
-  xs ++ [ x ]   ↭⟨ ↭-shift xs [] ⟩
-  x ∷ xs ++ []  ≡⟨ Lₚ.++-identityʳ _ ⟩
-  x ∷ xs        ∎)
-  where open PermutationReasoning
+module _{_∙_ : Op₂ A} {ε : A}
+        (isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε) where
 
-------------------------------------------------------------------------
--- ʳ++
+  private
+    commutativeMonoid : CommutativeMonoid _ _
+    commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
+    open module CM = CommutativeMonoid commutativeMonoid
+      using (∙-cong; ∙-congˡ; ∙-congʳ; assoc; comm)
+
+  foldr-pres-↭ : (foldr _∙_ ε) Preserves _↭_ ⟶ _≈_
+  foldr-pres-↭ (refl xs≋ys)        = Pointwise.foldr⁺ ∙-cong CM.refl xs≋ys
+  foldr-pres-↭ (prep x≈y xs↭ys)    = ∙-cong x≈y (foldr-pres-↭ xs↭ys)
+  foldr-pres-↭ (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = begin
+    x ∙ (y ∙ foldr _∙_ ε xs)    ≈⟨ ∙-congˡ (∙-congˡ (foldr-pres-↭ 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-pres-↭ (trans xs↭ys ys↭zs) = CM.trans (foldr-pres-↭ xs↭ys) (foldr-pres-↭ ys↭zs)
 
-++↭ʳ++ : ∀ (xs ys : List A) → xs ++ ys ↭ xs ʳ++ ys
-++↭ʳ++ []       ys = ↭-refl
-++↭ʳ++ (x ∷ xs) ys = ↭-trans (↭-sym (↭-shift xs ys)) (++↭ʳ++ xs (x ∷ ys))
 
 ------------------------------------------------------------------------
--- foldr of Commutative Monoid
+-- TOWARDS DEPRECATION
+------------------------------------------------------------------------
 
-module _ {_∙_ : Op₂ A} {ε : A} (isCmonoid : IsCommutativeMonoid _≈_ _∙_ ε) where
-  open module CM = IsCommutativeMonoid isCmonoid
+≋⇒↭ = ↭-pointwise
 
-  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)
+-- These are easily superseded by ↭-transˡ-≋, ↭-transʳ-≋
+-- But for the properties of steps which require precise measurement
+
+↭-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ˡ-≋ : _↭_ 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
+
+-- Properties of steps using the above
+
+0<steps : (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ˡ : (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ʳ : (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)
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.1
+
+split : ∀ (v : A) as bs {xs} → xs ↭ as ++ [ v ] ++ bs →
+        ∃₂ λ ps qs → xs ≋ ps ++ [ v ] ++ qs
+split v as bs xs↭as++[v]++bs
+  with ps , qs , eq , _ ← ↭-split v as bs xs↭as++[v]++bs
+  = ps , qs , eq
+{-# WARNING_ON_USAGE split
+"Warning: split was deprecated in v2.1.
+Please use the sharper lemma ↭-split instead."
+#-}
+
+foldr-commMonoid = foldr-pres-↭
+{-# WARNING_ON_USAGE foldr-commMonoid
+"Warning: foldr-commMonoid was deprecated in v2.1.
+Please use foldr-pres-↭ instead."
+#-}

From 9399636f8d856192cee8686c6d973588c199ac0e Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 10:10:30 +0000
Subject: [PATCH 04/35] tidy up

---
 .../Binary/Permutation/Setoid/Properties.agda | 22 +++++++++----------
 1 file changed, 10 insertions(+), 12 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index dc94f88022..4d84f22cf7 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -43,9 +43,6 @@ open import Relation.Binary.PropositionalEquality.Core as ≡
 open import Relation.Nullary.Decidable using (yes; no; does)
 open import Relation.Nullary.Negation using (contradiction)
 
-private
-  variable
-    b p r : Level
 
 open Setoid S using (_≈_)
   renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans)
@@ -59,6 +56,7 @@ open module ≋ = Equality S
 
 private
   variable
+    b p r : Level
     x y z v w : A
     xs ys zs vs ws : List A
     P : Pred A p
@@ -70,13 +68,13 @@ private
 -- Relationships to other predicates
 ------------------------------------------------------------------------
 
-All-resp-↭ : ∀ {P : Pred A p} → P Respects _≈_ → (All P) Respects _↭_
+All-resp-↭ : 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-↭ : 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)
@@ -85,7 +83,7 @@ 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-↭ : 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) ∼) ∷
@@ -97,7 +95,7 @@ AllPairs-resp-↭ sym resp@(rʳ , rˡ) (swap eq₁ eq₂ p) ((∼₁ ∷ ∼₂)
 AllPairs-resp-↭ sym resp (trans p₁ p₂)    pxs             =
   AllPairs-resp-↭ sym resp p₂ (AllPairs-resp-↭ sym resp p₁ pxs)
 
-∈-resp-↭ : ∀ {x} → (x ∈_) Respects _↭_
+∈-resp-↭ : (x ∈_) Respects _↭_
 ∈-resp-↭ = Any-resp-↭ (flip ≈-trans)
 
 Unique-resp-↭ : Unique Respects _↭_
@@ -173,7 +171,7 @@ module _ (T : Setoid b r) where
 ------------------------------------------------------------------------
 -- filter
 
-module _ {p} {P : Pred A p} (P? : Decidable P) (P≈ : P Respects _≈_) where
+module _ (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)
@@ -208,7 +206,7 @@ module _ {p} {P : Pred A p} (P? : Decidable P) (P≈ : P Respects _≈_) where
 ------------------------------------------------------------------------
 -- _++_
 
-++⁺ʳ : ∀ {xs ys : List A} zs → xs ↭ ys → xs ++ zs ↭ ys ++ zs
+++⁺ʳ : ∀ 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 ↭)
@@ -229,7 +227,7 @@ dropMiddleElement-≋ (w ∷ ws) (x ∷ xs) (w≈x ∷ eq) = prep w≈x (dropMid
 -- Properties depending on the core properties of _↭_
 ------------------------------------------------------------------------
 
-↭-shift : ∀ {v : A} xs ys → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
+↭-shift : ∀ {v} xs ys → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
 ↭-shift = shift ≈-refl
 
 ++⁺ˡ : ∀ xs {ys zs} → ys ↭ zs → xs ++ ys ↭ xs ++ zs
@@ -244,7 +242,7 @@ dropMiddleElement-≋ (w ∷ ws) (x ∷ xs) (w≈x ∷ eq) = prep w≈x (dropMid
 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)
 
@@ -344,7 +342,7 @@ dropMiddle : ∀ {vs} ws xs {ys zs} →
 dropMiddle {[]}     ws xs p = p
 dropMiddle {v ∷ vs} ws xs p = dropMiddle ws xs (dropMiddleElement ws xs p)
 
-drop-∷ : ∀ {x : A} {xs ys} → x ∷ xs ↭ x ∷ ys → xs ↭ ys
+drop-∷ : x ∷ xs ↭ x ∷ ys → xs ↭ ys
 drop-∷ = dropMiddleElement [] []
 
 ------------------------------------------------------------------------

From c6f701ffb3e892044c090ead53cfb65390a2e3d6 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 10:11:12 +0000
Subject: [PATCH 05/35] add equivalence with `Setoid` representation

---
 .../Binary/Permutation/Propositional.agda     | 53 +++++++++++++++----
 1 file changed, 43 insertions(+), 10 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional.agda b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
index c41793d28a..113a655508 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
@@ -10,14 +10,22 @@ 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)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; refl)
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 open import Relation.Binary.Reasoning.Syntax
 
+import Data.List.Relation.Binary.Permutation.Setoid as Permutation
+
+private
+  variable
+    x y z v w : A
+    ws xs ys zs : List A
+
 ------------------------------------------------------------------------
 -- An inductive definition of permutation
 
@@ -30,20 +38,23 @@ open import Relation.Binary.Reasoning.Syntax
 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
+  refl  : xs ↭ xs
+  prep  : ∀ x → xs ↭ ys → x ∷ xs ↭ x ∷ ys
+  swap  : ∀ x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
+  trans : xs ↭ ys → ys ↭ zs → xs ↭ zs
 
 ------------------------------------------------------------------------
 -- _↭_ is an equivalence
 
-↭-reflexive : _≡_ ⇒ _↭_
-↭-reflexive refl = refl
-
 ↭-refl : Reflexive _↭_
 ↭-refl = refl
 
+↭-reflexive : _≡_ ⇒ _↭_
+↭-reflexive refl = ↭-refl
+
+↭-pointwise : _≋_ ⇒ _↭_
+↭-pointwise xs≋ys = ↭-reflexive (≋⇒≡ xs≋ys)
+
 ↭-sym : ∀ {xs ys} → xs ↭ ys → ys ↭ xs
 ↭-sym refl                = refl
 ↭-sym (prep x xs↭ys)      = prep x (↭-sym xs↭ys)
@@ -68,6 +79,28 @@ data _↭_ : Rel (List A) a where
   { isEquivalence = ↭-isEquivalence
   }
 
+------------------------------------------------------------------------
+-- _↭_ is equivalent to `Setoid`-based permutation
+
+private
+  open module ↭ₛ = Permutation (≡.setoid A)
+    using ()
+    renaming (_↭_ to _↭ₛ_)
+
+↭⇒↭ₛ : xs ↭ ys → xs ↭ₛ ys
+↭⇒↭ₛ refl         = ↭ₛ.↭-refl
+↭⇒↭ₛ (prep x p)   = ↭ₛ.↭-prep x (↭⇒↭ₛ p)
+↭⇒↭ₛ (swap x y p) = ↭ₛ.↭-swap x y (↭⇒↭ₛ p)
+↭⇒↭ₛ (trans p q)  = ↭ₛ.↭-trans (↭⇒↭ₛ p) (↭⇒↭ₛ q)
+
+
+↭ₛ⇒↭ : _↭ₛ_ ⇒ _↭_
+↭ₛ⇒↭ (↭ₛ.refl xs≋ys)       = ↭-pointwise xs≋ys
+↭ₛ⇒↭ (↭ₛ.prep refl p)      = prep _ (↭ₛ⇒↭ p)
+↭ₛ⇒↭ (↭ₛ.swap refl refl p) = swap _ _ (↭ₛ⇒↭ p)
+↭ₛ⇒↭ (↭ₛ.trans p q)        = ↭-trans (↭ₛ⇒↭ p) (↭ₛ⇒↭ q)
+
+
 ------------------------------------------------------------------------
 -- A reasoning API to chain permutation proofs and allow "zooming in"
 -- to localised reasoning.
@@ -89,12 +122,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

From b37ba6f5ecb495a72fa7a818e3358aa58e78f1dd Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 11:38:45 +0000
Subject: [PATCH 06/35] removed buggy `PermutationReasoning` syntax

---
 .../Relation/Binary/Permutation/Setoid/Properties.agda    | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index 4d84f22cf7..94b9e9b67a 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -108,8 +108,8 @@ Unique-resp-↭ = AllPairs-resp-↭ (_∘ ≈-sym) ≉-resp₂
 shift : v ≈ w → ∀ xs ys → 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 ⟩
+  x ∷ (xs ++ [ v ] ++ ys) ↭⟨ ↭-prep x (shift v≈w xs ys) ⟩
+  x ∷ w ∷ xs ++ ys        ↭⟨ ↭-swap x w ↭-refl ⟩
   w ∷ x ∷ xs ++ ys        ∎
   where open PermutationReasoning
 
@@ -263,7 +263,7 @@ inject v ws↭ys xs↭zs = ↭-trans (++⁺ˡ _ (↭-prep _ xs↭zs)) (++⁺ʳ _
 ++-comm : Commutative _↭_ _++_
 ++-comm []       ys = ↭-sym (++-identityʳ ys)
 ++-comm (x ∷ xs) ys = begin
-  x ∷ xs ++ ys   <⟨ ++-comm xs ys ⟩
+  x ∷ xs ++ ys   ↭⟨ ↭-prep x (++-comm xs ys) ⟩
   x ∷ ys ++ xs   ↭⟨ ↭-shift ys xs ⟨
   ys ++ (x ∷ xs) ∎
   where open PermutationReasoning
@@ -399,7 +399,7 @@ module _ (R? : B.Decidable R) where
     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 ∷ merge R? (x ∷ xs) ys ↭⟨ ↭-prep _ rec ⟩
     y ∷ x ∷ xs ++ ys         ↭⟨ ↭-shift (x ∷ xs) ys ⟨
     (x ∷ xs) ++ y ∷ ys       ≡⟨ List.++-assoc [ x ] xs (y ∷ ys) ⟨
     x ∷ xs ++ y ∷ ys         ∎

From 791baf9d8335882bd877e4a55ab12fe8d8197f65 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 11:40:02 +0000
Subject: [PATCH 07/35] refactored; removed buggy `PermutationReasoning` syntax

---
 .../Permutation/Propositional/Properties.agda | 127 +++++++++---------
 1 file changed, 61 insertions(+), 66 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index d56bdb7fb3..e6828e5852 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -12,16 +12,16 @@ 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.Product.Base using (-,_; proj₂)
+open import Data.Nat.Base using (ℕ; suc)
+import Data.Nat.Properties as ℕ
+open import Data.Product.Base using (-,_)
 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.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)
@@ -33,6 +33,8 @@ open import Relation.Binary.PropositionalEquality.Core as ≡
 open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning)
 open import Relation.Nullary
 
+import Data.List.Relation.Binary.Permutation.Setoid.Properties as Permutation
+
 private
   variable
     a b p : Level
@@ -169,64 +171,62 @@ inject v ws↭ys xs↭zs = trans (++⁺ˡ _ (prep v xs↭zs)) (++⁺ʳ _ ws↭ys
 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 ⟩
+  x ∷ (xs ++ [ v ] ++ ys) ↭⟨ prep _ (shift v xs ys) ⟩
+  x ∷ v ∷ xs ++ ys        ↭⟨ swap _ _ refl ⟩
   v ∷ x ∷ xs ++ ys        ∎
   where open PermutationReasoning
 
 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-≡ []       []       eq
+  with refl ← List.∷-injectiveʳ eq = 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-≡ (w ∷ ws) (x ∷ xs) eq
+  with refl , eq′ ← List.∷-injective 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
-  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 _}
-                                                                       (λ { (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
-      _ ∷ _             <⟨ p ⟩
-      _ ∷ (xs ++ _ ∷ _) <⟨ shift _ _ _ ⟩
-      _ ∷ _ ∷ xs ++ _   <<⟨ refl ⟩
-      _ ∷ _ ∷ xs ++ _   ∎
-      where open PermutationReasoning
-  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′ : ∀ {as bs} → as ↭ bs →
+            ∀ {x : A} ws xs {ys zs} →
+            as ≡ ws ++ [ x ] ++ ys →
+            bs ≡ xs ++ [ x ] ++ zs →
+            ws ++ ys ↭ xs ++ zs
+drop-mid ws xs p = drop-mid′ p ws xs refl refl
+drop-mid′ refl ws xs refl eq = drop-mid-≡ ws xs eq
+drop-mid′ (trans p q) ws  xs refl refl
+  with h , t , refl ← ∈-∃++ (∈-resp-↭ p (∈-insert ws))
+  = trans (drop-mid ws h p) (drop-mid h xs q)
+drop-mid′ (prep x p)   []           []           refl eq
+  with refl ← List.∷-injectiveʳ 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 ws xs p)
+drop-mid′ (swap y z p) []           []           refl refl = prep _ p
+drop-mid′ (swap y z p) []           (x ∷ [])     refl eq
+  with refl , eq′ ← List.∷-injective eq
+  with refl ← List.∷-injectiveʳ eq′ = 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 refl ← List.∷-injectiveʳ eq  = 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
+    _ ∷ _             ↭⟨ prep _ p ⟩
+    _ ∷ (xs ++ _ ∷ _) ↭⟨ prep _ (shift _ _ _) ⟩
+    _ ∷ _ ∷ xs ++ _   ↭⟨ swap _ _ refl ⟩
+    _ ∷ _ ∷ xs ++ _   ∎
+    where open PermutationReasoning
+drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ [])     refl refl = begin
+    _ ∷ _ ∷ ws ++ _   ↭⟨ swap _ _ refl ⟩
+    _ ∷ (_ ∷ ws ++ _) ↭⟨ prep _ (shift _ _ _) ⟨
+    _ ∷ (ws ++ _ ∷ _) ↭⟨ prep _ p ⟩
+    _ ∷ _             ∎
+    where open PermutationReasoning
+drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ y ∷ xs) refl refl = swap y z (drop-mid _ _ p)
+
 
 -- Algebraic properties
 
@@ -234,18 +234,18 @@ 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)
 ++-comm (x ∷ xs) ys = begin
-  x ∷ xs ++ ys   <⟨ ++-comm xs ys ⟩
+  x ∷ xs ++ ys   ↭⟨ prep _ (++-comm xs ys) ⟩
   x ∷ ys ++ xs   ↭⟨ shift x ys xs ⟨
   ys ++ (x ∷ xs) ∎
   where open PermutationReasoning
@@ -318,7 +318,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 +335,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 ∎
@@ -354,9 +354,9 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where
     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 ∷ merge R? (x ∷ xs) ys ↭⟨ prep _ 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
 
@@ -364,12 +364,7 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where
 -- 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-↭ p = foldr-pres-↭ ℕ-*-1.isCommutativeMonoid (↭⇒↭ₛ p)
+  where
+  module ℕ-*-1 = CommutativeMonoid ℕ.*-1-commutativeMonoid
+  open Permutation ℕ-*-1.setoid

From ff7845a2475e759a0049334b919d80be49e76f7d Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 11:42:17 +0000
Subject: [PATCH 08/35] `CHANGELOG`

---
 CHANGELOG.md | 40 ++++++++++++++++++++++++++++++++++++++--
 1 file changed, 38 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2b9d357511..b23f9c3acc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -49,9 +49,18 @@ Deprecated names
   _-_  ↦  _//_
   ```
 
-* In `Data.Nat.Divisibility.Core`:
+* In `Data.List.Relation.Binary.Permutation.Setoid`:
   ```agda
-  *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
+  steps  ↦  Data.List.Relation.Binary.Permutation.Homogeneous.steps
+  ```
+
+* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
+  ```agda
+  split  ↦  ↭-split
+        ```
+  with a more informative type, and a simple renaming
+  ```agda
+  foldr-commMonoid  ↦  foldr-pres-↭
   ```
 
 New modules
@@ -262,6 +271,33 @@ Additions to existing modules
   reverse-downFrom      : reverse (downFrom n) ≡ upTo n
   ```
 
+* In `Data.List.Relation.Binary.Permutation.Homogeneous`:
+  ```agda
+  steps : Permutation R xs ys → ℕ
+  ```
+
+* In `Data.List.Relation.Binary.Permutation.Propositional`:
+  ```agda
+  steps : Permutation R xs ys → ℕ
+  ```
+
+* In `Data.List.Relation.Binary.Permutation.Setoid`:
+  ```agda
+  ↭-pointwise : _≋_ ⇒ _↭_
+  ↭⇒↭ₛ        : _↭_ ⇒ _↭ₛ_
+  ↭ₛ⇒↭        : _↭ₛ_ ⇒ _↭_
+  ```
+  where `_↭ₛ_` is the `Setoid (setoid _)` instance of `Permutation`
+
+* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
+  ```agda
+  ↭-split : xs ↭ (as ++[ v ]++ bs) →
+            ∃₂ λ ps qs → xs ≋ (ps ++[ v ]++ qs) × (ps ++ qs) ↭ (as ++ bs)
+  drop-∷  : x ∷ xs ↭ x ∷ ys → xs ↭ ys
+
+  foldr-pres-↭ : (IsCommutativeMonoid _≈_ _∙_ ε) → (foldr _∙_ ε) Preserves _↭_ ⟶ _≈_
+  ```
+
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
   All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs)

From a3d0b8eaff1c315da85fa3baff8191b7d9fd0e1f Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 12:08:14 +0000
Subject: [PATCH 09/35] final fix-ups

---
 CHANGELOG.md                                  | 14 +++--
 .../Binary/Permutation/Setoid/Properties.agda | 60 +++++++++----------
 2 files changed, 38 insertions(+), 36 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b23f9c3acc..43057e052b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -57,7 +57,7 @@ Deprecated names
 * In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
   ```agda
   split  ↦  ↭-split
-        ```
+  ```
   with a more informative type, and a simple renaming
   ```agda
   foldr-commMonoid  ↦  foldr-pres-↭
@@ -278,16 +278,18 @@ Additions to existing modules
 
 * In `Data.List.Relation.Binary.Permutation.Propositional`:
   ```agda
-  steps : Permutation R xs ys → ℕ
+  ↭-pointwise : _≋_ ⇒ _↭_
+  ↭⇒↭ₛ        : _↭_  ⇒ _↭ₛ_
+  ↭ₛ⇒↭        : _↭ₛ_ ⇒ _↭_
   ```
+  where `_↭ₛ_` is the `Setoid (setoid _)` instance of `Permutation`
 
 * In `Data.List.Relation.Binary.Permutation.Setoid`:
   ```agda
-  ↭-pointwise : _≋_ ⇒ _↭_
-  ↭⇒↭ₛ        : _↭_ ⇒ _↭ₛ_
-  ↭ₛ⇒↭        : _↭ₛ_ ⇒ _↭_
+  ↭-pointwise : _≋_  ⇒ _↭_
+  ↭-transˡ-≋  : LeftTrans _≋_ _↭_
+  ↭-transʳ-≋  : RightTrans _↭_ _≋_
   ```
-  where `_↭ₛ_` is the `Setoid (setoid _)` instance of `Permutation`
 
 * In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
   ```agda
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index 94b9e9b67a..b4060eeece 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -122,35 +122,35 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin
                      × (ps ++ qs) ↭ (as ++ bs)
 ↭-split v as bs p = helper as bs p ≋-refl
   where
-    helper : ∀ as bs → 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)
-      = [] , _ , ≈-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 , ≈-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 , ≈-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 , ≈-trans x≈v v≈y ∷ eq , prep ≈-refl ↭
-    helper []           [] (swap _ _ _) (_ ∷ ())
-    helper []      (b ∷ _) (swap x≈v y≈w xs↭vs) (w≈z ∷ v≈y ∷ vs≋ys)
-      = b ∷ [] , _ , ≈-trans x≈v v≈y ∷ ≈-trans y≈w w≈z ∷ ≋-refl
-                   , ↭-prep b (↭-transʳ-≋ xs↭vs vs≋ys)
-    helper (a ∷ [])     bs (swap x≈v y≈w xs↭vs)  (w≈z ∷ v≈y ∷ vs≋ys)
-      = []     , a ∷ _ , ≈-trans x≈v v≈y ∷ ≈-trans y≈w w≈z ∷ ≋-refl
-                       , ↭-prep a (↭-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 , ≈-trans x≈v v≈b ∷ ≈-trans y≈w w≈a ∷ eq
-                        , ↭-swap _ _ ↭
-
------------------------------------------------------------
+  helper : ∀ as bs → 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)
+    = [] , _ , ≈-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 , ≈-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 , ≈-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 , ≈-trans x≈v v≈y ∷ eq , prep ≈-refl ↭
+  helper []           [] (swap _ _ _) (_ ∷ ())
+  helper []      (b ∷ _) (swap x≈v y≈w xs↭vs) (w≈z ∷ v≈y ∷ vs≋ys)
+    = b ∷ [] , _ , ≈-trans x≈v v≈y ∷ ≈-trans y≈w w≈z ∷ ≋-refl
+                 , ↭-prep b (↭-transʳ-≋ xs↭vs vs≋ys)
+  helper (a ∷ [])     bs (swap x≈v y≈w xs↭vs)  (w≈z ∷ v≈y ∷ vs≋ys)
+    = []     , a ∷ _ , ≈-trans x≈v v≈y ∷ ≈-trans y≈w w≈z ∷ ≋-refl
+                     , ↭-prep a (↭-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 , ≈-trans x≈v v≈b ∷ ≈-trans y≈w w≈a ∷ eq
+                      , ↭-swap _ _ ↭
+
+------------------------------------------------------------------------
 -- Core properties of lists depending on the representation of _↭_
 ------------------------------------------------------------------------
 
@@ -327,7 +327,7 @@ shifts xs ys {zs} = begin
   }
 
 ------------------------------------------------------------------------
--- dropMiddleElelment, dropMiddle, and inversion for _∷_
+-- dropMiddleElement, dropMiddle, and inversion for _∷_
 
 dropMiddleElement : ∀ {v} ws xs {ys zs} →
                     ws ++ [ v ] ++ ys ↭ xs ++ [ v ] ++ zs →

From 2950a394bba8f35f50134a64557cd6520ab10d4d Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 12:42:00 +0000
Subject: [PATCH 10/35] tighten `import`s

---
 src/Data/Nat/Primality/Factorisation.agda | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda
index 6dda6bac9d..ce53d79991 100644
--- a/src/Data/Nat/Primality/Factorisation.agda
+++ b/src/Data/Nat/Primality/Factorisation.agda
@@ -21,15 +21,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 +141,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,18 +165,19 @@ 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 a ys zs
 
       bs′ = proj₁ shuffle
       bs↭a∷bs′ = proj₂ shuffle
 
       Πas≡Πbs′ : product as ≡ product bs′
-      Πas≡Πbs′ = *-cancelˡ-≡ (product as) (product bs′) a {{prime⇒nonZero prime[a]}} $ begin
+      Πas≡Πbs′ = *-cancelˡ-≡ (product as) (product bs′) a $ begin
         a * product as  ≡⟨ Πas≡Πbs ⟩
         product bs      ≡⟨ product-↭ bs↭a∷bs′ ⟩
         a * product bs′ ∎
-        where open ≡-Reasoning
+        where open ≡-Reasoning ; instance _ = prime⇒nonZero prime[a]
 
       prime[bs'] : All Prime bs′
       prime[bs'] = All.tail (All-resp-↭ bs↭a∷bs′ prime[bs])

From 69ca8fda491bb6d88836a0e13304dc67f23871a7 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 12:48:45 +0000
Subject: [PATCH 11/35] tighten `import`s

---
 src/Data/List/Relation/Binary/Permutation/Setoid.agda | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
index bac92d5410..cb9e82b5a0 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
@@ -21,7 +21,6 @@ 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.Nat.Base using (ℕ)
 open import Level using (_⊔_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
@@ -142,8 +141,7 @@ module PermutationReasoning where
 
 -- Version 2.1
 
-steps : ∀ {xs ys} → xs ↭ ys → ℕ
-steps = Homogeneous.steps
+steps = Homogeneous.steps {R = _≈_}
 {-# WARNING_ON_USAGE steps
 "Warning: steps was deprecated in v2.1.
 Please use Homogeneous.steps explicitly instead."

From 5f0051af853dcf068dd3976c13f1d63d9296e90f Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 13:24:43 +0000
Subject: [PATCH 12/35] redundant constructor aliases

---
 CHANGELOG.md                                  |  7 +++++++
 .../Binary/Permutation/Propositional.agda     | 20 +++++++++++++------
 2 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 43057e052b..0d1dcf54c5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -277,6 +277,13 @@ Additions to existing modules
   ```
 
 * In `Data.List.Relation.Binary.Permutation.Propositional`:
+  constructor aliases
+  ```agda
+  ↭-refl  : Reflexive _↭_
+  ↭-prep  : ∀ x → xs ↭ ys → x ∷ xs ↭ x ∷ ys
+  ↭-swap  : ∀ x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
+  ```
+  and properties
   ```agda
   ↭-pointwise : _≋_ ⇒ _↭_
   ↭⇒↭ₛ        : _↭_  ⇒ _↭ₛ_
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional.agda b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
index 113a655508..b6abdb98c8 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
@@ -43,19 +43,27 @@ data _↭_ : Rel (List A) a where
   swap  : ∀ x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
   trans : xs ↭ ys → ys ↭ zs → xs ↭ zs
 
-------------------------------------------------------------------------
--- _↭_ is an equivalence
+-- Constructor aliases
 
 ↭-refl : Reflexive _↭_
 ↭-refl = refl
 
+↭-prep  : ∀ x → xs ↭ ys → x ∷ xs ↭ x ∷ ys
+↭-prep = prep
+
+↭-swap  : ∀ x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
+↭-swap = swap
+
+------------------------------------------------------------------------
+-- _↭_ is an equivalence
+
 ↭-reflexive : _≡_ ⇒ _↭_
 ↭-reflexive refl = ↭-refl
 
 ↭-pointwise : _≋_ ⇒ _↭_
 ↭-pointwise xs≋ys = ↭-reflexive (≋⇒≡ xs≋ys)
 
-↭-sym : ∀ {xs ys} → xs ↭ ys → ys ↭ xs
+↭-sym : 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)
@@ -69,7 +77,7 @@ data _↭_ : Rel (List A) a where
 
 ↭-isEquivalence : IsEquivalence _↭_
 ↭-isEquivalence = record
-  { refl  = refl
+  { refl  = ↭-refl
   ; sym   = ↭-sym
   ; trans = ↭-trans
   }
@@ -96,8 +104,8 @@ private
 
 ↭ₛ⇒↭ : _↭ₛ_ ⇒ _↭_
 ↭ₛ⇒↭ (↭ₛ.refl xs≋ys)       = ↭-pointwise xs≋ys
-↭ₛ⇒↭ (↭ₛ.prep refl p)      = prep _ (↭ₛ⇒↭ p)
-↭ₛ⇒↭ (↭ₛ.swap refl refl p) = swap _ _ (↭ₛ⇒↭ p)
+↭ₛ⇒↭ (↭ₛ.prep refl p)      = ↭-prep _ (↭ₛ⇒↭ p)
+↭ₛ⇒↭ (↭ₛ.swap refl refl p) = ↭-swap _ _ (↭ₛ⇒↭ p)
 ↭ₛ⇒↭ (↭ₛ.trans p q)        = ↭-trans (↭ₛ⇒↭ p) (↭ₛ⇒↭ q)
 
 

From 5461356cc53e5903506cfc139157d34d4805d820 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 13:26:35 +0000
Subject: [PATCH 13/35] fix-up `Reasoning` steps with the alias

---
 src/Data/Nat/Primality/Factorisation.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda
index ce53d79991..06438eb8d0 100644
--- a/src/Data/Nat/Primality/Factorisation.agda
+++ b/src/Data/Nat/Primality/Factorisation.agda
@@ -21,7 +21,7 @@ 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 (_↭_; ↭-refl; module PermutationReasoning)
+  using (_↭_; ↭-refl; ↭-prep; module PermutationReasoning)
 open import Data.List.Relation.Binary.Permutation.Propositional.Properties
   using (product-↭; All-resp-↭; shift)
 open import Data.Sum.Base using (inj₁; inj₂)
@@ -184,7 +184,7 @@ private
 
       a∷as↭bs : a ∷ as ↭ bs
       a∷as↭bs = begin
-        a ∷ as  <⟨ factorisationUnique′ as bs′ Πas≡Πbs′ prime[as] prime[bs'] ⟩
+        a ∷ as  ↭⟨ ↭-prep a (factorisationUnique′ as bs′ Πas≡Πbs′ prime[as] prime[bs']) ⟩
         a ∷ bs′ ↭⟨ bs↭a∷bs′ ⟨
         bs      ∎
         where open PermutationReasoning

From 8b44fd8d068dd2e4fba81206d97001da7954db8f Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 13:51:48 +0000
Subject: [PATCH 14/35] use aliases

---
 src/Data/List/Relation/Binary/Permutation/Propositional.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional.agda b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
index b6abdb98c8..83d3142c6e 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
@@ -130,12 +130,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 = ↭-go (prep x xs↭ys) 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 = ↭-go (swap x y xs↭ys) 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

From 7918a8dd5783f7c8e0dff519c1cb3a0a4cfacd9f Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 14:05:48 +0000
Subject: [PATCH 15/35] more `import` tightening

---
 .../List/Relation/Binary/Permutation/Setoid.agda | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
index cb9e82b5a0..35717745ca 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
@@ -6,26 +6,26 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-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; LeftTrans; RightTrans)
-open import Relation.Binary.Reasoning.Syntax
 
 module Data.List.Relation.Binary.Permutation.Setoid
   {a ℓ} (S : Setoid a ℓ) where
 
 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
+import Data.List.Relation.Binary.Equality.Setoid as ≋
+open import Function.Base using (_∘′_)
 open import Level using (_⊔_)
+open import Relation.Binary.Core using (Rel; _⇒_)
+open import Relation.Binary.Definitions
+  using (Reflexive; Symmetric; Transitive; LeftTrans; RightTrans)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+open import Relation.Binary.Reasoning.Syntax
+open import Relation.Binary.Structures using (IsEquivalence)
 
 open module ≈ = Setoid S using (_≈_) renaming (Carrier to A)
+open ≋ S using (_≋_; _∷_; ≋-refl; ≋-sym; ≋-trans)
 
 ------------------------------------------------------------------------
 -- Definition

From 00a335a7bfd90f924199e6f47b4f50b9e67636b7 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 14:34:43 +0000
Subject: [PATCH 16/35] refactor: encapsulate and tighten up

---
 .../Relation/Binary/BagAndSetEquality.agda    | 21 ++---
 .../Permutation/Propositional/Properties.agda | 81 ++++++++++---------
 2 files changed, 50 insertions(+), 52 deletions(-)

diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index f014df8b41..6fff193032 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -566,27 +566,16 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
 
 
 ------------------------------------------------------------------------
--- Relationships to other relations
+-- Relationships to propositional permutation
 
 ↭⇒∼bag : _↭_ {A = A} ⇒ _∼[ bag ]_
-↭⇒∼bag 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 = ∈-resp-↭ xs↭ys
-
-  from : ∀ {xs ys} → xs ↭ ys → v ∈ ys → v ∈ xs
-  from xs↭ys = ∈-resp-↭ (↭-sym xs↭ys)
-
-  from∘to : ∀ {xs ys} (p : xs ↭ ys) (q : v ∈ xs) → from p (to p q) ≡ q
-  from∘to = ∈-resp-[σ⁻¹∘σ]
-
-  to∘from : ∀ {xs ys} (p : xs ↭ ys) (q : v ∈ ys) → to p (from p q) ≡ q
-  to∘from p with res ← from∘to (↭-sym p) rewrite ↭-sym-involutive p = res
+↭⇒∼bag xs↭ys {v} =
+  mk↔ₛ′ (∈-resp-↭ xs↭ys) (∈-resp-↭ (↭-sym xs↭ys)) (∈-resp-[σ∘σ⁻¹] xs↭ys) (∈-resp-[σ⁻¹∘σ] xs↭ys)
 
 ∼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
+  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 x zs₁ zs₂ ⟨
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index e6828e5852..670db89ba2 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -70,49 +70,58 @@ private
 ------------------------------------------------------------------------
 -- Relationships to other predicates
 
-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)
+module _ {P : Pred A p} where
+
+  All-resp-↭ : (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-↭ : (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)
+
+  Any-resp-[σ⁻¹∘σ] : ∀ {xs ys} (σ : 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
+
+  Any-resp-[σ∘σ⁻¹] : ∀ {xs ys} (σ : xs ↭ ys) (iy : Any P ys) →
+                     Any-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy
+  Any-resp-[σ∘σ⁻¹] p
+    with res ← Any-resp-[σ⁻¹∘σ] (↭-sym p)
+    rewrite ↭-sym-involutive p
+    = res
 
 ∈-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-[σ⁻¹∘σ] : ∀ {xs ys} {x : A} (σ : xs ↭ ys) (ix : x ∈ xs) →
                  ∈-resp-↭ (trans σ (↭-sym σ)) ix ≡ ix
 ∈-resp-[σ⁻¹∘σ] = Any-resp-[σ⁻¹∘σ]
 
+∈-resp-[σ∘σ⁻¹] : ∀ {xs ys} {y : A} (σ : xs ↭ ys) (iy : y ∈ ys) →
+                 ∈-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy
+∈-resp-[σ∘σ⁻¹] = Any-resp-[σ∘σ⁻¹]
+
 ------------------------------------------------------------------------
 -- map
 

From 91feb309ed326ebaca32c792d9cc13001eff8650 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 14:39:18 +0000
Subject: [PATCH 17/35] avoid `PermutationReasoning` custom combinators

---
 src/Data/List/Relation/Binary/BagAndSetEquality.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index 6fff193032..b31bf21504 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -573,11 +573,11 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
   mk↔ₛ′ (∈-resp-↭ xs↭ys) (∈-resp-↭ (↭-sym xs↭ys)) (∈-resp-[σ∘σ⁻¹] xs↭ys) (∈-resp-[σ⁻¹∘σ] xs↭ys)
 
 ∼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₂ , 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 ∷ xs           ↭⟨ ↭-prep x (∼bag⇒↭ (drop-cons (↔-trans eq (comm zs₁ (x ∷ zs₂))))) ⟩
+    x ∷ (zs₂ ++ zs₁) ↭⟨ ↭-prep x (++-comm zs₂ zs₁) ⟩
     x ∷ (zs₁ ++ zs₂) ↭⟨ shift x zs₁ zs₂ ⟨
     zs₁ ++ x ∷ zs₂   ∎
     where

From 227043d27ccb816dbe98c5af3d77caa2b0325c37 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 14:59:57 +0000
Subject: [PATCH 18/35] fix up `CHANGELOG`

---
 CHANGELOG.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0d1dcf54c5..31efc7c0ef 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -63,6 +63,11 @@ Deprecated names
   foldr-commMonoid  ↦  foldr-pres-↭
   ```
 
+* In `Data.Nat.Divisibility.Core`:
+  ```agda
+  *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
+  ```
+
 New modules
 -----------
 
@@ -396,6 +401,8 @@ Additions to existing modules
 
 * Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
   ```agda
+  Any-resp-[σ∘σ⁻¹] : (σ : xs ↭ ys) (iy : Any P ys) →
+                     Any-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy
   product-↭ : product Preserves _↭_ ⟶ _≡_
   ```
 

From 4df26efa8670772e925bab6c4b17ead87ddb3c99 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 15:13:15 +0000
Subject: [PATCH 19/35] encapsulate helper function

---
 .../Permutation/Propositional/Properties.agda | 73 ++++++++++---------
 1 file changed, 37 insertions(+), 36 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index 670db89ba2..52d254df88 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -198,43 +198,44 @@ drop-mid-≡ (w ∷ ws) (x ∷ xs) eq
 drop-mid : ∀ {x : A} ws xs {ys zs} →
            ws ++ [ x ] ++ ys ↭ xs ++ [ x ] ++ zs →
            ws ++ ys ↭ xs ++ zs
-drop-mid′ : ∀ {as bs} → as ↭ bs →
-            ∀ {x : A} ws xs {ys zs} →
-            as ≡ ws ++ [ x ] ++ ys →
-            bs ≡ xs ++ [ x ] ++ zs →
-            ws ++ ys ↭ xs ++ zs
 drop-mid ws xs p = drop-mid′ p ws xs refl refl
-drop-mid′ refl ws xs refl eq = drop-mid-≡ ws xs eq
-drop-mid′ (trans p q) ws  xs refl refl
-  with h , t , refl ← ∈-∃++ (∈-resp-↭ p (∈-insert ws))
-  = trans (drop-mid ws h p) (drop-mid h xs q)
-drop-mid′ (prep x p)   []           []           refl eq
-  with refl ← List.∷-injectiveʳ 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 ws xs p)
-drop-mid′ (swap y z p) []           []           refl refl = prep _ p
-drop-mid′ (swap y z p) []           (x ∷ [])     refl eq
-  with refl , eq′ ← List.∷-injective eq
-  with refl ← List.∷-injectiveʳ eq′ = 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 refl ← List.∷-injectiveʳ eq  = 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
-    _ ∷ _             ↭⟨ prep _ p ⟩
-    _ ∷ (xs ++ _ ∷ _) ↭⟨ prep _ (shift _ _ _) ⟩
-    _ ∷ _ ∷ xs ++ _   ↭⟨ swap _ _ refl ⟩
-    _ ∷ _ ∷ xs ++ _   ∎
-    where open PermutationReasoning
-drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ [])     refl refl = begin
-    _ ∷ _ ∷ ws ++ _   ↭⟨ swap _ _ refl ⟩
-    _ ∷ (_ ∷ ws ++ _) ↭⟨ prep _ (shift _ _ _) ⟨
-    _ ∷ (ws ++ _ ∷ _) ↭⟨ prep _ p ⟩
-    _ ∷ _             ∎
-    where open PermutationReasoning
-drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ y ∷ xs) refl refl = swap y z (drop-mid _ _ p)
+  where
+  drop-mid′ : ∀ {as bs} → as ↭ bs →
+              ∀ {x : A} ws xs {ys zs} →
+              as ≡ ws ++ [ x ] ++ ys →
+              bs ≡ xs ++ [ x ] ++ zs →
+              ws ++ ys ↭ xs ++ zs
+  drop-mid′ refl ws xs refl eq = drop-mid-≡ ws xs eq
+  drop-mid′ (trans p q) ws  xs refl refl
+    with h , t , refl ← ∈-∃++ (∈-resp-↭ p (∈-insert ws))
+    = trans (drop-mid ws h p) (drop-mid h xs q)
+  drop-mid′ (prep x p)   []           []           refl eq
+    with refl ← List.∷-injectiveʳ 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 ws xs p)
+  drop-mid′ (swap y z p) []           []           refl refl = prep _ p
+  drop-mid′ (swap y z p) []           (x ∷ [])     refl eq
+    with refl , eq′ ← List.∷-injective eq
+    with refl ← List.∷-injectiveʳ eq′ = 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 refl ← List.∷-injectiveʳ eq  = 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
+      _ ∷ _             ↭⟨ prep _ p ⟩
+      _ ∷ (xs ++ _ ∷ _) ↭⟨ prep _ (shift _ _ _) ⟩
+      _ ∷ _ ∷ xs ++ _   ↭⟨ swap _ _ refl ⟩
+      _ ∷ _ ∷ xs ++ _   ∎
+      where open PermutationReasoning
+  drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ [])     refl refl = begin
+      _ ∷ _ ∷ ws ++ _   ↭⟨ swap _ _ refl ⟩
+      _ ∷ (_ ∷ ws ++ _) ↭⟨ prep _ (shift _ _ _) ⟨
+      _ ∷ (ws ++ _ ∷ _) ↭⟨ prep _ p ⟩
+      _ ∷ _             ∎
+      where open PermutationReasoning
+  drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ y ∷ xs) refl refl = swap y z (drop-mid _ _ p)
 
 
 -- Algebraic properties

From 0bf8e3882c76d1bf811858abb4623694a0743849 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 17:25:00 +0000
Subject: [PATCH 20/35] revert changes

---
 src/Data/Nat/Primality/Factorisation.agda | 21 +++++++++------------
 1 file changed, 9 insertions(+), 12 deletions(-)

diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda
index 06438eb8d0..6dda6bac9d 100644
--- a/src/Data/Nat/Primality/Factorisation.agda
+++ b/src/Data/Nat/Primality/Factorisation.agda
@@ -21,17 +21,15 @@ 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 (_↭_; ↭-refl; ↭-prep; module PermutationReasoning)
-open import Data.List.Relation.Binary.Permutation.Propositional.Properties
-  using (product-↭; All-resp-↭; shift)
+  using (_↭_; prep; swap; ↭-reflexive; ↭-refl; ↭-trans; 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
@@ -141,7 +139,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
@@ -165,26 +163,25 @@ private
         where open ≡-Reasoning
 
       shuffle : ∃[ bs′ ] bs ↭ a ∷ bs′
-      shuffle
-        with ys , zs , refl ← ∈-∃++ (factorisationHasAllPrimeFactors prime[a] a∣Πbs prime[bs])
-        = ys ++ zs , shift a ys zs
+      shuffle with ys , zs , p ← ∈-∃++ (factorisationHasAllPrimeFactors prime[a] a∣Πbs prime[bs])
+        = ys ++ zs , ↭-trans (↭-reflexive p) (shift a ys zs)
 
       bs′ = proj₁ shuffle
       bs↭a∷bs′ = proj₂ shuffle
 
       Πas≡Πbs′ : product as ≡ product bs′
-      Πas≡Πbs′ = *-cancelˡ-≡ (product as) (product bs′) a $ begin
+      Πas≡Πbs′ = *-cancelˡ-≡ (product as) (product bs′) a {{prime⇒nonZero prime[a]}} $ begin
         a * product as  ≡⟨ Πas≡Πbs ⟩
         product bs      ≡⟨ product-↭ bs↭a∷bs′ ⟩
         a * product bs′ ∎
-        where open ≡-Reasoning ; instance _ = prime⇒nonZero prime[a]
+        where open ≡-Reasoning
 
       prime[bs'] : All Prime bs′
       prime[bs'] = All.tail (All-resp-↭ bs↭a∷bs′ prime[bs])
 
       a∷as↭bs : a ∷ as ↭ bs
       a∷as↭bs = begin
-        a ∷ as  ↭⟨ ↭-prep a (factorisationUnique′ as bs′ Πas≡Πbs′ prime[as] prime[bs']) ⟩
+        a ∷ as  <⟨ factorisationUnique′ as bs′ Πas≡Πbs′ prime[as] prime[bs'] ⟩
         a ∷ bs′ ↭⟨ bs↭a∷bs′ ⟨
         bs      ∎
         where open PermutationReasoning

From 60a19589b57f3d4fc38b183d4685adf239cd3eac Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 17:38:19 +0000
Subject: [PATCH 21/35] review comments

---
 CHANGELOG.md                                  | 18 +++++-------
 .../Binary/Permutation/Propositional.agda     |  8 +++---
 .../Relation/Binary/Permutation/Setoid.agda   | 28 +++++++++----------
 .../Binary/Permutation/Setoid/Properties.agda | 15 +++++-----
 4 files changed, 32 insertions(+), 37 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 31efc7c0ef..fd02943e47 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -49,11 +49,6 @@ Deprecated names
   _-_  ↦  _//_
   ```
 
-* In `Data.List.Relation.Binary.Permutation.Setoid`:
-  ```agda
-  steps  ↦  Data.List.Relation.Binary.Permutation.Homogeneous.steps
-  ```
-
 * In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
   ```agda
   split  ↦  ↭-split
@@ -290,17 +285,18 @@ Additions to existing modules
   ```
   and properties
   ```agda
-  ↭-pointwise : _≋_ ⇒ _↭_
-  ↭⇒↭ₛ        : _↭_  ⇒ _↭ₛ_
-  ↭ₛ⇒↭        : _↭ₛ_ ⇒ _↭_
+  ↭-reflexive-≋ : _≋_ ⇒ _↭_
+  ↭⇒↭ₛ          : _↭_  ⇒ _↭ₛ_
+  ↭ₛ⇒↭          : _↭ₛ_ ⇒ _↭_
   ```
   where `_↭ₛ_` is the `Setoid (setoid _)` instance of `Permutation`
 
 * In `Data.List.Relation.Binary.Permutation.Setoid`:
   ```agda
-  ↭-pointwise : _≋_  ⇒ _↭_
-  ↭-transˡ-≋  : LeftTrans _≋_ _↭_
-  ↭-transʳ-≋  : RightTrans _↭_ _≋_
+  ↭-reflexive-≋ : _≋_  ⇒ _↭_
+  ↭-transˡ-≋    : LeftTrans _≋_ _↭_
+  ↭-transʳ-≋    : RightTrans _↭_ _≋_
+  ↭-trans′      : Transitive _↭_
   ```
 
 * In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional.agda b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
index 83d3142c6e..0e13a5e3ba 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
@@ -60,8 +60,8 @@ data _↭_ : Rel (List A) a where
 ↭-reflexive : _≡_ ⇒ _↭_
 ↭-reflexive refl = ↭-refl
 
-↭-pointwise : _≋_ ⇒ _↭_
-↭-pointwise xs≋ys = ↭-reflexive (≋⇒≡ xs≋ys)
+↭-reflexive-≋ : _≋_ ⇒ _↭_
+↭-reflexive-≋ xs≋ys = ↭-reflexive (≋⇒≡ xs≋ys)
 
 ↭-sym : xs ↭ ys → ys ↭ xs
 ↭-sym refl                = refl
@@ -99,11 +99,11 @@ private
 ↭⇒↭ₛ refl         = ↭ₛ.↭-refl
 ↭⇒↭ₛ (prep x p)   = ↭ₛ.↭-prep x (↭⇒↭ₛ p)
 ↭⇒↭ₛ (swap x y p) = ↭ₛ.↭-swap x y (↭⇒↭ₛ p)
-↭⇒↭ₛ (trans p q)  = ↭ₛ.↭-trans (↭⇒↭ₛ p) (↭⇒↭ₛ q)
+↭⇒↭ₛ (trans p q)  = ↭ₛ.↭-trans′ (↭⇒↭ₛ p) (↭⇒↭ₛ q)
 
 
 ↭ₛ⇒↭ : _↭ₛ_ ⇒ _↭_
-↭ₛ⇒↭ (↭ₛ.refl xs≋ys)       = ↭-pointwise xs≋ys
+↭ₛ⇒↭ (↭ₛ.refl xs≋ys)       = ↭-reflexive-≋ xs≋ys
 ↭ₛ⇒↭ (↭ₛ.prep refl p)      = ↭-prep _ (↭ₛ⇒↭ p)
 ↭ₛ⇒↭ (↭ₛ.swap refl refl p) = ↭-swap _ _ (↭ₛ⇒↭ p)
 ↭ₛ⇒↭ (↭ₛ.trans p q)        = ↭-trans (↭ₛ⇒↭ p) (↭ₛ⇒↭ q)
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
index 35717745ca..73cd4a6db4 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
@@ -28,7 +28,7 @@ open module ≈ = Setoid S using (_≈_) renaming (Carrier to A)
 open ≋ S using (_≋_; _∷_; ≋-refl; ≋-sym; ≋-trans)
 
 ------------------------------------------------------------------------
--- Definition
+-- Definition, based on `Homogeneous`
 
 open Homogeneous public
   using (refl; prep; swap; trans)
@@ -38,13 +38,18 @@ infix 3 _↭_
 _↭_ : Rel (List A) (a ⊔ ℓ)
 _↭_ = Homogeneous.Permutation _≈_
 
+steps = Homogeneous.steps {R = _≈_}
+
 ------------------------------------------------------------------------
 -- Constructor aliases
 
 -- Constructor alias
 
-↭-pointwise : _≋_ ⇒ _↭_
-↭-pointwise = refl
+↭-reflexive-≋ : _≋_ ⇒ _↭_
+↭-reflexive-≋ = refl
+
+↭-trans : Transitive _↭_
+↭-trans = trans
 
 -- These provide aliases for `swap` and `prep` when the elements being
 -- swapped or prepended are propositionally equal
@@ -59,7 +64,7 @@ _↭_ = Homogeneous.Permutation _≈_
 -- _↭_ is an equivalence
 
 ↭-reflexive : _≡_ ⇒ _↭_
-↭-reflexive refl = ↭-pointwise ≋-refl
+↭-reflexive refl = ↭-reflexive-≋ ≋-refl
 
 ↭-refl : Reflexive _↭_
 ↭-refl = ↭-reflexive refl
@@ -87,10 +92,10 @@ _↭_ = Homogeneous.Permutation _≈_
 ↭-transʳ-≋ (trans xs↭ws ws↭ys)  ys≋zs
   = trans xs↭ws (↭-transʳ-≋ ws↭ys ys≋zs)
 
-↭-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
+↭-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
 
 ↭-isEquivalence : IsEquivalence _↭_
 ↭-isEquivalence = record
@@ -114,7 +119,7 @@ module PermutationReasoning where
     renaming (≈-go to ↭-go)
 
   open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public
-  open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ ↭-pointwise) ≋-sym public
+  open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ ↭-reflexive-≋) ≋-sym public
 
   -- Some extra combinators that allow us to skip certain elements
 
@@ -141,9 +146,4 @@ module PermutationReasoning where
 
 -- Version 2.1
 
-steps = Homogeneous.steps {R = _≈_}
-{-# WARNING_ON_USAGE steps
-"Warning: steps was deprecated in v2.1.
-Please use Homogeneous.steps explicitly instead."
-#-}
 
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index b4060eeece..755946e48e 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -62,7 +62,6 @@ private
     P : Pred A p
     R : Rel A r
 
-  _++[_]++_ = λ xs (z : A) ys → xs ++ [ z ] ++ ys
 
 ------------------------------------------------------------------------
 -- Relationships to other predicates
@@ -117,18 +116,18 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin
 -- Relationship to `_≋_`
 ------------------------------------------------------------------------
 
-↭-split : ∀ v as bs {xs} → xs ↭ (as ++[ v ]++ bs) →
-          ∃₂ λ ps qs → xs ≋ (ps ++[ v ]++ qs)
+↭-split : ∀ v as bs → xs ↭ (as ++ [ v ] ++ bs) →
+          ∃₂ λ ps qs → xs ≋ (ps ++ [ v ] ++ qs)
                      × (ps ++ qs) ↭ (as ++ bs)
 ↭-split v as bs p = helper as bs p ≋-refl
   where
-  helper : ∀ as bs → xs ↭ ys → ys ≋ (as ++[ v ]++ bs) →
-           ∃₂ λ ps qs → xs ≋ (ps ++[ v ]++ qs)
+  helper : ∀ as bs → 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 ↭′ ↭
+    = ps′ , qs′ , eq′ , ↭-trans′ ↭′ ↭
   helper []           _  (refl (x≈v ∷ xs≋vs)) (v≈y ∷ vs≋ys)
     = [] , _ , ≈-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)
@@ -218,7 +217,7 @@ module _ (P? : Decidable P) (P≈ : P Respects _≈_) where
 dropMiddleElement-≋ : ∀ {x} ws xs {ys} {zs} →
            ws ++ [ x ] ++ ys ≋ xs ++ [ x ] ++ zs →
            ws ++ ys ↭ xs ++ zs
-dropMiddleElement-≋ []       []       (_   ∷ eq) = ↭-pointwise eq
+dropMiddleElement-≋ []       []       (_   ∷ eq) = ↭-reflexive-≋ 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)
@@ -435,7 +434,7 @@ module _{_∙_ : Op₂ A} {ε : A}
 -- TOWARDS DEPRECATION
 ------------------------------------------------------------------------
 
-≋⇒↭ = ↭-pointwise
+≋⇒↭ = ↭-reflexive-≋
 
 -- These are easily superseded by ↭-transˡ-≋, ↭-transʳ-≋
 -- But for the properties of steps which require precise measurement

From fd80b0bdebe2c1f04cf0744443c4ea762ad1c199 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Mar 2024 17:46:34 +0000
Subject: [PATCH 22/35] `fix-whitespace`

---
 src/Data/List/Relation/Binary/Permutation/Setoid.agda | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
index 73cd4a6db4..3d97e15fe0 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
@@ -146,4 +146,3 @@ module PermutationReasoning where
 
 -- Version 2.1
 
-

From 1781ea3990ffd2a4151dfbd934c61deefa37b8f3 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 29 Mar 2024 07:12:43 +0000
Subject: [PATCH 23/35] toned down the comment on `steps`

---
 src/Data/List/Relation/Binary/Permutation/Homogeneous.agda | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
index 6e93c2f7ca..82640c750e 100644
--- a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
@@ -61,9 +61,7 @@ map R⇒S (swap e₁ e₂ xs∼ys)   = swap (R⇒S e₁) (R⇒S e₂) (map R⇒S
 map R⇒S (trans xs∼ys ys∼zs)  = trans (map R⇒S xs∼ys) (map R⇒S ys∼zs)
 
 ------------------------------------------------------------------------
--- Steps moves here towards eventual deprecation, because it is
--- * representation-dependent
--- * now obsolete wrt `Setoid.Properties.{dropMiddleElement,split}`
+-- Steps moves here because it is representation-dependent
 
 steps : ∀ {R : Rel A r} {xs ys} → Permutation R xs ys → ℕ
 steps (refl _)            = 1

From 7c2bc3517f74bb99e5989cc2c51eb322bd426c3d Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 29 Mar 2024 08:07:30 +0000
Subject: [PATCH 24/35] remove use of infix `insert`

---
 CHANGELOG.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index fd02943e47..16335f670a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -301,8 +301,8 @@ Additions to existing modules
 
 * In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
   ```agda
-  ↭-split : xs ↭ (as ++[ v ]++ bs) →
-            ∃₂ λ ps qs → xs ≋ (ps ++[ v ]++ qs) × (ps ++ qs) ↭ (as ++ bs)
+  ↭-split : xs ↭ (as ++ [ v ] ++ bs) →
+            ∃₂ λ ps qs → xs ≋ (ps ++ [ v ] ++ qs) × (ps ++ qs) ↭ (as ++ bs)
   drop-∷  : x ∷ xs ↭ x ∷ ys → xs ↭ ys
 
   foldr-pres-↭ : (IsCommutativeMonoid _≈_ _∙_ ε) → (foldr _∙_ ε) Preserves _↭_ ⟶ _≈_

From 2e032a51b01401eaa84b2a9c98c379003f841ffd Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 29 Mar 2024 08:58:25 +0000
Subject: [PATCH 25/35] revert other deprecation

---
 CHANGELOG.md                                   |  7 +------
 .../Permutation/Propositional/Properties.agda  |  2 +-
 .../Binary/Permutation/Setoid/Properties.agda  | 18 ++++++------------
 3 files changed, 8 insertions(+), 19 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 16335f670a..28fec20430 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -53,10 +53,7 @@ Deprecated names
   ```agda
   split  ↦  ↭-split
   ```
-  with a more informative type, and a simple renaming
-  ```agda
-  foldr-commMonoid  ↦  foldr-pres-↭
-  ```
+  with a more informative type.
 
 * In `Data.Nat.Divisibility.Core`:
   ```agda
@@ -304,8 +301,6 @@ Additions to existing modules
   ↭-split : xs ↭ (as ++ [ v ] ++ bs) →
             ∃₂ λ ps qs → xs ≋ (ps ++ [ v ] ++ qs) × (ps ++ qs) ↭ (as ++ bs)
   drop-∷  : x ∷ xs ↭ x ∷ ys → xs ↭ ys
-
-  foldr-pres-↭ : (IsCommutativeMonoid _≈_ _∙_ ε) → (foldr _∙_ ε) Preserves _↭_ ⟶ _≈_
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index 52d254df88..ea831f5d71 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -374,7 +374,7 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where
 -- product
 
 product-↭ : product Preserves _↭_ ⟶ _≡_
-product-↭ p = foldr-pres-↭ ℕ-*-1.isCommutativeMonoid (↭⇒↭ₛ p)
+product-↭ p = foldr-commMonoid ℕ-*-1.isCommutativeMonoid (↭⇒↭ₛ p)
   where
   module ℕ-*-1 = CommutativeMonoid ℕ.*-1-commutativeMonoid
   open Permutation ℕ-*-1.setoid
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index 755946e48e..28f9294899 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -416,18 +416,18 @@ module _{_∙_ : Op₂ A} {ε : A}
     open module CM = CommutativeMonoid commutativeMonoid
       using (∙-cong; ∙-congˡ; ∙-congʳ; assoc; comm)
 
-  foldr-pres-↭ : (foldr _∙_ ε) Preserves _↭_ ⟶ _≈_
-  foldr-pres-↭ (refl xs≋ys)        = Pointwise.foldr⁺ ∙-cong CM.refl xs≋ys
-  foldr-pres-↭ (prep x≈y xs↭ys)    = ∙-cong x≈y (foldr-pres-↭ xs↭ys)
-  foldr-pres-↭ (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = begin
-    x ∙ (y ∙ foldr _∙_ ε xs)    ≈⟨ ∙-congˡ (∙-congˡ (foldr-pres-↭ xs↭ys)) ⟩
+  foldr-commMonoid : (foldr _∙_ ε) Preserves _↭_ ⟶ _≈_
+  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 {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 CM.setoid
-  foldr-pres-↭ (trans xs↭ys ys↭zs) = CM.trans (foldr-pres-↭ xs↭ys) (foldr-pres-↭ ys↭zs)
+  foldr-commMonoid (trans xs↭ys ys↭zs) = CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs)
 
 
 ------------------------------------------------------------------------
@@ -491,9 +491,3 @@ split v as bs xs↭as++[v]++bs
 "Warning: split was deprecated in v2.1.
 Please use the sharper lemma ↭-split instead."
 #-}
-
-foldr-commMonoid = foldr-pres-↭
-{-# WARNING_ON_USAGE foldr-commMonoid
-"Warning: foldr-commMonoid was deprecated in v2.1.
-Please use foldr-pres-↭ instead."
-#-}

From 4ad9feffeac724ae301ec059a93cd45770ac0249 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 29 Mar 2024 13:10:58 +0000
Subject: [PATCH 26/35] no need for qualification

---
 src/Data/List/Relation/Binary/BagAndSetEquality.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index b31bf21504..91e4f678a8 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -575,7 +575,7 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
 ∼bag⇒↭ : _∼[ bag ]_ ⇒ _↭_ {A = A}
 ∼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
+  with zs₁ , zs₂ , refl ← ∈-∃++ (Inverse.to (eq {x}) (here refl)) = begin
     x ∷ xs           ↭⟨ ↭-prep x (∼bag⇒↭ (drop-cons (↔-trans eq (comm zs₁ (x ∷ zs₂))))) ⟩
     x ∷ (zs₂ ++ zs₁) ↭⟨ ↭-prep x (++-comm zs₂ zs₁) ⟩
     x ∷ (zs₁ ++ zs₂) ↭⟨ shift x zs₁ zs₂ ⟨

From 83dc6c70e8a036c2bb807c8dd717a57caa892caa Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 29 Mar 2024 18:07:32 +0000
Subject: [PATCH 27/35] remove deprecation banner

---
 src/Data/List/Relation/Binary/Permutation/Setoid.agda | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
index 3d97e15fe0..87b3bdd97c 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
@@ -137,12 +137,3 @@ module PermutationReasoning where
 
   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
-
-------------------------------------------------------------------------
--- DEPRECATED NAMES
-------------------------------------------------------------------------
--- Please use the new names as continuing support for the old names is
--- not guaranteed.
-
--- Version 2.1
-

From 246bf5c5a87ece9d955bcac845ae4d553ccd19a9 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 29 Mar 2024 18:54:49 +0000
Subject: [PATCH 28/35] three paras of commentary on the new transitivity
 proofs

---
 .../List/Relation/Binary/Permutation/Setoid.agda  | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
index 87b3bdd97c..5c81eb6999 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
@@ -72,6 +72,21 @@ steps = Homogeneous.steps {R = _≈_}
 ↭-sym : Symmetric _↭_
 ↭-sym = Homogeneous.sym ≈.sym
 
+-- As with the existing proofs `↭-respʳ-≋` and `↭-respˡ-≋` in `Setoid.Properties`
+-- (which appeal to symmetry of the underlying equality, and its effect on the
+-- proofs of symmetry for both pointwise equality and permutation) to the effect
+-- that _↭_ respects _≋_ on the left and right, such arguments can be both
+-- streamlined, and used to define a 'smart' constructor `↭-trans′` for transitivity.
+--
+-- The arguments below show how proofs of permutation can have all transitive
+-- compositions with instances of `refl` pushed to the leaves of derivations,
+-- thereby addressing the inefficiencies analysed in issue #1113
+--
+-- Conjecture: these transformations are `steps` invariant, but that is moot,
+-- given their use here, and in `Setoid.Properties.↭-split` (without requiring
+-- WF-induction on `steps`) to enable a new, sharper, analysis of lists `xs`
+-- such that `xs ↭ ys ++ [ x ] ++ zs` in terms of `x`, `ys`, and `zs`.
+
 ↭-transˡ-≋ : LeftTrans _≋_ _↭_
 ↭-transˡ-≋ xs≋ys               (refl ys≋zs)
   = refl (≋-trans xs≋ys ys≋zs)

From 39bb784f162ca0d46d0d51340297c2cd2aee9035 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 30 Mar 2024 06:05:34 +0000
Subject: [PATCH 29/35] missing entry

---
 CHANGELOG.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 28fec20430..fdb9d80236 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -394,7 +394,9 @@ Additions to existing modules
   ```agda
   Any-resp-[σ∘σ⁻¹] : (σ : xs ↭ ys) (iy : Any P ys) →
                      Any-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy
-  product-↭ : product Preserves _↭_ ⟶ _≡_
+  ∈-resp-[σ∘σ⁻¹]   : (σ : xs ↭ ys) (iy : y ∈ ys) →
+                     ∈-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy
+  product-↭        : product Preserves _↭_ ⟶ _≡_
   ```
 
 * Added new functions in `Data.String.Base`:

From b7dff80ad604394b450ce4cddc16b302309d19ab Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 30 Mar 2024 09:18:41 +0000
Subject: [PATCH 30/35] missing terminator

---
 CHANGELOG.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index fdb9d80236..50da6c920c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -402,6 +402,7 @@ Additions to existing modules
 * Added new functions in `Data.String.Base`:
   ```agda
   map : (Char → Char) → String → String
+  ```
 
 * Added new definition in `Relation.Binary.Construct.Closure.Transitive`
   ```

From ce4d72fa64d9d29fd22dec5658839af57479a5d7 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 6 Apr 2024 21:39:33 +0100
Subject: [PATCH 31/35] response to review comments

---
 CHANGELOG.md                                               | 2 +-
 src/Data/List/Relation/Binary/Permutation/Homogeneous.agda | 3 +--
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 50da6c920c..822dffb684 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -53,7 +53,7 @@ Deprecated names
   ```agda
   split  ↦  ↭-split
   ```
-  with a more informative type.
+  with a more informative type (see below).
 
 * In `Data.Nat.Divisibility.Core`:
   ```agda
diff --git a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
index 82640c750e..686c569423 100644
--- a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
@@ -60,8 +60,7 @@ 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)
 
-------------------------------------------------------------------------
--- Steps moves here because it is representation-dependent
+-- Measures the number of constructors, can be useful for termination proofs
 
 steps : ∀ {R : Rel A r} {xs ys} → Permutation R xs ys → ℕ
 steps (refl _)            = 1

From c8bf0a61e13ad4f28a7e6dac766a1bcb99949582 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 7 Apr 2024 14:57:45 +0100
Subject: [PATCH 32/35] `with` to `let`

---
 .../List/Relation/Binary/Permutation/Setoid/Properties.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index 28f9294899..4ce9b888a6 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -331,9 +331,9 @@ shifts xs ys {zs} = begin
 dropMiddleElement : ∀ {v} ws xs {ys zs} →
                     ws ++ [ v ] ++ ys ↭ xs ++ [ v ] ++ zs →
                     ws ++ ys ↭ xs ++ zs
-dropMiddleElement {v} ws xs {ys} {zs} p
-  with ps , qs , eq , ↭ ← ↭-split v xs zs p
-  = ↭-trans (dropMiddleElement-≋ ws ps eq) ↭
+dropMiddleElement {v} ws xs {ys} {zs} p =
+  let ps , qs , eq , ↭ = ↭-split v xs zs p
+  in ↭-trans (dropMiddleElement-≋ ws ps eq) ↭
 
 dropMiddle : ∀ {vs} ws xs {ys zs} →
              ws ++ vs ++ ys ↭ xs ++ vs ++ zs →

From cbef1f847e337de5f1f9b922530fe88f682ddcb0 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 24 Apr 2024 10:47:35 +0100
Subject: [PATCH 33/35] fixed `BagAndSetEquality`

---
 src/Data/List/Relation/Binary/BagAndSetEquality.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index d55fcb0c94..23e1e4bd30 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -27,9 +27,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 (_↭_; ↭-sym; refl; module PermutationReasoning)
+  using (_↭_; ↭-refl; ↭-sym; ↭-prep; module PermutationReasoning)
 open import Data.List.Relation.Binary.Permutation.Propositional.Properties
-  using (∈-resp-↭; ∈-resp-[σ⁻¹∘σ]; ↭-sym-involutive; shift; ++-comm)
+  using (∈-resp-↭; ∈-resp-[σ⁻¹∘σ]; ∈-resp-[σ∘σ⁻¹]; shift; ++-comm)
 open import Data.Product.Base as Prod using (∃; _,_; proj₁; proj₂; _×_)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum using (_⊎_; [_,_]′; inj₁; inj₂)

From dd296a66fb4aec146a77643706afdd1c5322fade Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 3 Sep 2024 22:07:29 +0100
Subject: [PATCH 34/35] fixed qualified `import` bug introduced during merge
 conflict resolution

---
 src/Data/List/Relation/Binary/BagAndSetEquality.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index 677a319f64..b27e45d585 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -30,7 +30,7 @@ open import Data.List.Relation.Binary.Permutation.Propositional
   using (_↭_; ↭-refl; ↭-sym; ↭-prep; module PermutationReasoning)
 open import Data.List.Relation.Binary.Permutation.Propositional.Properties
   using (∈-resp-↭; ∈-resp-[σ⁻¹∘σ]; ∈-resp-[σ∘σ⁻¹]; shift; ++-comm)
-open import Data.Product.Base as Prod using (∃; _,_; proj₁; proj₂; _×_)
+open import Data.Product.Base as Product using (∃; _,_; proj₁; proj₂; _×_)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum using (_⊎_; [_,_]′; inj₁; inj₂)
 open import Data.Sum.Properties using (inj₂-injective; inj₁-injective)

From 92c14a817e48dda284411f01333baba5c5b2318b Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Mon, 9 Sep 2024 10:33:37 +0100
Subject: [PATCH 35/35] Update CHANGELOG.md

Deleted spurious attribution of the lemmas in `Data.List.Properties` about `product` to `Data.List.Relation.Unary.All.Properties`. Hope this fixes things now!
---
 CHANGELOG.md | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f77870ec8f..89391033db 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -198,12 +198,6 @@ Additions to existing modules
   search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
   ```
 
-* In `Data.List.Relation.Unary.All.Properties`:
-  ```agda
-  product≢0 : All NonZero ns → NonZero (product ns)
-  ∈⇒≤product : All NonZero ns → n ∈ ns → n ≤ product ns
-  ```
-
 * In `Data.Maybe.Properties`:
   ```agda
   maybe′-∘ : ∀ f g → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b)