From 350eebf23e52eb1b16cfcc56caaf3ad9a73eae2c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 16 Jan 2025 15:24:38 +0000
Subject: [PATCH 1/8] move code to new module

---
 src/Data/Nat/SumAndProduct.agda | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 src/Data/Nat/SumAndProduct.agda

diff --git a/src/Data/Nat/SumAndProduct.agda b/src/Data/Nat/SumAndProduct.agda
new file mode 100644
index 0000000000..c0b3061dc1
--- /dev/null
+++ b/src/Data/Nat/SumAndProduct.agda
@@ -0,0 +1,18 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Natural numbers: sum and product of lists
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Nat.SumAndProduct where
+
+open import Data.Nat.Base using (ℕ; _+_; _*_)
+open import Data.List.Base using (List; foldr)
+
+sum : List ℕ → ℕ
+sum = foldr _+_ 0
+
+product : List ℕ → ℕ
+product = foldr _*_ 1

From 11b41eafbef56b5c32b154dc1dd9c73b55416b28 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 16 Jan 2025 15:25:26 +0000
Subject: [PATCH 2/8] refactor: deprecate old definitions

---
 src/Data/List/Base.agda | 23 +++++++++++++++++------
 1 file changed, 17 insertions(+), 6 deletions(-)

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 0c63e34940..b8a3157cb2 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -162,12 +162,6 @@ any p = or ∘ map p
 all : (A → Bool) → List A → Bool
 all p = and ∘ map p
 
-sum : List ℕ → ℕ
-sum = foldr _+_ 0
-
-product : List ℕ → ℕ
-product = foldr _*_ 1
-
 length : List A → ℕ
 length = foldr (const suc) 0
 
@@ -580,3 +574,20 @@ scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs
 "Warning: scanl was deprecated in v2.1.
 Please use Data.List.Scans.Base.scanl instead."
 #-}
+
+-- Version 2.3
+
+sum : List ℕ → ℕ
+sum = foldr _+_ 0
+{-# WARNING_ON_USAGE sum
+"Warning: sum was deprecated in v2.3.
+Please use Data.Nat.SumAndProduct.sum instead."
+#-}
+
+product : List ℕ → ℕ
+product = foldr _*_ 1
+{-# WARNING_ON_USAGE product
+"Warning: product was deprecated in v2.3.
+Please use Data.Nat.SumAndProduct.product instead."
+#-}
+

From 22873c6c07585669e00c3089d0a1eeb9ff62675f Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 16 Jan 2025 15:39:11 +0000
Subject: [PATCH 3/8] refactor: rejig `Nat` imports to uncouple `sum`,
 `product` form `length`

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

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index b8a3157cb2..59b66ab4ab 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -16,7 +16,7 @@ open import Data.Bool.Base as Bool
   using (Bool; false; true; not; _∧_; _∨_; if_then_else_)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′)
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _*_ ; _≤_ ; s≤s)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Data.Product.Base as Product using (_×_; _,_; map₁; map₂′)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
@@ -578,14 +578,14 @@ Please use Data.List.Scans.Base.scanl instead."
 -- Version 2.3
 
 sum : List ℕ → ℕ
