diff --git a/README/Case.agda b/README/Case.agda
index 358460a63b..450105aff9 100644
--- a/README/Case.agda
+++ b/README/Case.agda
@@ -12,8 +12,6 @@ module README.Case where
 open import Data.Fin   hiding (pred)
 open import Data.Maybe hiding (from-just)
 open import Data.Nat   hiding (pred)
-open import Data.List
-open import Data.Sum
 open import Data.Product
 open import Function.Base using (case_of_; case_return_of_)
 open import Relation.Nullary
diff --git a/README/Data/Container/FreeMonad.agda b/README/Data/Container/FreeMonad.agda
index 54f0935937..ab302c90f5 100644
--- a/README/Data/Container/FreeMonad.agda
+++ b/README/Data/Container/FreeMonad.agda
@@ -15,7 +15,7 @@ open import Data.Empty
 open import Data.Unit
 open import Data.Bool.Base using (Bool; true)
 open import Data.Nat
-open import Data.Sum using (inj₁; inj₂)
+open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Product.Base renaming (_×_ to _⟨×⟩_)
 open import Data.Container using (Container; _▷_)
 open import Data.Container.Combinator
diff --git a/README/Design/Decidability.agda b/README/Design/Decidability.agda
index e615af282e..38bb52d489 100644
--- a/README/Design/Decidability.agda
+++ b/README/Design/Decidability.agda
@@ -9,7 +9,7 @@
 module README.Design.Decidability where
 
 open import Data.Bool
-open import Data.List
+open import Data.List.Base using (List; []; _∷_)
 open import Data.List.Properties using (∷-injective)
 open import Data.Nat
 open import Data.Nat.Properties using (suc-injective)
diff --git a/README/Design/Hierarchies.agda b/README/Design/Hierarchies.agda
index 0a91586086..f0a642e2a8 100644
--- a/README/Design/Hierarchies.agda
+++ b/README/Design/Hierarchies.agda
@@ -8,7 +8,7 @@
 
 module README.Design.Hierarchies where
 
-open import Data.Sum using (_⊎_)
+open import Data.Sum.Base using (_⊎_)
 open import Level using (Level; _⊔_; suc)
 open import Relation.Binary using (_Preserves₂_⟶_⟶_)
 
diff --git a/README/Nary.agda b/README/Nary.agda
index 826d7b74e6..da2c2fcca3 100644
--- a/README/Nary.agda
+++ b/README/Nary.agda
@@ -16,7 +16,7 @@ open import Data.Fin using (Fin; fromℕ; #_; inject₁)
 open import Data.List
 open import Data.List.Properties
 open import Data.Product using (_×_; _,_)
-open import Data.Sum using (inj₁; inj₂)
+open import Data.Sum.Base using (inj₁; inj₂)
 open import Function
 open import Relation.Nullary
 open import Relation.Binary using (module Tri); open Tri
diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda
index cc84ad59c9..4dd5849a6f 100644
--- a/src/Algebra/Construct/Flip/Op.agda
+++ b/src/Algebra/Construct/Flip/Op.agda
@@ -11,7 +11,7 @@ module Algebra.Construct.Flip.Op where
 
 open import Algebra
 import Data.Product.Base as Prod
-import Data.Sum as Sum
+import Data.Sum.Base as Sum
 open import Function.Base using (flip)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_)
diff --git a/src/Algebra/Construct/NaturalChoice/Min.agda b/src/Algebra/Construct/NaturalChoice/Min.agda
index 100dac2193..41f895afe6 100644
--- a/src/Algebra/Construct/NaturalChoice/Min.agda
+++ b/src/Algebra/Construct/NaturalChoice/Min.agda
@@ -9,7 +9,7 @@
 open import Algebra.Core
 open import Algebra.Bundles
 open import Algebra.Construct.NaturalChoice.Base
-open import Data.Sum using (inj₁; inj₂; [_,_])
+open import Data.Sum.Base using (inj₁; inj₂; [_,_])
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
 open import Relation.Binary
diff --git a/src/Algebra/Construct/Subst/Equality.agda b/src/Algebra/Construct/Subst/Equality.agda
index 636b1d8004..05d0277398 100644
--- a/src/Algebra/Construct/Subst/Equality.agda
+++ b/src/Algebra/Construct/Subst/Equality.agda
@@ -19,7 +19,7 @@ module Algebra.Construct.Subst.Equality
 
 open import Algebra.Definitions
 open import Algebra.Structures
