diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda
index 9cb46af85f..d53142c532 100644
--- a/src/Function/Endomorphism/Propositional.agda
+++ b/src/Function/Endomorphism/Propositional.agda
@@ -16,7 +16,7 @@ open import Algebra.Morphism; open Definitions
 
 open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Data.Nat.Properties using (+-0-monoid; +-semigroup)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 
 open import Function.Base using (id; _∘′_; _∋_)
 open import Function.Equality using (_⟨$⟩_)
diff --git a/src/Function/Nary/NonDependent.agda b/src/Function/Nary/NonDependent.agda
index 3c29079b5e..aa9c35a0f5 100644
--- a/src/Function/Nary/NonDependent.agda
+++ b/src/Function/Nary/NonDependent.agda
@@ -17,7 +17,7 @@ module Function.Nary.NonDependent where
 open import Level using (Level; 0ℓ; _⊔_; Lift)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Fin.Base using (Fin; zero; suc)
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.Product.Nary.NonDependent
 open import Function.Base using (_∘′_; _$′_; const; flip)
 open import Relation.Unary using (IUniversal)
diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda
index c8abd7db19..89aab1b58e 100644
--- a/src/Function/Properties/Bijection.agda
+++ b/src/Function/Properties/Bijection.agda
@@ -13,7 +13,7 @@ open import Level using (Level)
 open import Relation.Binary hiding (_⇔_)
 import Relation.Binary.PropositionalEquality.Properties as P
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
-open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Function.Base using (_∘_)
 open import Function.Properties.Inverse using (Inverse⇒Equivalence)
 
diff --git a/src/Function/Related.agda b/src/Function/Related.agda
index ca06dceffb..12920055af 100644
--- a/src/Function/Related.agda
+++ b/src/Function/Related.agda
@@ -20,7 +20,7 @@ open import Function.Surjection  as Surj    using (Surjection)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as P
-open import Data.Product using (_,_; proj₁; proj₂; <_,_>)
+open import Data.Product.Base using (_,_; proj₁; proj₂; <_,_>)
 
 import Function.Related.Propositional as R
 import Function.Bundles as B
diff --git a/src/Function/Related/TypeIsomorphisms/Solver.agda b/src/Function/Related/TypeIsomorphisms/Solver.agda
index 29f19c8afd..52f27d15ed 100644
--- a/src/Function/Related/TypeIsomorphisms/Solver.agda
+++ b/src/Function/Related/TypeIsomorphisms/Solver.agda
@@ -13,7 +13,7 @@ module Function.Related.TypeIsomorphisms.Solver where
 open import Algebra using (CommutativeSemiring)
 import Algebra.Solver.Ring.NaturalCoefficients.Default
 open import Data.Empty.Polymorphic using (⊥)
-open import Data.Product using (_×_)
+open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
 open import Data.Unit.Polymorphic using (⊤)
 open import Level using (Level)
diff --git a/src/Reflection/AST/Abstraction.agda b/src/Reflection/AST/Abstraction.agda
index 793c729aec..55043355d7 100644
--- a/src/Reflection/AST/Abstraction.agda
+++ b/src/Reflection/AST/Abstraction.agda
@@ -8,7 +8,7 @@
 
 module Reflection.AST.Abstraction where
 
-open import Data.Product                               using (_×_; <_,_>; uncurry)
+open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
 open import Data.String as String                      using (String)
 open import Level
 open import Relation.Nullary.Decidable                 using (Dec; map′; _×-dec_)
diff --git a/src/Reflection/AST/Argument.agda b/src/Reflection/AST/Argument.agda
index 0feb2deddd..449a45c4d8 100644
--- a/src/Reflection/AST/Argument.agda
+++ b/src/Reflection/AST/Argument.agda
@@ -9,7 +9,7 @@
 module Reflection.AST.Argument where
 
 open import Data.List.Base as List                     using (List; []; _∷_)
-open import Data.Product                               using (_×_; <_,_>; uncurry)
+open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
 open import Relation.Nullary.Decidable                 using (Dec; map′; _×-dec_)
 open import Relation.Binary                            using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda
index 7ccabb6f51..ea005eebd3 100644
--- a/src/Reflection/AST/Definition.agda
+++ b/src/Reflection/AST/Definition.agda
@@ -10,7 +10,7 @@ module Reflection.AST.Definition where
 
 import Data.List.Properties as Listₚ                   using (≡-dec)
 import Data.Nat.Properties as ℕₚ                       using (_≟_)