-sum = foldr _+_ 0
+sum = foldr ℕ._+_ 0
 {-# WARNING_ON_USAGE sum
 "Warning: sum was deprecated in v2.3.
 Please use Data.Nat.SumAndProduct.sum instead."
 #-}
 
 product : List ℕ → ℕ
-product = foldr _*_ 1
+product = foldr ℕ._*_ 1
 {-# WARNING_ON_USAGE product
 "Warning: product was deprecated in v2.3.
 Please use Data.Nat.SumAndProduct.product instead."

From 3da9f7468779181b6bd744af4de869b7d09f6429 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 16 Jan 2025 15:58:54 +0000
Subject: [PATCH 4/8] refactor: `CHANGELOG`

---
 CHANGELOG.md | 598 +--------------------------------------------------
 1 file changed, 6 insertions(+), 592 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6703f59fb9..d020d141d3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,622 +1,36 @@
-Version 2.2
-===========
+Version 2.3-dev
+===============
 
 The library has been tested using Agda 2.7.0 and 2.7.0.1.
 
 Highlights
 ----------
 
-* Added missing morphisms between the more advanced algebraic structures.
-
-* Added many missing lemmas about positive and negative rational numbers.
-
 Bug-fixes
 ---------
 
-* Made the types for `≡-syntax` in `Relation.Binary.HeterogeneousEquality` more general.
-  These operators are used for equational reasoning of heterogeneous equality
-  `x ≅ y`, but previously the three operators in `≡-syntax` unnecessarily required
-  `x` and `y` to have the same type, making them unusable in many situations.
-
-* Removed unnecessary parameter `#-trans : Transitive _#_` from
-  `Relation.Binary.Reasoning.Base.Apartness`.
-
-* The `IsSemiringWithoutOne` record no longer incorrectly exposes the `Carrier` field
-  inherited from `Setoid` when opening the record publicly.
-
 Non-backwards compatible changes
 --------------------------------
 
-* In `Data.List.Relation.Binary.Sublist.Propositional.Properties` the implicit module parameters `a` and `A` have been replaced with `variable`s. This should be a backwards compatible change for the majority of uses, and would only be non-backwards compatible if for some reason you were explicitly supplying these implicit parameters when importing the module. Explicitly supplying the implicit parameters for functions exported from the module should not be affected.
-
-* [issue #2504](https://github.com/agda/agda-stdlib/issues/2504) and [issue #2519](https://github.com/agda/agda-stdlib/issues/2510) In `Data.Nat.Base` the definitions of `_≤′_` and `_≤‴_` have been modified to make the witness to equality explicit in new constructors `≤′-reflexive` and `≤‴-reflexive`; pattern synonyms `≤′-refl` and `≤‴-refl` have been added for backwards compatibility. This should be a backwards compatible change for the majority of uses, but the change in parametrisation means that these patterns are *not* necessarily well-formed if the old implicit arguments `m`,`n` are supplied explicitly.
-
 Minor improvements
 ------------------
 
-* In `Function.Related.TypeIsomorphisms`, the unprimed versions are more level polymorphic; and the primed versions retain `Level` homogeneous types for the `Semiring` axioms to hold.
-
 Deprecated modules
 ------------------
 
 Deprecated names
 ----------------
 
-* In `Algebra.Properties.CommutativeMagma.Divisibility`:
-  ```agda
-  ∣-factors    ↦  x|xy∧y|xy
-  ∣-factors-≈  ↦  xy≈z⇒x|z∧y|z
-  ```
-
-* In `Algebra.Properties.Magma.Divisibility`:
-  ```agda
-  ∣-respˡ   ↦  ∣-respˡ-≈
-  ∣-respʳ   ↦  ∣-respʳ-≈
-  ∣-resp    ↦  ∣-resp-≈
-  ```
-
-* In `Algebra.Solver.CommutativeMonoid`:
-  ```agda
-  normalise-correct  ↦  Algebra.Solver.CommutativeMonoid.Normal.correct
-  sg                 ↦  Algebra.Solver.CommutativeMonoid.Normal.singleton
-  sg-correct         ↦  Algebra.Solver.CommutativeMonoid.Normal.singleton-correct
-  ```
-
-* In `Algebra.Solver.IdempotentCommutativeMonoid`:
-  ```agda
-  flip12             ↦  Algebra.Properties.CommutativeSemigroup.xy∙z≈y∙xz
-  distr              ↦  Algebra.Properties.IdempotentCommutativeMonoid.∙-distrˡ-∙
-  normalise-correct  ↦  Algebra.Solver.IdempotentCommutativeMonoid.Normal.correct
-  sg                 ↦  Algebra.Solver.IdempotentCommutativeMonoid.Normal.singleton
-  sg-correct         ↦  Algebra.Solver.IdempotentCommutativeMonoid.Normal.singleton-correct
-  ```
-
-* In `Algebra.Solver.Monoid`:
-  ```agda
-  homomorphic        ↦  Algebra.Solver.Monoid.Normal.comp-correct
-  normalise-correct  ↦  Algebra.Solver.Monoid.Normal.correct
-  ```
-
-* In `Data.List.Properties`:
-  ```agda
-  concat-[-]   ↦  concat-map-[_]
-  ```
-
-* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
-  ```agda
-  split  ↦  ↭-split
-  ```
-  with a more informative type (see below).
-  ```
-
-* In `Data.List.Relation.Unary.All.Properties`:
-  ```agda
-  takeWhile⁻  ↦  all-takeWhile
-  ```
-
-* In `Data.Vec.Properties`:
+* In `Data.List.Base`:
   ```agda
-  ++-assoc _      ↦  ++-assoc-eqFree
-  ++-identityʳ _  ↦  ++-identityʳ-eqFree
-  unfold-∷ʳ _     ↦  unfold-∷ʳ-eqFree
-  ++-∷ʳ _         ↦  ++-∷ʳ-eqFree
-  ∷ʳ-++ _         ↦  ∷ʳ-++-eqFree
-  reverse-++ _    ↦  reverse-++-eqFree
-  ∷-ʳ++ _         ↦  ∷-ʳ++-eqFree
-  ++-ʳ++ _        ↦  ++-ʳ++-eqFree
-  ʳ++-ʳ++ _       ↦  ʳ++-ʳ++-eqFree
+  sum       ↦  Data.Nat.SumAndProduct.sum
+  product   ↦  Data.Nat.SumAndProduct.product
   ```
 
 New modules
 -----------
 
-* Consequences of module monomorphisms
-  ```
-  Algebra.Module.Morphism.BimoduleMonomorphism
-  Algebra.Module.Morphism.BisemimoduleMonomorphism
-  Algebra.Module.Morphism.LeftModuleMonomorphism
-  Algebra.Module.Morphism.LeftSemimoduleMonomorphism
-  Algebra.Module.Morphism.ModuleMonomorphism
-  Algebra.Module.Morphism.RightModuleMonomorphism
-  Algebra.Module.Morphism.RightSemimoduleMonomorphism
-  Algebra.Module.Morphism.SemimoduleMonomorphism
-  ```
-
-* Bundled morphisms between (raw) algebraic structures:
-  ```
-  Algebra.Morphism.Bundles
-  ```
-
-* Properties of `IdempotentCommutativeMonoid`s refactored out from `Algebra.Solver.IdempotentCommutativeMonoid`:
-  ```
-  Algebra.Properties.IdempotentCommutativeMonoid
-  ```
-
-* Refactoring of the `Algebra.Solver.*Monoid` implementations, via
-  a single `Solver` module API based on the existing `Expr`, and
-  a common `Normal`-form API:
-  ```
-  Algebra.Solver.CommutativeMonoid.Normal
-  Algebra.Solver.IdempotentCommutativeMonoid.Normal
-  Algebra.Solver.Monoid.Expression
-  Algebra.Solver.Monoid.Normal
-  Algebra.Solver.Monoid.Solver
-  ```
-  NB Imports of the existing proof procedures `solve` and `prove` etc. should still be via the top-level interfaces in `Algebra.Solver.*Monoid`.
-
-* `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
-  Propositional counterpart to `Data.List.Relation.Binary.Disjoint.Setoid.Properties`
-
-* Properties of list permutations that require the `--with-K` flag:
-  ```
-  Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK
-  ```
-
-* Refactored `Data.Refinement` into:
-  ```agda
-  Data.Refinement.Base
-  Data.Refinement.Properties
-  ```
-
-* Added implementation of Haskell-like `Foldable`:
-  ```agda
-  Effect.Foldable
-  Data.List.Effectful.Foldable
-  Data.Vec.Effectful.Foldable
-  ```
-
-* Raw bundles for the `Relation.Binary.Bundles` hierarchy:
-  ```agda
-  Relation.Binary.Bundles.Raw
-  ```
+* `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.SumAndProduct`.
 
 Additions to existing modules
 -----------------------------
-
-* In `Algebra.Bundles.KleeneAlgebra`:
-  ```agda
-  rawKleeneAlgebra : RawKleeneAlgebra _ _
-  ```
-
-* In `Algebra.Bundles.Raw.*`
-  ```agda
-  rawSetoid : RawSetoid c ℓ
-  ```
-
-* In `Algebra.Bundles.Raw.RawRingWithoutOne`
-  ```agda
-  rawNearSemiring : RawNearSemiring c ℓ
-  ```
-
-* Exporting more `Raw` substructures from `Algebra.Bundles.Ring`:
-  ```agda
-  rawNearSemiring   : RawNearSemiring _ _
-  rawRingWithoutOne : RawRingWithoutOne _ _
-  +-rawGroup        : RawGroup _ _
-  ```
-
-* Exporting `RawRingWithoutOne` and `(Raw)NearSemiring` subbundles from
-  `Algebra.Bundles.RingWithoutOne`:
-  ```agda
-  nearSemiring      : NearSemiring _ _
-  rawNearSemiring   : RawNearSemiring _ _
-  rawRingWithoutOne : RawRingWithoutOne _ _
-  ```
-
-* In `Algebra.Morphism.Construct.Composition`:
-  ```agda
-  magmaHomomorphism          : MagmaHomomorphism M₁.rawMagma M₂.rawMagma →
-                               MagmaHomomorphism M₂.rawMagma M₃.rawMagma →
-                               MagmaHomomorphism M₁.rawMagma M₃.rawMagma
-  monoidHomomorphism         : MonoidHomomorphism M₁.rawMonoid M₂.rawMonoid →
-                               MonoidHomomorphism M₂.rawMonoid M₃.rawMonoid →
-                               MonoidHomomorphism M₁.rawMonoid M₃.rawMonoid
-  groupHomomorphism          : GroupHomomorphism M₁.rawGroup M₂.rawGroup →
-                               GroupHomomorphism M₂.rawGroup M₃.rawGroup →
-                               GroupHomomorphism M₁.rawGroup M₃.rawGroup
-  nearSemiringHomomorphism   : NearSemiringHomomorphism M₁.rawNearSemiring M₂.rawNearSemiring →
-                               NearSemiringHomomorphism M₂.rawNearSemiring M₃.rawNearSemiring →
-                               NearSemiringHomomorphism M₁.rawNearSemiring M₃.rawNearSemiring
-  semiringHomomorphism       : SemiringHomomorphism M₁.rawSemiring M₂.rawSemiring →
-                               SemiringHomomorphism M₂.rawSemiring M₃.rawSemiring →
-                               SemiringHomomorphism M₁.rawSemiring M₃.rawSemiring
-  kleeneAlgebraHomomorphism  : KleeneAlgebraHomomorphism M₁.rawKleeneAlgebra M₂.rawKleeneAlgebra →
-                               KleeneAlgebraHomomorphism M₂.rawKleeneAlgebra M₃.rawKleeneAlgebra →
-                               KleeneAlgebraHomomorphism M₁.rawKleeneAlgebra M₃.rawKleeneAlgebra
-  nearSemiringHomomorphism   : NearSemiringHomomorphism M₁.rawNearSemiring M₂.rawNearSemiring →
-                               NearSemiringHomomorphism M₂.rawNearSemiring M₃.rawNearSemiring →
-                               NearSemiringHomomorphism M₁.rawNearSemiring M₃.rawNearSemiring
-  ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₂.rawRingWithoutOne →
-                               RingWithoutOneHomomorphism M₂.rawRingWithoutOne M₃.rawRingWithoutOne →
-                               RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₃.rawRingWithoutOne
-  ringHomomorphism           : RingHomomorphism M₁.rawRing M₂.rawRing →
-                               RingHomomorphism M₂.rawRing M₃.rawRing →
-                               RingHomomorphism M₁.rawRing M₃.rawRing
-  quasigroupHomomorphism     : QuasigroupHomomorphism M₁.rawQuasigroup M₂.rawQuasigroup →
-                               QuasigroupHomomorphism M₂.rawQuasigroup M₃.rawQuasigroup →
-                               QuasigroupHomomorphism M₁.rawQuasigroup M₃.rawQuasigroup
-  loopHomomorphism           : LoopHomomorphism M₁.rawLoop M₂.rawLoop →
-                               LoopHomomorphism M₂.rawLoop M₃.rawLoop →
-                               LoopHomomorphism M₁.rawLoop M₃.rawLoop
-  ```
-
-* In `Algebra.Morphism.Construct.Identity`:
-  ```agda
-  magmaHomomorphism          : MagmaHomomorphism M.rawMagma M.rawMagma
-  monoidHomomorphism         : MonoidHomomorphism M.rawMonoid M.rawMonoid
-  groupHomomorphism          : GroupHomomorphism M.rawGroup M.rawGroup
-  nearSemiringHomomorphism   : NearSemiringHomomorphism M.raw M.raw
-  semiringHomomorphism       : SemiringHomomorphism M.rawNearSemiring M.rawNearSemiring
-  kleeneAlgebraHomomorphism  : KleeneAlgebraHomomorphism M.rawKleeneAlgebra M.rawKleeneAlgebra
-  nearSemiringHomomorphism   : NearSemiringHomomorphism M.rawNearSemiring M.rawNearSemiring
-  ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M.rawRingWithoutOne M.rawRingWithoutOne
-  ringHomomorphism           : RingHomomorphism M.rawRing M.rawRing
-  quasigroupHomomorphism     : QuasigroupHomomorphism M.rawQuasigroup M.rawQuasigroup
-  loopHomomorphism           : LoopHomomorphism M.rawLoop M.rawLoop
-  ```
-
-* In `Algebra.Morphism.Structures.RingMorphisms`
-  ```agda
-  isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧
-  ```
-
-* In `Algebra.Morphism.Structures.RingWithoutOneMorphisms`
-  ```agda
-  isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧
-  ```
-
-* In `Algebra.Structures.IsSemiringWithoutOne`:
-  ```agda
-  distribˡ : * DistributesOverˡ +
-  distribʳ : * DistributesOverʳ +
-  +-cong : Congruent +
-  +-congˡ : LeftCongruent +
-  +-congʳ : RightCongruent +
-  +-assoc : Associative +
-  +-identity : Identity 0# +
-  +-identityˡ : LeftIdentity 0# +
-  +-identityʳ : RightIdentity 0# +
-  ```
-
-* Properties of non-divisibility in `Algebra.Properties.Magma.Divisibility`:
-  ```agda
-  ∤-respˡ-≈ : _∤_ Respectsˡ _≈_
-  ∤-respʳ-≈ : _∤_ Respectsʳ _≈_
-  ∤-resp-≈  : _∤_ Respects₂ _≈_
-  ∤∤-sym    : Symmetric _∤∤_
-  ∤∤-respˡ-≈ : _∤∤_ Respectsˡ _≈_
-  ∤∤-respʳ-≈ : _∤∤_ Respectsʳ _≈_
-  ∤∤-resp-≈  : _∤∤_ Respects₂ _≈_
-  ```
-
-* In `Algebra.Solver.Ring`
-  ```agda
-  Env : ℕ → Set _
-  Env = Vec Carrier
-  ```
-
-* In `Algebra.Structures.RingWithoutOne`:
-  ```agda
-  isNearSemiring      : IsNearSemiring _ _
-  ```
-
-* In `Data.List.Membership.Propositional.Properties`:
-  ```agda
-  ∈-AllPairs₂    : AllPairs R xs → x ∈ xs → y ∈ xs → x ≡ y ⊎ R x y ⊎ R y x
-  ∈-map∘filter⁻  : y ∈ map f (filter P? xs) → (∃[ x ] x ∈ xs × y ≡ f x × P x)
-  ∈-map∘filter⁺  : (∃[ x ] x ∈ xs × y ≡ f x × P x) → y ∈ map f (filter P? xs)
-  ∈-concatMap⁺   : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
-  ∈-concatMap⁻   : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
-  ++-∈⇔          : v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys)
-  []∉map∷        : [] ∉ map (x ∷_) xss
-  map∷⁻          : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × xs ≡ y ∷ ys
-  map∷-decomp∈   : (x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss
-  ∈-map∷⁻        : xs ∈ map (x ∷_) xss → x ∈ xs
-  ∉[]            : x ∉ []
-  deduplicate-∈⇔ : z ∈ xs ⇔ z ∈ deduplicate _≈?_ xs
-  ```
-
-* In `Data.List.Membership.Propositional.Properties.WithK`:
-  ```agda
-  unique∧set⇒bag : Unique xs → Unique ys → xs ∼[ set ] ys → xs ∼[ bag ] ys
-  ```
-
-* In `Data.List.Membership.Setoid.Properties`:
-  ```agda
-  ∉⇒All[≉]       : x ∉ xs → All (x ≉_) xs
-  All[≉]⇒∉       : All (x ≉_) xs → x ∉ xs
-  Any-∈-swap     : Any (_∈ ys) xs → Any (_∈ xs) ys
-  All-∉-swap     : All (_∉ ys) xs → All (_∉ xs) ys
-  ∈-map∘filter⁻  : y ∈₂ map f (filter P? xs) → ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x
-  ∈-map∘filter⁺  : f Preserves _≈₁_ ⟶ _≈₂_ →
-                   ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x →
-                   y ∈₂ map f (filter P? xs)
-  ∈-concatMap⁺   : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
-  ∈-concatMap⁻   : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
-  ∉[]            : x ∉ []
-  deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → z ∈ xs ⇔ z ∈ deduplicate R? xs
-  ```
-
-* In `Data.List.Properties`:
-  ```agda
-  product≢0    : All NonZero ns → NonZero (product ns)
-  ∈⇒≤product   : All NonZero ns → n ∈ ns → n ≤ product ns
-  concat-[_]   : concat ∘ [_] ≗ id
-  concatMap-++ : concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys
-  filter-≐     : P ≐ Q → filter P? ≗ filter Q?
-
-  partition-is-foldr : partition P? ≗ foldr (λ x → if does (P? x) then map₁ (x ∷_) else map₂ (x ∷_)) ([] , [])
-  ```
-
-* In `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
-  ```agda
-  deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys)
-  ```
-
-* In `Data.List.Relation.Binary.Disjoint.Setoid.Properties`:
-  ```agda
-  deduplicate⁺ : Disjoint S xs ys → Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys)
-  ```
-
-* In `Data.List.Relation.Binary.Equality.Setoid`:
-  ```agda
-  ++⁺ˡ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs
-  ++⁺ʳ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs
-  ```
-
-* In `Data.List.Relation.Binary.Permutation.Homogeneous`:
-  ```agda
-  steps : Permutation R xs ys → ℕ
-  ```
-
-* 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
-  ↭-reflexive-≋ : _≋_ ⇒ _↭_
-  ↭⇒↭ₛ          : _↭_  ⇒ _↭ₛ_
-  ↭ₛ⇒↭          : _↭ₛ_ ⇒ _↭_
-  ```
-  where `_↭ₛ_` is the `Setoid (setoid _)` instance of `Permutation`
-
-* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
-  ```agda
-  Any-resp-[σ∘σ⁻¹] : (σ : xs ↭ ys) (iy : Any P ys) →
-                     Any-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy
-  ∈-resp-[σ∘σ⁻¹]   : (σ : xs ↭ ys) (iy : y ∈ ys) →
-                     ∈-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy
-  product-↭        : product Preserves _↭_ ⟶ _≡_
-  sum-↭ : sum Preserves _↭_ ⟶ _≡_
-  ```
-
-* In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`:
-  ```agda
-  dedup-++-↭ : Disjoint xs ys →
-               deduplicate _≟_ (xs ++ ys) ↭ deduplicate _≟_ xs ++ deduplicate _≟_ ys
-  ```
-
-* In `Data.List.Relation.Binary.Permutation.Setoid`:
-  ```agda
-  ↭-reflexive-≋ : _≋_  ⇒ _↭_
-  ↭-transˡ-≋    : LeftTrans _≋_ _↭_
-  ↭-transʳ-≋    : RightTrans _↭_ _≋_
-  ↭-trans′      : Transitive _↭_
-  ```
-
-* 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
-  ```
-
-* In `Data.List.Relation.Binary.Pointwise`:
-  ```agda
-  ++⁺ˡ : Reflexive R → ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R)
-  ++⁺ʳ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
-  ```
-
-* In `Data.List.Relation.Binary.Sublist.Heterogeneous.Properties`:
-  ```agda
-  Sublist-[]-universal : Universal (Sublist R [])
-
-  module ⊆-Reasoning (≲ : Preorder a e r)
-  ```
-
-* In `Data.List.Relation.Binary.Sublist.Propositional.Properties`:
-  ```agda
-  ⊆⇒⊆ₛ : (S : Setoid a ℓ) → as ⊆ bs → as (SetoidSublist.⊆ S) bs
-  ```
-
-* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
-  ```agda
-  []⊆-universal : Universal ([] ⊆_)
-
-  module ⊆-Reasoning
-
-  concat⁺               : Sublist _⊆_ ass bss → concat ass ⊆ concat bss
-  xs∈xss⇒xs⊆concat[xss] : xs ∈ xss → xs ⊆ concat xss
-  all⊆concat            : (xss : List (List A)) → All (_⊆ concat xss) xss
-  ```
-
-* In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
-  ```agda
-  ∷⊈[]   : x ∷ xs ⊈ []
-  ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
-  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
-
-  concatMap⁺ : xs ⊆ ys → concatMap f xs ⊆ concatMap f ys
-  ```
-
-* In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
-  ```agda
-  ∷⊈[]   : x ∷ xs ⊈ []
-  ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
-  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
-  ```
-
-* In `Data.List.Relation.Unary.First.Properties`:
-  ```agda
-  ¬First⇒All : ∁ Q ⊆ P → ∁ (First P Q) ⊆ All P
-  ¬All⇒First : Decidable P → ∁ P ⊆ Q → ∁ (All P) ⊆ First P Q
-  ```
-
-* In `Data.List.Relation.Unary.All`:
-  ```agda
-  search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
-  ```
-
-* In `Data.List.Relation.Unary.All.Properties`:
-  ```agda
-  all⇒dropWhile≡[] : (P? : Decidable P) → All P xs → dropWhile P? xs ≡ []
-  all⇒takeWhile≗id : (P? : Decidable P) → All P xs → takeWhile P? xs ≡ xs
-  ```
-
-* In `Data.List.Relation.Unary.Any.Properties`:
-  ```agda
-  concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs)
-  concatMap⁻ : Any P (concatMap f xs) → Any (Any P ∘ f) xs
-  ```
-
-* In `Data.List.Relation.Unary.Unique.Propositional.Properties`:
-  ```agda
-  Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs
-  ```
-
-* In `Data.List.Relation.Unary.Unique.Setoid.Properties`:
-  ```agda
-  Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs
-  ```
-
-* In `Data.Maybe.Properties`:
-  ```agda
-  maybe′-∘ : ∀ f g → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b)
-  ```
-
-* New lemmas in `Data.Nat.Properties`:
-  ```agda
-  m≤n⇒m≤n*o : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ n * o
-  m≤n⇒m≤o*n : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ o * n
-  <‴-irrefl : Irreflexive _≡_ _<‴_
-  ≤‴-irrelevant : Irrelevant {A = ℕ} _≤‴_
-  <‴-irrelevant : Irrelevant {A = ℕ} _<‴_
-  >‴-irrelevant : Irrelevant {A = ℕ} _>‴_
-  ≥‴-irrelevant : Irrelevant {A = ℕ} _≥‴_
-  ```
-
-  Added adjunction between `suc` and `pred`
-  ```agda
-  suc[m]≤n⇒m≤pred[n] : suc m ≤ n → m ≤ pred n
-  m≤pred[n]⇒suc[m]≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n
-  ```
-
-* In `Data.Product.Function.Dependent.Propositional`:
-  ```agda
-  congˡ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B
-  ```
-
-* New lemmas in `Data.Rational.Properties`:
-  ```agda
-  nonNeg+nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p + q)
-  nonPos+nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonPositive (p + q)
-  pos+nonNeg⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : NonNegative q}} → Positive (p + q)
-  nonNeg+pos⇒pos : ∀ p .{{_ : NonNegative p}} q .{{_ : Positive q}} → Positive (p + q)
-  pos+pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p + q)
-  neg+nonPos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : NonPositive q}} → Negative (p + q)
-  nonPos+neg⇒neg : ∀ p .{{_ : NonPositive p}} q .{{_ : Negative q}} → Negative (p + q)
-  neg+neg⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Negative (p + q)
-  nonNeg*nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p * q)
-  nonPos*nonNeg⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonNegative q}} → NonPositive (p * q)
-  nonNeg*nonPos⇒nonPos : ∀ p .{{_ : NonNegative p}} q .{{_ : NonPositive q}} → NonPositive (p * q)
-  nonPos*nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonNegative (p * q)
-  pos*pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p * q)
-  neg*pos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Positive q}} → Negative (p * q)
-  pos*neg⇒neg : ∀ p .{{_ : Positive p}} q .{{_ : Negative q}} → Negative (p * q)
-  neg*neg⇒pos : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Positive (p * q)
-  ```
-
-* New properties re-exported from `Data.Refinement`:
-  ```agda
-  value-injective : value v ≡ value w → v ≡ w
-  _≟_             : DecidableEquality A → DecidableEquality [ x ∈ A ∣ P x ]
-  ```
-
-* New lemma in `Data.Vec.Properties`:
-  ```agda
-  map-concat : map f (concat xss) ≡ concat (map (map f) xss)
-  ```
-
-* New lemma in `Data.Vec.Relation.Binary.Equality.Cast`:
-  ```agda
-  ≈-cong′ : ∀ {f-len : ℕ → ℕ} (f : ∀ {n} → Vec A n → Vec B (f-len n))
-    {m n} {xs : Vec A m} {ys : Vec A n} .{eq} →
-    xs ≈[ eq ] ys → f xs ≈[ _ ] f ys
-  ```
-
-* In `Data.Vec.Relation.Binary.Equality.DecPropositional`:
-  ```agda
-  _≡?_ : DecidableEquality (Vec A n)
-  ```
-
-* In `Function.Related.TypeIsomorphisms`:
-  ```agda
-  Σ-distribˡ-⊎ : (∃ λ a → P a ⊎ Q a) ↔ (∃ P ⊎ ∃ Q)
-  Σ-distribʳ-⊎ : (Σ (A ⊎ B) P) ↔ (Σ A (P ∘ inj₁) ⊎ Σ B (P ∘ inj₂))
-  ×-distribˡ-⊎ : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C)
-  ×-distribʳ-⊎ : ((A ⊎ B) × C) ↔ (A × C ⊎ B × C)
-  ∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y)
-  ```
-
-* In `Relation.Binary.Bundles`:
-  ```agda
-  record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂))
-  ```
-  plus associated sub-bundles.
-
-* In `Relation.Binary.Construct.Interior.Symmetric`:
-  ```agda
-  decidable         : Decidable R → Decidable (SymInterior R)
-  ```
-  and for `Reflexive` and `Transitive` relations `R`:
-  ```agda
-  isDecEquivalence  : Decidable R → IsDecEquivalence (SymInterior R)
-  isDecPreorder     : Decidable R → IsDecPreorder (SymInterior R) R
-  isDecPartialOrder : Decidable R → IsDecPartialOrder (SymInterior R) R
-  decPreorder       : Decidable R → DecPreorder _ _ _
-  decPoset          : Decidable R → DecPoset _ _ _
-  ```
-
-* In `Relation.Binary.Structures`:
-  ```agda
-  record IsDecPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
-    field
-      isPreorder : IsPreorder _≲_
-      _≟_        : Decidable _≈_
-      _≲?_       : Decidable _≲_
-  ```
-  plus associated `isDecPreorder` fields in each higher `IsDec*Order` structure.
-
-* In `Relation.Binary.Bundles` added `rawX` (e.g. `RawSetoid`) fields to each bundle.
-
-* In `Relation.Nullary.Decidable`:
-  ```agda
-  does-⇔  : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b?
-  does-≡  : (a? b? : Dec A) → does a? ≡ does b?
-  ```
-
-* In `Relation.Nullary.Recomputable`:
-  ```agda
-  irrelevant-recompute : Recomputable (Irrelevant A)
-  ```
-
-* In `Relation.Unary.Properties`:
-  ```agda
-  map    : P ≐ Q → Decidable P → Decidable Q
-  does-≐ : P ≐ Q → (P? : Decidable P) → (Q? : Decidable Q) → does ∘ P? ≗ does ∘ Q?
-  does-≡ : (P? P?′ : Decidable P) → does ∘ P? ≗ does ∘ P?′
-  ```

From d98b25778f53ae11030f5fcda57d1c33a29cfd72 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 16 Jan 2025 17:03:25 +0000
Subject: [PATCH 5/8] refactor: move and deprecate

---
 CHANGELOG.md                    |  8 ++++
 src/Data/List/Properties.agda   | 83 +++++++++++++++++++--------------
 src/Data/Nat/SumAndProduct.agda | 61 +++++++++++++++++++++++-
 3 files changed, 114 insertions(+), 38 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d020d141d3..c5cf1a5a04 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -27,6 +27,14 @@ Deprecated names
   product   ↦  Data.Nat.SumAndProduct.product
   ```
 
+* In `Data.List.Properties`:
+  ```agda
+  sum-++       ↦  Data.Nat.SumAndProduct.sum-++
+  ∈⇒∣product   ↦  Data.Nat.SumAndProduct.∈⇒∣product
+  product≢0    ↦  Data.Nat.SumAndProduct.product≢0
+  ∈⇒≤product   ↦  Data.Nat.SumAndProduct.∈⇒≤product
+  ```
+
 New modules
 -----------
 
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index c6d9faea11..f4069f33a9 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -21,13 +21,11 @@ import Algebra.Structures as AlgebraicStructures
 open import Data.Bool.Base using (Bool; false; true; not; if_then_else_)
 open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ)
 open import Data.List.Base as List
-open import Data.List.Membership.Propositional using (_∈_)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.Any using (just) renaming (Any to MAny)
 open import Data.Nat.Base
-open import Data.Nat.Divisibility using (_∣_; divides; ∣n⇒∣m*n)
 open import Data.Nat.Properties
 open import Data.Product.Base as Product
   using (_×_; _,_; uncurry; uncurry′; proj₁; proj₂; <_,_>)
@@ -829,34 +827,6 @@ mapMaybeIsInj₂∘mapInj₂ = mapMaybe-map-retract λ _ → refl
 mapMaybeIsInj₂∘mapInj₁ : (xs : List A) → mapMaybe (isInj₂ {B = B}) (map inj₁ xs) ≡ []
 mapMaybeIsInj₂∘mapInj₁ = mapMaybe-map-none λ _ → refl
 
-------------------------------------------------------------------------
--- sum
-
-sum-++ : ∀ xs ys → sum (xs ++ ys) ≡ sum xs + sum ys
-sum-++ []       ys = refl
-sum-++ (x ∷ xs) ys = begin
-  x + sum (xs ++ ys)     ≡⟨ cong (x +_) (sum-++ xs ys) ⟩
-  x + (sum xs + sum ys)  ≡⟨ sym (+-assoc x _ _) ⟩
-  (x + sum xs) + sum ys  ∎
-
-------------------------------------------------------------------------
--- product
-
-∈⇒∣product : ∀ {n ns} → n ∈ ns → n ∣ product ns
-∈⇒∣product {n} {n ∷ ns} (here  refl) = divides (product ns) (*-comm n (product ns))
-∈⇒∣product {n} {m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns)
-
-product≢0 : ∀ {ns} → All NonZero ns → NonZero (product ns)
-product≢0 [] = _
-product≢0 {n ∷ ns} (n≢0 ∷ ns≢0) = m*n≢0 n (product ns) {{n≢0}} {{product≢0 ns≢0}}
-
-∈⇒≤product : ∀ {n ns} → All NonZero ns → n ∈ ns → n ≤ product ns
-∈⇒≤product {ns = n ∷ ns} (_ ∷ ns≢0) (here refl) =
-  m≤m*n n (product ns) {{product≢0 ns≢0}}
-∈⇒≤product {ns = n ∷ _} (n≢0 ∷ ns≢0) (there n∈ns) =
-  m≤n⇒m≤o*n n {{n≢0}} (∈⇒≤product ns≢0 n∈ns)
-
-
 ------------------------------------------------------------------------
 -- applyUpTo
 
@@ -1565,12 +1535,6 @@ map-++-commute = map-++
 Please use map-++ instead."
 #-}
 
-sum-++-commute = sum-++
-{-# WARNING_ON_USAGE sum-++-commute
-"Warning: map-++-commute was deprecated in v2.0.
-Please use map-++ instead."
-#-}
-
 reverse-map-commute = reverse-map
 {-# WARNING_ON_USAGE reverse-map-commute
 "Warning: reverse-map-commute was deprecated in v2.0.
@@ -1658,3 +1622,50 @@ concat-[-] = concat-map-[_]
 "Warning: concat-[-] was deprecated in v2.2.
 Please use concat-map-[_] instead."
 #-}
+
+-- Version 2.3
+
+sum-++ : ∀ xs ys → sum (xs ++ ys) ≡ sum xs + sum ys
+sum-++ []       ys = refl
+sum-++ (x ∷ xs) ys = begin
+  x + sum (xs ++ ys)     ≡⟨ cong (x +_) (sum-++ xs ys) ⟩
+  x + (sum xs + sum ys)  ≡⟨ +-assoc x _ _ ⟨
+  (x + sum xs) + sum ys  ∎
+{-# WARNING_ON_USAGE sum-++
+"Warning: sum-++ was deprecated in v2.3.
+Please use Data.Nat.SumAndProperties.sum-++ instead."
+#-}
+sum-++-commute = sum-++
+{-# WARNING_ON_USAGE sum-++-commute
+"Warning: sum-++-commute was deprecated in v2.0.
+Please use Data.Nat.SumAndProperties.sum-++ instead."
+#-}
+
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.Nat.Divisibility using (_∣_; m∣m*n; ∣n⇒∣m*n)
+
+∈⇒∣product : ∀ {n ns} → n ∈ ns → n ∣ product ns
+∈⇒∣product {ns = n ∷ ns} (here  refl) = m∣m*n (product ns)
+∈⇒∣product {ns = m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns)
+{-# WARNING_ON_USAGE ∈⇒∣product
+"Warning: ∈⇒∣product was deprecated in v2.3.
+Please use Data.Nat.SumAndProperties.∈⇒∣product instead."
+#-}
+
+product≢0 : ∀ {ns} → All NonZero ns → NonZero (product ns)
+product≢0 [] = _
+product≢0 {n ∷ ns} (n≢0 ∷ ns≢0) = m*n≢0 n (product ns) {{n≢0}} {{product≢0 ns≢0}}
+{-# WARNING_ON_USAGE product≢0
+"Warning: product≢0 was deprecated in v2.3.
+Please use Data.Nat.SumAndProperties.product≢0 instead."
+#-}
+
+∈⇒≤product : ∀ {n ns} → All NonZero ns → n ∈ ns → n ≤ product ns
+∈⇒≤product {ns = n ∷ ns} (_ ∷ ns≢0) (here refl) =
+  m≤m*n n (product ns) {{product≢0 ns≢0}}
+∈⇒≤product {ns = n ∷ _} (n≢0 ∷ ns≢0) (there n∈ns) =
+  m≤n⇒m≤o*n n {{n≢0}} (∈⇒≤product ns≢0 n∈ns)
+{-# WARNING_ON_USAGE ∈⇒≤product
+"Warning: ∈⇒≤product was deprecated in v2.3.
+Please use Data.Nat.SumAndProperties.∈⇒≤product instead."
+#-}
diff --git a/src/Data/Nat/SumAndProduct.agda b/src/Data/Nat/SumAndProduct.agda
index c0b3061dc1..bf0971a9d4 100644
--- a/src/Data/Nat/SumAndProduct.agda
+++ b/src/Data/Nat/SumAndProduct.agda
@@ -2,17 +2,74 @@
 -- The Agda standard library
 --
 -- Natural numbers: sum and product of lists
+--
+-- Issue #2553: this is a compatibility stub module,
+-- ahead of a more thorough breaking set of changes.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
 module Data.Nat.SumAndProduct where
 
-open import Data.Nat.Base using (ℕ; _+_; _*_)
-open import Data.List.Base using (List; foldr)
+open import Data.List.Base using (List; []; _∷_; _++_; foldr)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Relation.Unary.All using (All; []; _∷_)
+open import Data.List.Relation.Unary.Any using (here; there)
+open import Data.Nat.Base using (ℕ; _+_; _*_; NonZero; _≤_)
+open import Data.Nat.Divisibility using (_∣_; m∣m*n; ∣n⇒∣m*n)
+open import Data.Nat.Properties
+  using (+-assoc; *-assoc; *-identityˡ; m*n≢0; m≤m*n; m≤n⇒m≤o*n)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; refl; sym; cong)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
+
+private
+  variable
+    m n : ℕ
+    ms ns : List ℕ
+
+
+------------------------------------------------------------------------
+-- Definitions
 
 sum : List ℕ → ℕ
 sum = foldr _+_ 0
 
 product : List ℕ → ℕ
 product = foldr _*_ 1
+
+------------------------------------------------------------------------
+-- Properties
+
+-- sum
+
+sum-++ : ∀ ms ns → sum (ms ++ ns) ≡ sum ms + sum ns
+sum-++ []       ns = refl
+sum-++ (m ∷ ms) ns = begin
+  m + sum (ms ++ ns)     ≡⟨ cong (m +_) (sum-++ ms ns) ⟩
+  m + (sum ms + sum ns)  ≡⟨ +-assoc m _ _ ⟨
+  (m + sum ms) + sum ns  ∎
+  where open ≡-Reasoning
+
+-- product
+
+product-++ : ∀ ms ns → product (ms ++ ns) ≡ product ms * product ns
+product-++ []       ns = sym (*-identityˡ _)
+product-++ (m ∷ ms) ns = begin
+  m * product (ms ++ ns)         ≡⟨ cong (m *_) (product-++ ms ns) ⟩
+  m * (product ms * product ns)  ≡⟨ *-assoc m _ _ ⟨
+  (m * product ms) * product ns  ∎
+  where open ≡-Reasoning
+
+∈⇒∣product : n ∈ ns → n ∣ product ns
+∈⇒∣product {ns = n ∷ ns} (here  refl) = m∣m*n (product ns)
+∈⇒∣product {ns = m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns)
+
+product≢0 : All NonZero ns → NonZero (product ns)
+product≢0 []           = _
+product≢0 (n≢0 ∷ ns≢0) = m*n≢0 _ _ {{n≢0}} {{product≢0 ns≢0}}
+
+∈⇒≤product : All NonZero ns → n ∈ ns → n ≤ product ns
+∈⇒≤product (n≢0 ∷ ns≢0) (here refl)  = m≤m*n _ _ {{product≢0 ns≢0}}
+∈⇒≤product (n≢0 ∷ ns≢0) (there n∈ns) = m≤n⇒m≤o*n _ {{n≢0}} (∈⇒≤product ns≢0 n∈ns)

From 56d0a744127f00d08251f63008a8addf399c9444 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 16 Jan 2025 18:36:25 +0000
Subject: [PATCH 6/8] refactor: move+deprecate

---
 CHANGELOG.md                                  |  6 +++
 doc/README/Data/List.agda                     |  3 +-
 src/Data/List/Properties.agda                 |  2 +-
 .../Permutation/Propositional/Properties.agda | 41 ++++++++++---------
 src/Data/Nat/Primality.agda                   |  4 +-
 src/Data/Nat/Primality/Factorisation.agda     |  5 ++-
 src/Data/Nat/SumAndProduct.agda               | 17 +++++++-
 src/Data/Tree/Binary/Zipper.agda              |  3 +-
 src/Data/Tree/Binary/Zipper/Properties.agda   |  3 +-
 src/Test/Golden.agda                          |  5 ++-
 src/Text/Format/Generic.agda                  |  5 ++-
 11 files changed, 62 insertions(+), 32 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c5cf1a5a04..682569e56e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -35,6 +35,12 @@ Deprecated names
   ∈⇒≤product   ↦  Data.Nat.SumAndProduct.∈⇒≤product
   ```
 
+* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
+  ```agda
+  sum-↭       ↦  Data.Nat.SumAndProduct.sum-↭
+  product-↭   ↦  Data.Nat.SumAndProduct.product-↭
+  ```
+
 New modules
 -----------
 
diff --git a/doc/README/Data/List.agda b/doc/README/Data/List.agda
index 2c284daa78..eaf46ee9ec 100644
--- a/doc/README/Data/List.agda
+++ b/doc/README/Data/List.agda
@@ -7,6 +7,7 @@
 module README.Data.List where
 
 open import Data.Nat.Base using (ℕ; _+_)
+open import Data.Nat.SumAndProduct using (sum)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 
 ------------------------------------------------------------------------
@@ -18,7 +19,7 @@ open import Data.List
   using
   (List
   ; []; _∷_
-  ; sum; map; take; reverse; _++_; drop
+  ; map; take; reverse; _++_; drop
   )
 
 -- Lists are built using the "[]" and "_∷_" constructors.
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index f4069f33a9..f12da99940 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -1504,7 +1504,7 @@ module _ (f : A → B) where
 
 
 ------------------------------------------------------------------------
--- DEPRECATED
+-- DEPRECATED NAMES
 ------------------------------------------------------------------------
 -- Please use the new names as continuing support for the old names is
 -- not guaranteed.
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index d31071834f..939003b9be 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -15,7 +15,7 @@ open import Data.Bool.Base using (Bool; true; false)
 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.Base as List hiding (sum; product)
 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; []; _∷_)