-import Data.Sum as Sum
+import Data.Sum.Base as Sum
 open import Function.Base
 open import Relation.Binary.Construct.Subst.Equality equiv
 
diff --git a/src/Algebra/Lattice/Construct/Subst/Equality.agda b/src/Algebra/Lattice/Construct/Subst/Equality.agda
index 19b4884e8e..14a8f650cf 100644
--- a/src/Algebra/Lattice/Construct/Subst/Equality.agda
+++ b/src/Algebra/Lattice/Construct/Subst/Equality.agda
@@ -12,7 +12,6 @@
 open import Algebra.Core using (Op₂)
 open import Algebra.Definitions
 open import Algebra.Lattice.Structures
-import Data.Sum as Sum
 open import Data.Product as Prod
 open import Function.Base
 open import Relation.Binary.Core
diff --git a/src/Algebra/Module/Definitions/Left.agda b/src/Algebra/Module/Definitions/Left.agda
index 1175292fcb..e43f2ef38e 100644
--- a/src/Algebra/Module/Definitions/Left.agda
+++ b/src/Algebra/Module/Definitions/Left.agda
@@ -15,7 +15,6 @@ module Algebra.Module.Definitions.Left
   {a b ℓb} (A : Set a) {B : Set b} (_≈_ : Rel B ℓb)
   where
 
-open import Data.Sum
 open import Data.Product
 
 ------------------------------------------------------------------------
diff --git a/src/Algebra/Module/Definitions/Right.agda b/src/Algebra/Module/Definitions/Right.agda
index 9f9dc67bf7..875dcfc594 100644
--- a/src/Algebra/Module/Definitions/Right.agda
+++ b/src/Algebra/Module/Definitions/Right.agda
@@ -16,7 +16,6 @@ module Algebra.Module.Definitions.Right
   where
 
 open import Data.Product
-open import Data.Sum
 
 ------------------------------------------------------------------------
 -- Binary operations
diff --git a/src/Data/Container/Indexed/Combinator.agda b/src/Data/Container/Indexed/Combinator.agda
index bc99e83f96..43721d4689 100644
--- a/src/Data/Container/Indexed/Combinator.agda
+++ b/src/Data/Container/Indexed/Combinator.agda
@@ -13,7 +13,7 @@ open import Data.Container.Indexed
 open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
 open import Data.Unit.Polymorphic.Base using (⊤)
 open import Data.Product as Prod hiding (Σ) renaming (_×_ to _⟨×⟩_)
-open import Data.Sum renaming (_⊎_ to _⟨⊎⟩_)
+open import Data.Sum.Base renaming (_⊎_ to _⟨⊎⟩_)
 open import Data.Sum.Relation.Unary.All as All using (All)
 open import Function.Base as F hiding (id; const) renaming (_∘_ to _⟨∘⟩_)
 open import Function.Inverse using (_↔̇_; inverse)
diff --git a/src/Data/List/Relation/Unary/Enumerates/Setoid.agda b/src/Data/List/Relation/Unary/Enumerates/Setoid.agda
index cdfd9c7ed5..4ac2f914d7 100644
--- a/src/Data/List/Relation/Unary/Enumerates/Setoid.agda
+++ b/src/Data/List/Relation/Unary/Enumerates/Setoid.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.List
+open import Data.List.Base using (List)
 open import Level
 open import Relation.Binary
 
diff --git a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda
index b9eabc66b3..8185cacfe3 100644
--- a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda
@@ -11,7 +11,7 @@ open import Data.List.Membership.Setoid.Properties as Membership
 open import Data.List.Relation.Unary.Any using (index)
 open import Data.List.Relation.Unary.Any.Properties using (lookup-index)
 open import Data.List.Relation.Unary.Enumerates.Setoid
-open import Data.Sum using (inj₁; inj₂)
+open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Sum.Relation.Binary.Pointwise
   using (_⊎ₛ_; inj₁; inj₂)
 open import Data.Product using (_,_; proj₁; proj₂)
diff --git a/src/Data/List/Relation/Unary/First.agda b/src/Data/List/Relation/Unary/First.agda
index b00f35e9d3..90b8bf26cb 100644
--- a/src/Data/List/Relation/Unary/First.agda
+++ b/src/Data/List/Relation/Unary/First.agda
@@ -16,7 +16,7 @@ open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.Product as Prod using (∃; -,_; _,_)
-open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
+open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function
 open import Relation.Unary
 open import Relation.Nullary