-open import Data.Product                               using (_×_; <_,_>; uncurry)
+open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
 open import Relation.Nullary.Decidable                 using (map′; _×-dec_; yes; no)
 open import Relation.Binary                            using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
diff --git a/src/Reflection/AST/Show.agda b/src/Reflection/AST/Show.agda
index f0291cf447..7650f6fc8e 100644
--- a/src/Reflection/AST/Show.agda
+++ b/src/Reflection/AST/Show.agda
@@ -15,7 +15,7 @@ import Data.Char as Char   using (show)
 import Data.Float as Float using (show)
 open import Data.List.Base hiding (_++_; intersperse)
 import Data.Nat.Show as ℕ using (show)
-open import Data.Product   using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.String as String
   using (String; _++_; intersperse; braces; parens; parensIfSpace; _<+>_)
 import Data.Word as Word   using (toℕ)
diff --git a/src/Reflection/AST/Term.agda b/src/Reflection/AST/Term.agda
index cfa7e70cb1..c850900464 100644
--- a/src/Reflection/AST/Term.agda
+++ b/src/Reflection/AST/Term.agda
@@ -10,8 +10,8 @@ module Reflection.AST.Term where
 
 open import Data.List.Base as List  hiding (_++_)
 open import Data.List.Properties    using (∷-dec)
-open import Data.Nat as ℕ          using (ℕ; zero; suc)
-open import Data.Product            using (_×_; _,_; <_,_>; uncurry; map₁)
+open import Data.Nat as ℕ           using (ℕ; zero; suc)
+open import Data.Product.Base       using (_×_; _,_; <_,_>; uncurry; map₁)
 open import Data.Product.Properties using (,-injective)
 open import Data.Maybe.Base         using (Maybe; just; nothing)
 open import Data.String as String   using (String)
diff --git a/src/Reflection/AST/Traversal.agda b/src/Reflection/AST/Traversal.agda
index c311567c7f..5437c52b73 100644
--- a/src/Reflection/AST/Traversal.agda
+++ b/src/Reflection/AST/Traversal.agda
@@ -13,7 +13,7 @@ module Reflection.AST.Traversal
 
 open import Data.Nat          using (ℕ; zero; suc; _+_)
 open import Data.List.Base    using (List; []; _∷_; _++_; reverse; length)
-open import Data.Product      using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.String       using (String)
 open import Function.Base     using (_∘_)
 open import Reflection        hiding (pure)
diff --git a/src/Reflection/AST/Universe.agda b/src/Reflection/AST/Universe.agda
index 334458ce2d..dac0af71ed 100644
--- a/src/Reflection/AST/Universe.agda
+++ b/src/Reflection/AST/Universe.agda
@@ -10,7 +10,7 @@ module Reflection.AST.Universe where
 
 open import Data.List.Base             using (List)
 open import Data.String.Base           using (String)
-open import Data.Product               using (_×_)
+open import Data.Product.Base          using (_×_)
 open import Reflection.AST.Argument    using (Arg)
 open import Reflection.AST.Abstraction using (Abs)
 open import Reflection.AST.Term        using (Term; Pattern; Sort; Clause)
diff --git a/src/Reflection/AnnotatedAST.agda b/src/Reflection/AnnotatedAST.agda
index 8ebc54b919..9b281bd4bd 100644
--- a/src/Reflection/AnnotatedAST.agda
+++ b/src/Reflection/AnnotatedAST.agda
@@ -17,7 +17,7 @@ open import Effect.Applicative           using (RawApplicative)
 open import Data.Bool.Base               using (Bool; false; true; if_then_else_)
 open import Data.List.Base               using (List; []; _∷_)
 open import Data.List.Relation.Unary.All using (All; _∷_; [])
-open import Data.Product                 using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Base            using (_×_; _,_; proj₁; proj₂)
 open import Data.String.Base             using (String)
 
 open import Reflection                   hiding (pure)
diff --git a/src/Reflection/AnnotatedAST/Free.agda b/src/Reflection/AnnotatedAST/Free.agda
index 79ae7a96be..2017e2fd9f 100644
--- a/src/Reflection/AnnotatedAST/Free.agda
+++ b/src/Reflection/AnnotatedAST/Free.agda
@@ -12,7 +12,7 @@ open import Data.Bool.Base               using (if_then_else_)
 open import Data.Nat.Base                using (ℕ; _∸_; compare; _<ᵇ_; less; equal; greater)
 open import Data.List.Base               using (List; []; _∷_; [_]; concatMap; length)
 open import Data.List.Relation.Unary.All using (_∷_)