@@ -372,24 +372,6 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where
     x ∷ xs ++ y ∷ ys         ∎
     where open PermutationReasoning
 
-------------------------------------------------------------------------
--- sum
-
-sum-↭ : sum Preserves _↭_ ⟶ _≡_
-sum-↭ p = foldr-commMonoid ℕ-+-0.isCommutativeMonoid (↭⇒↭ₛ p)
-  where
-  module ℕ-+-0 = CommutativeMonoid ℕ.+-0-commutativeMonoid
-  open Permutation ℕ-+-0.setoid
-
-------------------------------------------------------------------------
--- product
-
-product-↭ : product Preserves _↭_ ⟶ _≡_
-product-↭ p = foldr-commMonoid ℕ-*-1.isCommutativeMonoid (↭⇒↭ₛ p)
-  where
-  module ℕ-*-1 = CommutativeMonoid ℕ.*-1-commutativeMonoid
-  open Permutation ℕ-*-1.setoid
-
 ------------------------------------------------------------------------
 -- catMaybes
 
@@ -408,3 +390,24 @@ catMaybes-↭ (swap (just x) (just y) xs↭) = swap x y $ catMaybes-↭ xs↭
 
 mapMaybe-↭ : (f : A → Maybe B) → xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
 mapMaybe-↭ f = catMaybes-↭ ∘ map⁺ f
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.3
+
+open import Data.Nat.SumAndProduct public
+  using (sum-↭; product-↭)
+
+{-# WARNING_ON_USAGE sum-↭
+"Warning: sum-↭ was deprecated in v2.3.
+Please use Data.Nat.SumAndProduct.sum-↭ instead."
+#-}
+{-# WARNING_ON_USAGE product-↭
+"Warning: product-↭ was deprecated in v2.3.
+Please use Data.Nat.SumAndProduct.product-↭ instead."
+#-}
diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda
index ad7283235e..c4cf0a4c88 100644
--- a/src/Data/Nat/Primality.agda
+++ b/src/Data/Nat/Primality.agda
@@ -8,13 +8,13 @@
 
 module Data.Nat.Primality where
 
-open import Data.List.Base using ([]; _∷_; product)
-open import Data.List.Properties using (product≢0)
+open import Data.List.Base using ([]; _∷_)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.Nat.Base
 open import Data.Nat.Divisibility
 open import Data.Nat.GCD using (module GCD; module Bézout)
 open import Data.Nat.Properties
+open import Data.Nat.SumAndProduct using (product; product≢0)
 open import Data.Product.Base using (∃-syntax; _×_; map₂; _,_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (flip; _∘_; _∘′_)
diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda
index 4a91348a66..89b107ef26 100644
--- a/src/Data/Nat/Primality/Factorisation.agda
+++ b/src/Data/Nat/Primality/Factorisation.agda
@@ -17,8 +17,9 @@ open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder)
 open import Data.Nat.Primality
   using (Prime; _Rough_; rough∧square>⇒prime; ∤⇒rough-suc; rough∧∣⇒rough; rough∧∣⇒prime;
          2-rough; euclidsLemma; prime⇒irreducible; ¬prime[1]; productOfPrimes≥1; prime⇒nonZero)
+open import Data.Nat.SumAndProduct using (product; product-↭)
 open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₁; proj₂)
-open import Data.List.Base using (List; []; _∷_; _++_; product)
+open import Data.List.Base using (List; []; _∷_; _++_)
 open import Data.List.Membership.Propositional using (_∈_)
 open import Data.List.Membership.Propositional.Properties using (∈-∃++)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
@@ -26,7 +27,7 @@ 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 (All-resp-↭; shift)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_$_; _∘_; _|>_; flip)
 open import Induction using (build)
