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 01/12] 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 02/12] 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 03/12] 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 04/12] 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 05/12] 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 06/12] 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 07/12] 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 08/12] 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."

From e871651658b958d0bdd8b3cb645adb62b3b8fd6c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 22 Jan 2025 10:37:23 +0000
Subject: [PATCH 09/12] refactor: renamed new module

---
 CHANGELOG.md                                   | 18 +++++++++---------
 doc/README/Data/List.agda                      |  2 +-
 src/Data/List/Base.agda                        |  4 ++--
 .../Permutation/Propositional/Properties.agda  |  6 +++---
 .../{SumAndProduct.agda => ListAction.agda}    |  2 +-
 src/Data/Nat/Primality.agda                    |  2 +-
 src/Data/Nat/Primality/Factorisation.agda      |  2 +-
 src/Data/Tree/Binary/Zipper.agda               |  2 +-
 src/Data/Tree/Binary/Zipper/Properties.agda    |  2 +-
 src/Test/Golden.agda                           |  2 +-
 src/Text/Format/Generic.agda                   |  2 +-
 11 files changed, 22 insertions(+), 22 deletions(-)
 rename src/Data/Nat/{SumAndProduct.agda => ListAction.agda} (98%)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 682569e56e..4229a49d02 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -23,28 +23,28 @@ Deprecated names
 
 * In `Data.List.Base`:
   ```agda
-  sum       ↦  Data.Nat.SumAndProduct.sum
-  product   ↦  Data.Nat.SumAndProduct.product
+  sum       ↦  Data.Nat.ListAction.sum
+  product   ↦  Data.Nat.ListAction.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
+  sum-++       ↦  Data.Nat.ListAction.sum-++
+  ∈⇒∣product   ↦  Data.Nat.ListAction.∈⇒∣product
+  product≢0    ↦  Data.Nat.ListAction.product≢0
+  ∈⇒≤product   ↦  Data.Nat.ListAction.∈⇒≤product
   ```
 
 * In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
   ```agda
-  sum-↭       ↦  Data.Nat.SumAndProduct.sum-↭
-  product-↭   ↦  Data.Nat.SumAndProduct.product-↭
+  sum-↭       ↦  Data.Nat.ListAction.sum-↭
+  product-↭   ↦  Data.Nat.ListAction.product-↭
   ```
 
 New modules
 -----------
 
-* `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.SumAndProduct`.
+* `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction`.
 
 Additions to existing modules
 -----------------------------
diff --git a/doc/README/Data/List.agda b/doc/README/Data/List.agda
index eaf46ee9ec..e47eb9ea1f 100644
--- a/doc/README/Data/List.agda
+++ b/doc/README/Data/List.agda
@@ -7,7 +7,7 @@
 module README.Data.List where
 
 open import Data.Nat.Base using (ℕ; _+_)
-open import Data.Nat.SumAndProduct using (sum)
+open import Data.Nat.ListAction using (sum)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 59b66ab4ab..aba8a90ef7 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -581,13 +581,13 @@ sum : List ℕ → ℕ
 sum = foldr ℕ._+_ 0
 {-# WARNING_ON_USAGE sum
 "Warning: sum was deprecated in v2.3.
-Please use Data.Nat.SumAndProduct.sum instead."
+Please use Data.Nat.ListAction.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."
+Please use Data.Nat.ListAction.product instead."
 #-}
 
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index b39140e158..b697367cd5 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -400,15 +400,15 @@ mapMaybe-↭ f = catMaybes-↭ ∘ map⁺ f
 
 -- Version 2.3
 
-import Data.Nat.SumAndProduct as ℕ
+import Data.Nat.ListAction as ℕ
 
 sum-↭ = ℕ.sum-↭
 {-# WARNING_ON_USAGE sum-↭
 "Warning: sum-↭ was deprecated in v2.3.
-Please use Data.Nat.SumAndProduct.sum-↭ instead."
+Please use Data.Nat.ListAction.sum-↭ instead."
 #-}
 product-↭ = ℕ.product-↭
 {-# WARNING_ON_USAGE product-↭
 "Warning: product-↭ was deprecated in v2.3.
-Please use Data.Nat.SumAndProduct.product-↭ instead."
+Please use Data.Nat.ListAction.product-↭ instead."
 #-}
diff --git a/src/Data/Nat/SumAndProduct.agda b/src/Data/Nat/ListAction.agda
similarity index 98%
rename from src/Data/Nat/SumAndProduct.agda
rename to src/Data/Nat/ListAction.agda
index f66b224c91..dd6f2da811 100644
--- a/src/Data/Nat/SumAndProduct.agda
+++ b/src/Data/Nat/ListAction.agda
@@ -9,7 +9,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-module Data.Nat.SumAndProduct where
+module Data.Nat.ListAction where
 
 open import Algebra.Bundles using (CommutativeMonoid)
 open import Data.List.Base using (List; []; _∷_; _++_; foldr)
diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda
index c4cf0a4c88..6965c35430 100644
--- a/src/Data/Nat/Primality.agda
+++ b/src/Data/Nat/Primality.agda
@@ -14,7 +14,7 @@ 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.Nat.ListAction 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 b41eef323b..70c7a06abd 100644
--- a/src/Data/Nat/Primality/Factorisation.agda
+++ b/src/Data/Nat/Primality/Factorisation.agda
@@ -17,7 +17,7 @@ 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.Nat.ListAction using (product; product-↭)
 open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₁; proj₂)
 open import Data.List.Base using (List; []; _∷_; _++_)
 open import Data.List.Membership.Propositional using (_∈_)
diff --git a/src/Data/Tree/Binary/Zipper.agda b/src/Data/Tree/Binary/Zipper.agda
index 7b27f37d9b..75017d1195 100644
--- a/src/Data/Tree/Binary/Zipper.agda
+++ b/src/Data/Tree/Binary/Zipper.agda
@@ -13,7 +13,7 @@ open import Data.Tree.Binary as BT using (Tree; node; leaf)
 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 Data.Nat.ListAction 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 88be616cad..c4307fcb1e 100644
--- a/src/Data/Tree/Binary/Zipper/Properties.agda
+++ b/src/Data/Tree/Binary/Zipper/Properties.agda
@@ -13,7 +13,7 @@ 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.Nat.ListAction 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 804e221db0..ecababe7c8 100644
--- a/src/Test/Golden.agda
+++ b/src/Test/Golden.agda
@@ -88,7 +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)
+open import Data.Nat.ListAction 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)
diff --git a/src/Text/Format/Generic.agda b/src/Text/Format/Generic.agda
index a9116b9856..fd1f05ec1c 100644
--- a/src/Text/Format/Generic.agda
+++ b/src/Text/Format/Generic.agda
@@ -14,7 +14,7 @@ open import Data.Char.Base using (Char)
 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.Nat.ListAction using (sum)
 open import Data.Product.Base using (_,_)
 open import Data.Product.Nary.NonDependent
 open import Data.Sum.Base