-open import Data.Product                 using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Base            using (_×_; _,_; proj₁; proj₂)
 open import Data.String.Base             using (String)
 
 open import Reflection
diff --git a/src/Reflection/External.agda b/src/Reflection/External.agda
index e7e9ae989d..5a132d9362 100644
--- a/src/Reflection/External.agda
+++ b/src/Reflection/External.agda
@@ -12,7 +12,7 @@ import Agda.Builtin.Reflection.External as Builtin
 
 open import Data.Nat.Base using (ℕ; suc; zero; NonZero)
 open import Data.List.Base using (List; _∷_; [])
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.String.Base as String using (String; _++_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Unit.Base using (⊤; tt)
diff --git a/src/Relation/Binary/Construct/Subst/Equality.agda b/src/Relation/Binary/Construct/Subst/Equality.agda
index 4e0a3d0100..24e465f9f0 100644
--- a/src/Relation/Binary/Construct/Subst/Equality.agda
+++ b/src/Relation/Binary/Construct/Subst/Equality.agda
@@ -9,7 +9,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.Product as Prod
+open import Data.Product.Base as Prod
 open import Relation.Binary
 
 module Relation.Binary.Construct.Subst.Equality
diff --git a/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda b/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda
index 1f218cfc01..4bbd118c13 100644
--- a/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda
+++ b/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda
@@ -11,7 +11,7 @@
 
 module Relation.Binary.Indexed.Homogeneous.Bundles where
 
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_⟨_⟩_)
 open import Level using (Level; _⊔_; suc)
 open import Relation.Binary.Core using (_⇒_; Rel)
diff --git a/src/Relation/Binary/Indexed/Homogeneous/Core.agda b/src/Relation/Binary/Indexed/Homogeneous/Core.agda
index 7281652597..50f8b3a200 100644
--- a/src/Relation/Binary/Indexed/Homogeneous/Core.agda
+++ b/src/Relation/Binary/Indexed/Homogeneous/Core.agda
@@ -12,7 +12,7 @@
 module Relation.Binary.Indexed.Homogeneous.Core where
 
 open import Level using (Level; _⊔_)
-open import Data.Product using (_×_)
+open import Data.Product.Base using (_×_)
 open import Relation.Binary.Core as B using (REL; Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 import Relation.Binary.Indexed.Heterogeneous as I
diff --git a/src/Relation/Binary/Indexed/Homogeneous/Definitions.agda b/src/Relation/Binary/Indexed/Homogeneous/Definitions.agda
index 0231def44f..6160c7e014 100644
--- a/src/Relation/Binary/Indexed/Homogeneous/Definitions.agda
+++ b/src/Relation/Binary/Indexed/Homogeneous/Definitions.agda
@@ -11,7 +11,7 @@
 
 module Relation.Binary.Indexed.Homogeneous.Definitions where
 
-open import Data.Product using (_×_)
+open import Data.Product.Base using (_×_)
 open import Level using (Level)
 import Relation.Binary as B
 open import Relation.Unary.Indexed using (IPred)
diff --git a/src/Relation/Binary/Indexed/Homogeneous/Structures.agda b/src/Relation/Binary/Indexed/Homogeneous/Structures.agda
index 0ccad66a6f..77438dafdd 100644
--- a/src/Relation/Binary/Indexed/Homogeneous/Structures.agda
+++ b/src/Relation/Binary/Indexed/Homogeneous/Structures.agda
@@ -17,7 +17,7 @@ module Relation.Binary.Indexed.Homogeneous.Structures
   (_≈ᵢ_ : IRel A ℓ) -- The underlying indexed equality relation
   where
 
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_⟨_⟩_)
 open import Level using (Level; _⊔_; suc)
 open import Relation.Binary.Core using (_⇒_)
diff --git a/src/Relation/Binary/Lattice/Properties/BoundedLattice.agda b/src/Relation/Binary/Lattice/Properties/BoundedLattice.agda
index 1f3477b19d..b665166517 100644
--- a/src/Relation/Binary/Lattice/Properties/BoundedLattice.agda
+++ b/src/Relation/Binary/Lattice/Properties/BoundedLattice.agda
@@ -14,7 +14,7 @@ module Relation.Binary.Lattice.Properties.BoundedLattice
 open BoundedLattice L
 
 open import Algebra.Definitions _≈_
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Lattice.Properties.MeetSemilattice meetSemilattice
 open import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice
diff --git a/src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda b/src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda
index 8ee0462d39..e3bd0170eb 100644
--- a/src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda
+++ b/src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda
@@ -14,7 +14,7 @@ module Relation.Binary.Lattice.Properties.DistributiveLattice
 open DistributiveLattice L hiding (refl)
 
 open import Algebra.Definitions _≈_
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Relation.Binary
 open import Relation.Binary.Reasoning.Setoid setoid
 open import Relation.Binary.Lattice.Properties.Lattice lattice
diff --git a/src/Relation/Binary/Lattice/Properties/Lattice.agda b/src/Relation/Binary/Lattice/Properties/Lattice.agda
index a221c35b2e..633832a26c 100644
--- a/src/Relation/Binary/Lattice/Properties/Lattice.agda
+++ b/src/Relation/Binary/Lattice/Properties/Lattice.agda
@@ -16,7 +16,7 @@ open Lattice L
 import Algebra.Lattice as Alg
 import Algebra.Structures as Alg
 open import Algebra.Definitions _≈_
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (flip)
 open import Relation.Binary
 open import Relation.Binary.Properties.Poset poset
diff --git a/src/Relation/Binary/Morphism/Construct/Identity.agda b/src/Relation/Binary/Morphism/Construct/Identity.agda
index c8ed9c6b03..db12c9793b 100644
--- a/src/Relation/Binary/Morphism/Construct/Identity.agda
+++ b/src/Relation/Binary/Morphism/Construct/Identity.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
 open import Level using (Level)
 open import Relation.Binary
diff --git a/src/Relation/Binary/Morphism/OrderMonomorphism.agda b/src/Relation/Binary/Morphism/OrderMonomorphism.agda
index dd2e0ef821..3d788184c2 100644
--- a/src/Relation/Binary/Morphism/OrderMonomorphism.agda
+++ b/src/Relation/Binary/Morphism/OrderMonomorphism.agda
@@ -11,7 +11,7 @@
 
 open import Algebra.Morphism.Definitions
 open import Function.Base
-open import Data.Product using (_,_; map)
+open import Data.Product.Base using (_,_; map)
 open import Relation.Binary
 open import Relation.Binary.Morphism
 import Relation.Binary.Morphism.RelMonomorphism as RawRelation
diff --git a/src/Relation/Binary/Properties/HeytingAlgebra.agda b/src/Relation/Binary/Properties/HeytingAlgebra.agda
index f823a5b519..8786792e78 100644
--- a/src/Relation/Binary/Properties/HeytingAlgebra.agda
+++ b/src/Relation/Binary/Properties/HeytingAlgebra.agda
@@ -15,7 +15,7 @@ open HeytingAlgebra L
 
 open import Algebra.Core
 open import Algebra.Definitions _≈_
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_$_; flip; _∘_)
 open import Level using (_⊔_)
 open import Relation.Binary
diff --git a/src/Relation/Nary.agda b/src/Relation/Nary.agda
index da804883f5..36d1db0568 100644
--- a/src/Relation/Nary.agda
+++ b/src/Relation/Nary.agda
@@ -19,7 +19,7 @@ open import Data.Unit.Base
 open import Data.Bool.Base using (true; false)
 open import Data.Empty
 open import Data.Nat.Base using (zero; suc)
-open import Data.Product as Prod using (_×_; _,_)
+open import Data.Product.Base as Prod using (_×_; _,_)
 open import Data.Product.Nary.NonDependent
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_$_; _∘′_)
diff --git a/src/Relation/Nullary/Universe.agda b/src/Relation/Nullary/Universe.agda
index 5df3c1c423..658f8c7bf7 100644
--- a/src/Relation/Nullary/Universe.agda
+++ b/src/Relation/Nullary/Universe.agda
@@ -19,7 +19,7 @@ import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
   as Trivial
 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.Base as Prod hiding (map)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Function.Base using (_∘_; id)
 import Function.Equality as FunS
diff --git a/src/Relation/Unary/Algebra.agda b/src/Relation/Unary/Algebra.agda
index 600bab6c1f..514470de38 100644
--- a/src/Relation/Unary/Algebra.agda
+++ b/src/Relation/Unary/Algebra.agda
@@ -14,7 +14,7 @@ open import Algebra.Lattice.Bundles
 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.Product.Base as Product using (_,_; proj₁; proj₂; <_,_>; curry; uncurry)
 open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
 open import Data.Unit.Polymorphic using (tt)
 open import Function.Base using (id; const; _∘_)