diff --git a/src/Data/Nat/SumAndProduct.agda b/src/Data/Nat/SumAndProduct.agda
index bf0971a9d4..f66b224c91 100644
--- a/src/Data/Nat/SumAndProduct.agda
+++ b/src/Data/Nat/SumAndProduct.agda
@@ -11,14 +11,20 @@
 
 module Data.Nat.SumAndProduct where
 
+open import Algebra.Bundles using (CommutativeMonoid)
 open import Data.List.Base using (List; []; _∷_; _++_; foldr)
 open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭⇒↭ₛ)
+open import Data.List.Relation.Binary.Permutation.Setoid.Properties
+  using (foldr-commMonoid)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (here; there)
 open import Data.Nat.Base using (ℕ; _+_; _*_; NonZero; _≤_)
 open import Data.Nat.Divisibility using (_∣_; m∣m*n; ∣n⇒∣m*n)
 open import Data.Nat.Properties
-  using (+-assoc; *-assoc; *-identityˡ; m*n≢0; m≤m*n; m≤n⇒m≤o*n)
+  using (+-assoc; *-assoc; *-identityˡ; m*n≢0; m≤m*n; m≤n⇒m≤o*n;
+         +-0-commutativeMonoid; *-1-commutativeMonoid)
+open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; sym; cong)
 open import Relation.Binary.PropositionalEquality.Properties