From a2e7f549fb87cefc22655e2ac4c7c1a0ebc8f5de Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 23 Jan 2025 08:20:46 +0000
Subject: [PATCH 10/12] refactor: introduce `Properties` module

---
 CHANGELOG.md                                  | 14 ++--
 src/Data/List/Base.agda                       |  1 -
 src/Data/List/Properties.agda                 | 10 +--
 .../Permutation/Propositional/Properties.agda |  2 +-
 src/Data/Nat/ListAction.agda                  | 67 +------------------
 src/Data/Nat/Primality.agda                   |  3 +-
 src/Data/Nat/Primality/Factorisation.agda     |  3 +-
 7 files changed, 18 insertions(+), 82 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4229a49d02..1a1ff7af1a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -29,22 +29,22 @@ Deprecated names
 
 * In `Data.List.Properties`:
   ```agda
-  sum-++       ↦  Data.Nat.ListAction.sum-++
-  ∈⇒∣product   ↦  Data.Nat.ListAction.∈⇒∣product
-  product≢0    ↦  Data.Nat.ListAction.product≢0
-  ∈⇒≤product   ↦  Data.Nat.ListAction.∈⇒≤product
+  sum-++       ↦  Data.Nat.ListAction.Properties.sum-++
+  ∈⇒∣product   ↦  Data.Nat.ListAction.Properties.∈⇒∣product
+  product≢0    ↦  Data.Nat.ListAction.Properties.product≢0
+  ∈⇒≤product   ↦  Data.Nat.ListAction.Properties.∈⇒≤product
   ```
 
 * In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
   ```agda
-  sum-↭       ↦  Data.Nat.ListAction.sum-↭
-  product-↭   ↦  Data.Nat.ListAction.product-↭
+  sum-↭       ↦  Data.Nat.ListAction.Properties.sum-↭
+  product-↭   ↦  Data.Nat.ListAction.Properties.product-↭
   ```
 
 New modules
 -----------
 