diff --git a/src/System/Environment.agda b/src/System/Environment.agda
index 228bf699ac..ec6833f64c 100644
--- a/src/System/Environment.agda
+++ b/src/System/Environment.agda
@@ -11,7 +11,7 @@ module System.Environment where
 open import IO using (IO; lift; run; ignore)
 open import Data.List.Base using (List)
 open import Data.Maybe.Base using (Maybe)
-open import Data.Product using (_×_)
+open import Data.Product.Base using (_×_)
 open import Data.String.Base using (String)
 open import Data.Unit.Polymorphic using (⊤)
 open import Foreign.Haskell.Coerce
diff --git a/src/System/FilePath/Posix.agda b/src/System/FilePath/Posix.agda
index d486f1d342..f12cf8180e 100644
--- a/src/System/FilePath/Posix.agda
+++ b/src/System/FilePath/Posix.agda
@@ -13,7 +13,7 @@ open import Agda.Builtin.List using (List)
 open import Agda.Builtin.String using (String)
 open import IO.Base using (IO; lift)
 open import Data.Maybe.Base using (Maybe)
-open import Data.Product using (_×_)
+open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
 
 open import Foreign.Haskell.Coerce
diff --git a/src/System/Process.agda b/src/System/Process.agda
index 1473788365..4aff9ca4dd 100644
--- a/src/System/Process.agda
+++ b/src/System/Process.agda
@@ -10,7 +10,7 @@ module System.Process where
 
 open import Level using (Level)
 open import Data.List.Base using (List)
-open import Data.Product using (_×_; proj₁)
+open import Data.Product.Base using (_×_; proj₁)
 open import Data.String.Base using (String)
 open import Data.Unit.Polymorphic using (⊤)
 open import Foreign.Haskell.Coerce
diff --git a/src/Tactic/MonoidSolver.agda b/src/Tactic/MonoidSolver.agda
index 991ff41556..1448e41fe3 100644
--- a/src/Tactic/MonoidSolver.agda
+++ b/src/Tactic/MonoidSolver.agda
@@ -79,7 +79,7 @@ open import Data.Bool         as Bool    using (Bool; _∨_; if_then_else_)
 open import Data.Maybe        as Maybe   using (Maybe; just; nothing; maybe)
 open import Data.List.Base    as List    using (List; _∷_; [])
 open import Data.Nat          as ℕ       using (ℕ; suc; zero)
-open import Data.Product      as Product using (_×_; _,_)
+open import Data.Product.Base as Product using (_×_; _,_)
 
 open import Reflection.AST
 open import Reflection.AST.Term
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
index 1f6de95f4f..3ea01b2c17 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
@@ -15,7 +15,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Addition
 
 open import Data.Nat            as ℕ  using (ℕ; suc; zero; compare; _≤′_; ≤′-step; ≤′-refl)
 open import Data.Nat.Properties as ℕₚ using (≤′-trans)
-open import Data.Product              using (_,_; _×_; proj₂)
+open import Data.Product.Base         using (_,_; _×_; proj₂)
 open import Data.List.Base            using (_∷_; [])
 open import Data.List.Kleene
 open import Data.Vec                  using (Vec)
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda
index 9435251957..eeacadb154 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda
@@ -16,7 +16,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Exponentiation
 open import Function.Base using (_⟨_⟩_)
 
 open import Data.Nat.Base as ℕ using (ℕ; suc; zero; compare)