@@ -52,6 +58,11 @@ sum-++ (m ∷ ms) ns = begin
   (m + sum ms) + sum ns  ∎
   where open ≡-Reasoning
 
+sum-↭ : sum Preserves _↭_ ⟶ _≡_
+sum-↭ p = foldr-commMonoid ℕ-+-0.setoid ℕ-+-0.isCommutativeMonoid (↭⇒↭ₛ p)
+  where module ℕ-+-0 = CommutativeMonoid +-0-commutativeMonoid
+
+
 -- product
 
 product-++ : ∀ ms ns → product (ms ++ ns) ≡ product ms * product ns
@@ -73,3 +84,7 @@ product≢0 (n≢0 ∷ ns≢0) = m*n≢0 _ _ {{n≢0}} {{product≢0 ns≢0}}
 ∈⇒≤product : All NonZero ns → n ∈ ns → n ≤ product ns
 ∈⇒≤product (n≢0 ∷ ns≢0) (here refl)  = m≤m*n _ _ {{product≢0 ns≢0}}
 ∈⇒≤product (n≢0 ∷ ns≢0) (there n∈ns) = m≤n⇒m≤o*n _ {{n≢0}} (∈⇒≤product ns≢0 n∈ns)
+
+product-↭ : product Preserves _↭_ ⟶ _≡_
+product-↭ p = foldr-commMonoid ℕ-*-1.setoid ℕ-*-1.isCommutativeMonoid (↭⇒↭ₛ p)
+  where module ℕ-*-1 = CommutativeMonoid *-1-commutativeMonoid
diff --git a/src/Data/Tree/Binary/Zipper.agda b/src/Data/Tree/Binary/Zipper.agda
index 3024b125ca..7b27f37d9b 100644
--- a/src/Data/Tree/Binary/Zipper.agda
+++ b/src/Data/Tree/Binary/Zipper.agda
@@ -10,9 +10,10 @@ module Data.Tree.Binary.Zipper where
 
 open import Level using (Level; _⊔_)
 open import Data.Tree.Binary as BT using (Tree; node; leaf)