-* `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction`.
+* `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.
 
 Additions to existing modules
 -----------------------------
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index aba8a90ef7..6e01481f3b 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -590,4 +590,3 @@ product = foldr ℕ._*_ 1
 "Warning: product was deprecated in v2.3.
 Please use Data.Nat.ListAction.product instead."
 #-}
-
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index f12da99940..bd771bc650 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -1633,12 +1633,12 @@ sum-++ (x ∷ xs) ys = begin
   (x + sum xs) + sum ys  ∎
 {-# WARNING_ON_USAGE sum-++
 "Warning: sum-++ was deprecated in v2.3.
-Please use Data.Nat.SumAndProperties.sum-++ instead."
+Please use Data.Nat.ListAction.Properties.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."
+Please use Data.Nat.ListAction.Properties.sum-++ instead."
 #-}
 
 open import Data.List.Membership.Propositional using (_∈_)
@@ -1649,7 +1649,7 @@ open import Data.Nat.Divisibility using (_∣_; m∣m*n; ∣n⇒∣m*n)
 ∈⇒∣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."
+Please use Data.Nat.ListAction.Properties.∈⇒∣product instead."
 #-}
 
 product≢0 : ∀ {ns} → All NonZero ns → NonZero (product ns)
@@ -1657,7 +1657,7 @@ 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."
+Please use Data.Nat.ListAction.Properties.product≢0 instead."
 #-}
 
 ∈⇒≤product : ∀ {n ns} → All NonZero ns → n ∈ ns → n ≤ product ns
@@ -1667,5 +1667,5 @@ Please use Data.Nat.SumAndProperties.product≢0 instead."
   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."
+Please use Data.Nat.ListAction.Properties.∈⇒≤product instead."
 #-}
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index b697367cd5..45ce52f344 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -400,7 +400,7 @@ mapMaybe-↭ f = catMaybes-↭ ∘ map⁺ f
 
 -- Version 2.3
 
-import Data.Nat.ListAction as ℕ
+import Data.Nat.ListAction.Properties as ℕ
 
 sum-↭ = ℕ.sum-↭
 {-# WARNING_ON_USAGE sum-↭
diff --git a/src/Data/Nat/ListAction.agda b/src/Data/Nat/ListAction.agda
index dd6f2da811..2d80e84a10 100644
--- a/src/Data/Nat/ListAction.agda
+++ b/src/Data/Nat/ListAction.agda
@@ -11,29 +11,8 @@
 
 module Data.Nat.ListAction 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;
-         +-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
-  using (module ≡-Reasoning)
-
-private
-  variable
-    m n : ℕ
-    ms ns : List ℕ
+open import Data.Nat.Base using (ℕ; _+_; _*_)
 
 
 ------------------------------------------------------------------------
@@ -44,47 +23,3 @@ 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
-
-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
-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)
-
-product-↭ : product Preserves _↭_ ⟶ _≡_
-product-↭ p = foldr-commMonoid ℕ-*-1.setoid ℕ-*-1.isCommutativeMonoid (↭⇒↭ₛ p)
-  where module ℕ-*-1 = CommutativeMonoid *-1-commutativeMonoid
diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda
index 6965c35430..06737e6684 100644
--- a/src/Data/Nat/Primality.agda
+++ b/src/Data/Nat/Primality.agda
@@ -13,8 +13,9 @@ 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.ListAction using (product)
+open import Data.Nat.ListAction.Properties using (product≢0)
 open import Data.Nat.Properties
-open import Data.Nat.ListAction 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 70c7a06abd..a875614fdd 100644
--- a/src/Data/Nat/Primality/Factorisation.agda
+++ b/src/Data/Nat/Primality/Factorisation.agda
@@ -14,10 +14,11 @@ open import Data.Nat.Divisibility
         divides)
 open import Data.Nat.Properties
 open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder)
+open import Data.Nat.ListAction using (product)
+open import Data.Nat.ListAction.Properties using (product-↭)
 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.ListAction using (product; product-↭)
 open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₁; proj₂)
 open import Data.List.Base using (List; []; _∷_; _++_)
 open import Data.List.Membership.Propositional using (_∈_)

From ed3936dca4dcf6d0250aae38155ff8a7802199e0 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 23 Jan 2025 08:22:25 +0000
Subject: [PATCH 11/12] bug: add the new module!

---
 src/Data/Nat/ListAction/Properties.agda | 82 +++++++++++++++++++++++++
 1 file changed, 82 insertions(+)
 create mode 100644 src/Data/Nat/ListAction/Properties.agda

diff --git a/src/Data/Nat/ListAction/Properties.agda b/src/Data/Nat/ListAction/Properties.agda
new file mode 100644
index 0000000000..4c1d17cf25
--- /dev/null
+++ b/src/Data/Nat/ListAction/Properties.agda
@@ -0,0 +1,82 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Natural numbers: properties of sum and product
+--
+-- Issue #2553: this is a compatibility stub module,
+-- ahead of a more thorough breaking set of changes.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Nat.ListAction.Properties where
+
+open import Algebra.Bundles using (CommutativeMonoid)
+open import Data.List.Base using (List; []; _∷_; _++_)
+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.ListAction
+open import Data.Nat.Properties
+  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
+  using (module ≡-Reasoning)
+
+private
+  variable
+    m n : ℕ
+    ms ns : List ℕ
+
+
+------------------------------------------------------------------------
+-- 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
+
+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
+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)
+
+product-↭ : product Preserves _↭_ ⟶ _≡_
+product-↭ p = foldr-commMonoid ℕ-*-1.setoid ℕ-*-1.isCommutativeMonoid (↭⇒↭ₛ p)
+  where module ℕ-*-1 = CommutativeMonoid *-1-commutativeMonoid

From f6122ce5d444c4c947e4729cf065f4616e23a242 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 5 Feb 2025 13:58:47 +0000
Subject: [PATCH 12/12] fix: pasre error

---
 src/Data/List/Base.agda | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 4b7e8c2e95..e2bb18441b 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -591,6 +591,7 @@ Please use Data.Bool.ListAction.or instead."
 {-# WARNING_ON_USAGE any
 "Warning: any was deprecated in v2.3.
 Please use Data.Bool.ListAction.any instead."
+#-}
 
 sum : List ℕ → ℕ
 sum = foldr ℕ._+_ 0