diff --git a/src/Data/List/Relation/Unary/Grouped.agda b/src/Data/List/Relation/Unary/Grouped.agda
index 51f3f28a17..b907069142 100644
--- a/src/Data/List/Relation/Unary/Grouped.agda
+++ b/src/Data/List/Relation/Unary/Grouped.agda
@@ -10,7 +10,7 @@ module Data.List.Relation.Unary.Grouped where
 
 open import Data.List.Base using (List; []; _∷_; map)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_; all?)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Product using (_×_; _,_)
 open import Relation.Binary as B using (REL; Rel)
 open import Relation.Unary as U using (Pred)
diff --git a/src/Data/List/Relation/Unary/Grouped/Properties.agda b/src/Data/List/Relation/Unary/Grouped/Properties.agda
index a8a72e6cec..65ac3d6ed6 100644
--- a/src/Data/List/Relation/Unary/Grouped/Properties.agda
+++ b/src/Data/List/Relation/Unary/Grouped/Properties.agda
@@ -9,7 +9,7 @@
 module Data.List.Relation.Unary.Grouped.Properties where
 
 open import Data.Bool using (true; false)
-open import Data.List
+open import Data.List.Base using ([]; [_]; _∷_; map; derun)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 import Data.List.Relation.Unary.All.Properties as All
 open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_)
diff --git a/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda b/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda
index 8945b2f220..2eda2ded13 100644
--- a/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.List
+open import Data.List.Base using ([]; _∷_; deduplicate)
 import Data.List.Relation.Unary.Unique.DecSetoid as Unique
 open import Data.List.Relation.Unary.All.Properties using (all-filter)
 open import Data.List.Relation.Unary.Unique.Setoid.Properties
diff --git a/src/Data/Nat/Binary/Subtraction.agda b/src/Data/Nat/Binary/Subtraction.agda
index 8b095b137f..f1c0b64f56 100644
--- a/src/Data/Nat/Binary/Subtraction.agda
+++ b/src/Data/Nat/Binary/Subtraction.agda
@@ -17,7 +17,7 @@ open import Data.Nat.Binary.Base
 open import Data.Nat.Binary.Properties
 import Data.Nat.Properties as ℕₚ
 open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃)
-open import Data.Sum using (inj₁; inj₂)
+open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Vec using ([]; _∷_)
 open import Function.Base using (_∘_; _$_)
 open import Level using (0ℓ)
diff --git a/src/Data/Nat/Combinatorics/Specification.agda b/src/Data/Nat/Combinatorics/Specification.agda
index 533a565d23..0b263eed54 100644
--- a/src/Data/Nat/Combinatorics/Specification.agda
+++ b/src/Data/Nat/Combinatorics/Specification.agda
@@ -16,7 +16,7 @@ open import Data.Nat.DivMod
 open import Data.Nat.Divisibility
 open import Data.Nat.Properties
 open import Data.Nat.Combinatorics.Base
-open import Data.Sum using (inj₁; inj₂)
+open import Data.Sum.Base using (inj₁; inj₂)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; trans; _≢_)
 open import Relation.Nullary.Decidable using (yes; no; does)
diff --git a/src/Data/Nat/InfinitelyOften.agda b/src/Data/Nat/InfinitelyOften.agda
index 0913f3fd5c..ba4dc24f1d 100644
--- a/src/Data/Nat/InfinitelyOften.agda
+++ b/src/Data/Nat/InfinitelyOften.agda
@@ -14,7 +14,7 @@ open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Product as Prod hiding (map)
-open import Data.Sum hiding (map)
+open import Data.Sum.Base using (inj₁; inj₂; _⊎_)
 open import Function
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Negation using (¬_)
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index 8b5b195d42..41da2c1676 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -17,7 +17,7 @@ open import Data.Maybe.Properties using (just-injective)
 open import Data.Maybe.Relation.Unary.All as Maybe using (nothing; just)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product as Prod using (∃; ∃-syntax; _×_; _,_; proj₁; proj₂)
-open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
+open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function.Base as F
 open import Level using (Level)
 
diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional.agda b/src/Data/Tree/AVL/Map/Membership/Propositional.agda
index 7e5d297025..5e9498ea31 100644
--- a/src/Data/Tree/AVL/Map/Membership/Propositional.agda
+++ b/src/Data/Tree/AVL/Map/Membership/Propositional.agda
@@ -17,7 +17,7 @@ open import Data.Bool.Base using (true; false)
 open import Data.Maybe.Base using (just; nothing; is-just)
 open import Data.Product as Prod using (_×_; ∃-syntax; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent renaming (Pointwise to _×ᴿ_)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; _∘′_)
 open import Level using (Level)
 
diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
index 91df2a1c0c..c05ed27177 100644
--- a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
+++ b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
@@ -17,7 +17,7 @@ open import Data.Bool.Base using (true; false)
 open import Data.Maybe.Base using (just; nothing; is-just)
 open import Data.Product as Prod using (_×_; ∃-syntax; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent renaming (Pointwise to _×ᴿ_)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; _∘′_)
 open import Level using (Level)
 
diff --git a/src/Data/Vec/Relation/Binary/Lex/Core.agda b/src/Data/Vec/Relation/Binary/Lex/Core.agda
index 4ac943401e..e11acaf86b 100644
--- a/src/Data/Vec/Relation/Binary/Lex/Core.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/Core.agda
@@ -12,7 +12,7 @@ open import Data.Empty
 open import Data.Nat using (ℕ; suc)
 import Data.Nat.Properties as ℕ
 open import Data.Product using (_×_; _,_; proj₁; proj₂; uncurry)
-open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Vec using (Vec; []; _∷_)
 open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_)
 open import Function.Base using (flip)
diff --git a/src/Effect/Monad/Error/Transformer.agda b/src/Effect/Monad/Error/Transformer.agda
index d6d5f97626..308a20bbbd 100644
--- a/src/Effect/Monad/Error/Transformer.agda
+++ b/src/Effect/Monad/Error/Transformer.agda
@@ -41,7 +41,7 @@ record RawMonadError
 
 module Sumₗ where
 
-  open import Data.Sum using (inj₁; inj₂; [_,_]′)
+  open import Data.Sum.Base using (inj₁; inj₂; [_,_]′)
   open import Data.Sum.Effectful.Left.Transformer E a
 
   monadError : RawMonad M → RawMonadError (SumₗT M)
@@ -54,7 +54,7 @@ module Sumₗ where
 
 module Sumᵣ where
 
-  open import Data.Sum using (inj₁; inj₂; [_,_]′)
+  open import Data.Sum.Base using (inj₁; inj₂; [_,_]′)
   open import Data.Sum.Effectful.Right.Transformer a E
 
   monadError : RawMonad M → RawMonadError (SumᵣT M)
diff --git a/src/Reflection/External.agda b/src/Reflection/External.agda
index ba4e076426..e7e9ae989d 100644
--- a/src/Reflection/External.agda
+++ b/src/Reflection/External.agda
@@ -14,7 +14,7 @@ open import Data.Nat.Base using (ℕ; suc; zero; NonZero)
 open import Data.List.Base using (List; _∷_; [])
 open import Data.Product using (_×_; _,_)
 open import Data.String.Base as String using (String; _++_)
-open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Unit.Base using (⊤; tt)
 open import Function.Base using (case_of_; _$_; _∘_)
 open import Reflection hiding (name)
diff --git a/src/Relation/Nullary/Universe.agda b/src/Relation/Nullary/Universe.agda
index 4c0308343d..f566b2880a 100644
--- a/src/Relation/Nullary/Universe.agda
+++ b/src/Relation/Nullary/Universe.agda
@@ -16,7 +16,7 @@ open import Relation.Binary.PropositionalEquality as PropEq
   using (_≡_; refl)
 import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
   as Trivial
-open import Data.Sum     as Sum  hiding (map)
+open import Data.Sum.Base as Sum  hiding (map)
 open import Data.Sum.Relation.Binary.Pointwise
 open import Data.Product as Prod hiding (map)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
diff --git a/src/Relation/Unary/Algebra.agda b/src/Relation/Unary/Algebra.agda
index 2d121be0fa..600bab6c1f 100644
--- a/src/Relation/Unary/Algebra.agda
+++ b/src/Relation/Unary/Algebra.agda
@@ -15,7 +15,7 @@ import Algebra.Lattice.Structures as AlgebraicLatticeStructures
 import Algebra.Structures as AlgebraicStructures
 open import Data.Empty.Polymorphic using (⊥-elim)
 open import Data.Product as Product using (_,_; proj₁; proj₂; <_,_>; curry; uncurry)
-open import Data.Sum as Sum using (inj₁; inj₂; [_,_])
+open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
 open import Data.Unit.Polymorphic using (tt)
 open import Function.Base using (id; const; _∘_)
 open import Level