-open import Data.List.Base as List using (List; []; _∷_; sum; _++_; [_])
+open import Data.List.Base as List using (List; []; _∷_; _++_; [_])
 open import Data.Maybe.Base using (Maybe; nothing; just)
 open import Data.Nat.Base using (ℕ; suc; _+_)
+open import Data.Nat.SumAndProduct using (sum)
 open import Function.Base using (_$_; _∘_)
 
 private
diff --git a/src/Data/Tree/Binary/Zipper/Properties.agda b/src/Data/Tree/Binary/Zipper/Properties.agda
index 03a88b09d2..88be616cad 100644
--- a/src/Data/Tree/Binary/Zipper/Properties.agda
+++ b/src/Data/Tree/Binary/Zipper/Properties.agda
@@ -8,11 +8,12 @@
 
 module Data.Tree.Binary.Zipper.Properties where
 
-open import Data.List.Base as List using (List ; [] ; _∷_; sum)
+open import Data.List.Base as List using (List ; [] ; _∷_)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.All using (All; just; nothing)
 open import Data.Nat.Base using (ℕ; suc; _+_)
 open import Data.Nat.Properties using (+-identityʳ; +-comm; +-assoc)
+open import Data.Nat.SumAndProduct using (sum)
 open import Data.Tree.Binary as BT using (Tree; node; leaf)
 open import Data.Tree.Binary.Zipper using (Zipper; toTree; up; mkZipper;
   leftBranch; rightBranch; left; right; #nodes; Crumb; getTree; #leaves;
diff --git a/src/Test/Golden.agda b/src/Test/Golden.agda
index 7e592a3ff2..804e221db0 100644
--- a/src/Test/Golden.agda
+++ b/src/Test/Golden.agda
@@ -22,7 +22,7 @@
 --   * Use `$1` as the variable standing for the Agda executable to be tested
 --   * Clean up after itself (e.g. by running `rm -rf build/`)
 --
--- + `expected` a file containting the expected output of `run`
+-- + `expected` a file containing the expected output of `run`
 --
 -- During testing, the test harness will generate an `output` file.
 -- It will be compared to the `expected` golden file provided by the user.
@@ -88,6 +88,7 @@ open import Data.List.Relation.Binary.Infix.Heterogeneous.Properties using (infi
 open import Data.List.Relation.Unary.Any using (any?)
 open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe)
 open import Data.Nat.Base using (ℕ; _≡ᵇ_; _<ᵇ_; _+_; _∸_)
+open import Data.Nat.SumAndProduct using (sum)
 import Data.Nat.Show as ℕ using (show)
 open import Data.Product.Base using (_×_; _,_)
 open import Data.String.Base as String using (String; lines; unlines; unwords; concat)
@@ -306,7 +307,7 @@ runTest opts testPath = do
     printTiming false _    msg = putStrLn $ concat (testPath ∷ ": " ∷ msg ∷ [])
     printTiming true  time msg =
       let time  = ℕ.show (time .seconds) String.++ "s"
-          spent = 9 + List.sum (List.map String.length (testPath ∷ time ∷ []))
+          spent = 9 + sum (List.map String.length (testPath ∷ time ∷ []))
                -- ^ hack: both "success" and "FAILURE" have the same length
                --   can't use `String.length msg` because the msg contains escape codes
           pad   = String.replicate (72 ∸ spent) ' '
diff --git a/src/Text/Format/Generic.agda b/src/Text/Format/Generic.agda
index 9969801832..a9116b9856 100644
--- a/src/Text/Format/Generic.agda
+++ b/src/Text/Format/Generic.agda
@@ -11,9 +11,10 @@ module Text.Format.Generic where
 open import Level using (0ℓ)
 open import Effect.Applicative
 open import Data.Char.Base using (Char)
-open import Data.List.Base as List
+open import Data.List.Base as List hiding (sum)
 open import Data.Maybe.Base as Maybe
 open import Data.Nat.Base
+open import Data.Nat.SumAndProduct using (sum)
 open import Data.Product.Base using (_,_)
 open import Data.Product.Nary.NonDependent
 open import Data.Sum.Base
@@ -63,7 +64,7 @@ module Format (spec : FormatSpec) where
   -- Semantics
 
   size : Format → ℕ
-  size = List.sum ∘′ List.map λ { (Raw _) → 0; _ → 1 }
+  size = sum ∘′ List.map λ { (Raw _) → 0; _ → 1 }
 
   -- Meaning of a format as a list of value types
 

From e37fe01dbf5a9b12b880feeb54872e697e3a8bb1 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 17 Jan 2025 12:24:05 +0000
Subject: [PATCH 7/8] refactor: cosmetic, tighten `import`s

---
 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 89b107ef26..b41eef323b 100644
--- a/src/Data/Nat/Primality/Factorisation.agda
+++ b/src/Data/Nat/Primality/Factorisation.agda
@@ -25,7 +25,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 (_↭_; prep; swap; ↭-reflexive; ↭-refl; ↭-trans; refl; module PermutationReasoning)
+  using (_↭_; ↭-reflexive; ↭-refl; ↭-trans; module PermutationReasoning)
 open import Data.List.Relation.Binary.Permutation.Propositional.Properties
   using (All-resp-↭; shift)
 open import Data.Sum.Base using (inj₁; inj₂)
@@ -147,7 +147,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

From c1423d2a12342f8f2efdc77af2bd7e36e2303239 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 17 Jan 2025 12:29:59 +0000
Subject: [PATCH 8/8] refactor: fix deprecation problem

---
 .../Binary/Permutation/Propositional/Properties.agda         | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index 939003b9be..b39140e158 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -400,13 +400,14 @@ mapMaybe-↭ f = catMaybes-↭ ∘ map⁺ f
 
 -- Version 2.3
 
-open import Data.Nat.SumAndProduct public
-  using (sum-↭; product-↭)
+import Data.Nat.SumAndProduct as ℕ
 
+sum-↭ = ℕ.sum-↭
 {-# WARNING_ON_USAGE sum-↭
 "Warning: sum-↭ was deprecated in v2.3.
 Please use Data.Nat.SumAndProduct.sum-↭ instead."
 #-}
+product-↭ = ℕ.product-↭
 {-# WARNING_ON_USAGE product-↭
 "Warning: product-↭ was deprecated in v2.3.
 Please use Data.Nat.SumAndProduct.product-↭ instead."