diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4940047ba8..a0dba2be8d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -57,6 +57,22 @@ Deprecated names
   or        ↦  Data.Bool.ListAction.or
   any       ↦  Data.Bool.ListAction.any
   all       ↦  Data.Bool.ListAction.all
+  sum       ↦  Data.Nat.ListAction.sum
+  product   ↦  Data.Nat.ListAction.product
+  ```
+
+* In `Data.List.Properties`:
+  ```agda
+  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.Properties.sum-↭
+  product-↭   ↦  Data.Nat.ListAction.Properties.product-↭
   ```
 
 New modules
@@ -64,6 +80,8 @@ New modules
 
 * `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.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/doc/README/Data/List.agda b/doc/README/Data/List.agda
index 2c284daa78..e47eb9ea1f 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.ListAction 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/Base.agda b/src/Data/List/Base.agda
index 62a68a02ed..e2bb18441b 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; _+_; _*_)
+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)
@@ -150,12 +150,6 @@ null : List A → Bool
 null []       = true
 null (x ∷ xs) = false
 
-sum : List ℕ → ℕ
-sum = foldr _+_ 0
-
-product : List ℕ → ℕ
-product = foldr _*_ 1
-
 length : List A → ℕ
 length = foldr (const suc) 0
 
@@ -598,3 +592,17 @@ Please use Data.Bool.ListAction.or instead."
 "Warning: any was deprecated in v2.3.
 Please use Data.Bool.ListAction.any instead."
 #-}
+
+sum : List ℕ → ℕ
+sum = foldr ℕ._+_ 0
+{-# WARNING_ON_USAGE sum
+"Warning: sum was deprecated in v2.3.
+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.ListAction.product instead."
+#-}
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index c6d9faea11..bd771bc650 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
 
@@ -1534,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.
@@ -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.ListAction.Properties.sum-++ instead."
+#-}
+sum-++-commute = sum-++
+{-# WARNING_ON_USAGE sum-++-commute
+"Warning: sum-++-commute was deprecated in v2.0.
+Please use Data.Nat.ListAction.Properties.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.ListAction.Properties.∈⇒∣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.ListAction.Properties.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.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 d31071834f..45ce52f344 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,25 @@ 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
+
+import Data.Nat.ListAction.Properties as ℕ
+
+sum-↭ = ℕ.sum-↭
+{-# WARNING_ON_USAGE sum-↭
+"Warning: sum-↭ was deprecated in v2.3.
+Please use Data.Nat.ListAction.sum-↭ instead."
+#-}
+product-↭ = ℕ.product-↭
+{-# WARNING_ON_USAGE product-↭
+"Warning: product-↭ was deprecated in v2.3.
+Please use Data.Nat.ListAction.product-↭ instead."
+#-}
diff --git a/src/Data/Nat/ListAction.agda b/src/Data/Nat/ListAction.agda
new file mode 100644
index 0000000000..2d80e84a10
--- /dev/null
+++ b/src/Data/Nat/ListAction.agda
@@ -0,0 +1,25 @@
+------------------------------------------------------------------------
+-- 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.ListAction where
+
+open import Data.List.Base using (List; []; _∷_; _++_; foldr)
+open import Data.Nat.Base using (ℕ; _+_; _*_)
+
+
+------------------------------------------------------------------------
+-- Definitions
+
+sum : List ℕ → ℕ
+sum = foldr _+_ 0
+
+product : List ℕ → ℕ
+product = foldr _*_ 1
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
diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda
index ad7283235e..06737e6684 100644
--- a/src/Data/Nat/Primality.agda
+++ b/src/Data/Nat/Primality.agda
@@ -8,12 +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.ListAction using (product)
+open import Data.Nat.ListAction.Properties using (product≢0)
 open import Data.Nat.Properties
 open import Data.Product.Base using (∃-syntax; _×_; map₂; _,_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda
index 4a91348a66..a875614fdd 100644
--- a/src/Data/Nat/Primality/Factorisation.agda
+++ b/src/Data/Nat/Primality/Factorisation.agda
@@ -14,19 +14,21 @@ 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.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; []; _∷_)
 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 (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)
@@ -146,7 +148,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
diff --git a/src/Data/Tree/Binary/Zipper.agda b/src/Data/Tree/Binary/Zipper.agda
index 3024b125ca..75017d1195 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.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 03a88b09d2..c4307fcb1e 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.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 7e592a3ff2..ecababe7c8 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.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)
@@ -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..fd1f05ec1c 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.ListAction 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