-open import Data.Product  using (_,_; _×_; proj₁; proj₂)
+open import Data.Product.Base  using (_,_; _×_; proj₁; proj₂)
 open import Data.List.Kleene
 open import Data.Vec      using (Vec)
 
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda
index 3e1ce2bfe3..90183bc4c9 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda
@@ -21,7 +21,7 @@ open import Data.Fin                                        using (Fin; zero; su
 open import Data.List.Base                                  using (_∷_; [])
 open import Data.Unit using (tt)
 open import Data.List.Kleene
-open import Data.Product                                    using (_,_; proj₁; proj₂; map₁; _×_)
+open import Data.Product.Base                               using (_,_; proj₁; proj₂; map₁; _×_)
 open import Data.Maybe                                      using (nothing; just)
 open import Function.Base                                   using (_⟨_⟩_)
 open import Level                                           using (lift)
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda
index 2baeac0f23..c7ad6d6145 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda
@@ -16,7 +16,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Multiplication
 open import Data.Nat.Base as ℕ     using (ℕ; suc; zero; _<′_; _≤′_; ≤′-step; ≤′-refl)
 open import Data.Nat.Properties    using (≤′-trans)
 open import Data.Nat.Induction
-open import Data.Product           using (_×_; _,_; proj₁; proj₂; map₁)
+open import Data.Product.Base      using (_×_; _,_; proj₁; proj₂; map₁)
 open import Data.List.Kleene
 open import Data.Vec               using (Vec)
 open import Function.Base using (_⟨_⟩_; flip)
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
index dd84eafef2..59b99cf71b 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
@@ -13,7 +13,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Negation
   (homo : Homomorphism r₁ r₂ r₃ r₄)
   where
 
-open import Data.Product          using (_,_)
+open import Data.Product.Base     using (_,_)
 open import Data.Vec              using (Vec)
 open import Data.Nat              using (_<′_)
 open import Data.Nat.Induction
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Variables.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Variables.agda
index c3884e9e2a..9fcaca2f66 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Variables.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Variables.agda
@@ -13,7 +13,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Variables
   (homo : Homomorphism r₁ r₂ r₃ r₄)
   where
 
-open import Data.Product         using (_,_)
+open import Data.Product.Base    using (_,_)
 open import Data.Vec.Base as Vec using (Vec)
 open import Data.Fin             using (Fin)
 open import Data.List.Kleene
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda b/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda
index 8cde662620..26e19d428a 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda
@@ -16,7 +16,7 @@ module Tactic.RingSolver.Core.Polynomial.Semantics
 open import Data.Nat          using (ℕ; suc; zero; _≤′_; ≤′-step; ≤′-refl)
 open import Data.Vec          using (Vec; []; _∷_; uncons)
 open import Data.List.Base    using ([]; _∷_)
-open import Data.Product      using (_,_; _×_)
+open import Data.Product.Base using (_,_; _×_)
 open import Data.List.Kleene  using (_+; _*; ∹_; _&_; [])
 
 open Homomorphism homo hiding (_^_)
diff --git a/src/Test/Golden.agda b/src/Test/Golden.agda
index efbfc59ada..079e25720a 100644
--- a/src/Test/Golden.agda
+++ b/src/Test/Golden.agda
@@ -89,7 +89,7 @@ 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 (ℕ; _≡ᵇ_; _<ᵇ_; _+_; _∸_)
 import Data.Nat.Show as ℕ using (show)
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.String as String using (String; lines; unlines; unwords; concat; _≟_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Unit.Base using (⊤)
diff --git a/src/Text/Regex/Properties/Core.agda b/src/Text/Regex/Properties/Core.agda
index e1916fb5cf..51097a7656 100644
--- a/src/Text/Regex/Properties/Core.agda
+++ b/src/Text/Regex/Properties/Core.agda
@@ -17,7 +17,7 @@ open import Data.List.Base as List using (List; []; _∷_; _++_)
 
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 
 open import Relation.Nullary using (¬_; Dec; yes; no)
diff --git a/src/Text/Tabular/List.agda b/src/Text/Tabular/List.agda
index dd06ea809a..70fc09f3d5 100644
--- a/src/Text/Tabular/List.agda
+++ b/src/Text/Tabular/List.agda
@@ -11,7 +11,7 @@ module Text.Tabular.List where
 open import Data.String using (String)
 open import Data.List.Base
 import Data.Nat.Properties as ℕₚ
-open import Data.Product using (-,_; proj₂)
+open import Data.Product.Base using (-,_; proj₂)
 open import Data.Vec.Base as Vec using (Vec)
 open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤)
 open import Function.Base
diff --git a/src/Text/Tabular/Vec.agda b/src/Text/Tabular/Vec.agda
index 74f899905c..1286ab1e14 100644
--- a/src/Text/Tabular/Vec.agda
+++ b/src/Text/Tabular/Vec.agda
@@ -9,7 +9,7 @@
 module Text.Tabular.Vec where
 
 open import Data.List.Base using (List)
-open import Data.Product as Prod using (uncurry)
+open import Data.Product.Base as Prod using (uncurry)
 open import Data.String using (String; rectangle; fromAlignment)
 open import Data.Vec.Base
 open import Function.Base