diff --git a/README/Data/Container/FreeMonad.agda b/README/Data/Container/FreeMonad.agda
index 7c4460609e..54f0935937 100644
--- a/README/Data/Container/FreeMonad.agda
+++ b/README/Data/Container/FreeMonad.agda
@@ -16,7 +16,7 @@ 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.Product renaming (_×_ to _⟨×⟩_)
+open import Data.Product.Base renaming (_×_ to _⟨×⟩_)
 open import Data.Container using (Container; _▷_)
 open import Data.Container.Combinator
 open import Data.Container.FreeMonad as FreeMonad
diff --git a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
index 7ac5b3e58a..1f04cc2dd0 100644
--- a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
+++ b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
@@ -11,7 +11,7 @@ open import Algebra.Apartness.Bundles using (HeytingCommutativeRing)
 module Algebra.Apartness.Properties.HeytingCommutativeRing
   {c ℓ₁ ℓ₂} (HCR : HeytingCommutativeRing c ℓ₁ ℓ₂) where
 
-open import Data.Product using (_,_; proj₂)
+open import Data.Product.Base using (_,_; proj₂)
 open import Algebra using (CommutativeRing; RightIdentity)
 
 open HeytingCommutativeRing HCR
diff --git a/src/Algebra/Construct/Add/Identity.agda b/src/Algebra/Construct/Add/Identity.agda
index 750c69523e..dc82a1c67b 100644
--- a/src/Algebra/Construct/Add/Identity.agda
+++ b/src/Algebra/Construct/Add/Identity.agda
@@ -14,7 +14,7 @@ open import Algebra.Core using (Op₂)
 open import Algebra.Definitions
 open import Algebra.Structures
 open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions
diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda
index 74ae5730bc..cc84ad59c9 100644
--- a/src/Algebra/Construct/Flip/Op.agda
+++ b/src/Algebra/Construct/Flip/Op.agda
@@ -10,7 +10,7 @@
 module Algebra.Construct.Flip.Op where
 
 open import Algebra
-import Data.Product as Prod
+import Data.Product.Base as Prod
 import Data.Sum as Sum
 open import Function.Base using (flip)
 open import Level using (Level)
diff --git a/src/Algebra/Construct/LexProduct/Inner.agda b/src/Algebra/Construct/LexProduct/Inner.agda
index 718bde2610..d235c1b8fd 100644
--- a/src/Algebra/Construct/LexProduct/Inner.agda
+++ b/src/Algebra/Construct/LexProduct/Inner.agda
@@ -8,7 +8,7 @@
 
 open import Algebra
 open import Data.Bool.Base using (false; true)
-open import Data.Product using (_×_; _,_; swap; map; uncurry′)
+open import Data.Product.Base using (_×_; _,_; swap; map; uncurry′)
 open import Function.Base using (_∘_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Definitions using (Decidable)
diff --git a/src/Algebra/Construct/LiftedChoice.agda b/src/Algebra/Construct/LiftedChoice.agda
index 357d2e725a..83cf2110c3 100644
--- a/src/Algebra/Construct/LiftedChoice.agda
+++ b/src/Algebra/Construct/LiftedChoice.agda
@@ -14,7 +14,7 @@ open import Algebra.Consequences.Base
 open import Relation.Binary
 open import Relation.Nullary using (¬_; yes; no)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Unary using (Pred)
diff --git a/src/Algebra/Construct/NaturalChoice/Min.agda b/src/Algebra/Construct/NaturalChoice/Min.agda
index 89bd2eefb8..100dac2193 100644
--- a/src/Algebra/Construct/NaturalChoice/Min.agda
+++ b/src/Algebra/Construct/NaturalChoice/Min.agda
@@ -10,7 +10,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.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
 open import Relation.Binary
 import Algebra.Construct.NaturalChoice.MinOp as MinOp
diff --git a/src/Algebra/Construct/Subst/Equality.agda b/src/Algebra/Construct/Subst/Equality.agda
index 697a29cd73..636b1d8004 100644
--- a/src/Algebra/Construct/Subst/Equality.agda
+++ b/src/Algebra/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.Core
 
 module Algebra.Construct.Subst.Equality
diff --git a/src/Algebra/Lattice/Morphism/Construct/Identity.agda b/src/Algebra/Lattice/Morphism/Construct/Identity.agda
index 9b5993696f..8531643540 100644
--- a/src/Algebra/Lattice/Morphism/Construct/Identity.agda
+++ b/src/Algebra/Lattice/Morphism/Construct/Identity.agda
@@ -11,7 +11,7 @@ module Algebra.Lattice.Morphism.Construct.Identity where
 open import Algebra.Lattice.Bundles
 open import Algebra.Lattice.Morphism.Structures
   using ( module LatticeMorphisms )
-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.Morphism.Construct.Identity using (isRelHomomorphism)
diff --git a/src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda b/src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda
index bfed8d01ec..c2c8301409 100644
--- a/src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda
+++ b/src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda
@@ -15,7 +15,7 @@ open import Algebra.Lattice.Morphism.Structures
 import Algebra.Consequences.Setoid as Consequences
 import Algebra.Morphism.MagmaMonomorphism as MagmaMonomorphisms
 import Algebra.Lattice.Properties.Lattice as LatticeProperties
-open import Data.Product using (_,_; map)
+open import Data.Product.Base using (_,_; map)
 open import Relation.Binary
 import Relation.Binary.Morphism.RelMonomorphism as RelMonomorphisms
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
diff --git a/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda b/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda
index 587a5dcc2c..9cdad57edc 100644
--- a/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda
+++ b/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda
@@ -18,7 +18,7 @@ open import Effect.Applicative as Applicative
 open import Effect.Monad
 open import Data.Fin.Base using (Fin)
 open import Data.Nat.Base
-open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Data.Vec.Base as Vec using (Vec)
 import Data.Vec.Effectful as VecCat
 import Function.Identity.Effectful as IdCat
diff --git a/src/Algebra/Lattice/Structures/Biased.agda b/src/Algebra/Lattice/Structures/Biased.agda
index 66a93df06d..fefe3bef67 100644
--- a/src/Algebra/Lattice/Structures/Biased.agda
+++ b/src/Algebra/Lattice/Structures/Biased.agda
@@ -14,7 +14,7 @@
 
 open import Algebra.Core
 open import Algebra.Consequences.Setoid
-open import Data.Product using (proj₁; proj₂)
+open import Data.Product.Base using (proj₁; proj₂)
 open import Level using (_⊔_)
 open import Relation.Binary using (Rel; Setoid; IsEquivalence)
 
diff --git a/src/Algebra/Module/Morphism/Construct/Identity.agda b/src/Algebra/Module/Morphism/Construct/Identity.agda
index f5e5d73b05..90f6940a16 100644
--- a/src/Algebra/Module/Morphism/Construct/Identity.agda
+++ b/src/Algebra/Module/Morphism/Construct/Identity.agda
@@ -21,7 +21,7 @@ open import Algebra.Module.Morphism.Structures
         ; module ModuleMorphisms
         )
 open import Algebra.Morphism.Construct.Identity
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
 open import Level using (Level)
 
diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda
index 20269f13a6..4a0e40c17c 100644
--- a/src/Algebra/Module/Structures.agda
+++ b/src/Algebra/Module/Structures.agda
@@ -16,7 +16,7 @@ open import Algebra.Module.Core
 import Algebra.Definitions as Defs
 open import Algebra.Module.Definitions
 open import Algebra.Structures
-open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Level using (Level; _⊔_)
 
 private
diff --git a/src/Algebra/Morphism/Consequences.agda b/src/Algebra/Morphism/Consequences.agda
index d5bc6a8076..ac7d6de2c5 100644
--- a/src/Algebra/Morphism/Consequences.agda
+++ b/src/Algebra/Morphism/Consequences.agda
@@ -10,7 +10,7 @@ module Algebra.Morphism.Consequences where
 
 open import Algebra using (Magma)
 open import Algebra.Morphism.Definitions
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (id; _∘_)
 open import Function.Definitions
 import Relation.Binary.Reasoning.Setoid as EqR
diff --git a/src/Algebra/Morphism/Construct/Identity.agda b/src/Algebra/Morphism/Construct/Identity.agda
index 5ea2571de0..5529ec3c01 100644
--- a/src/Algebra/Morphism/Construct/Identity.agda
+++ b/src/Algebra/Morphism/Construct/Identity.agda
@@ -20,7 +20,7 @@ open import Algebra.Morphism.Structures
         ; module QuasigroupMorphisms
         ; module LoopMorphisms
         )
-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.Morphism.Construct.Identity using (isRelHomomorphism)
diff --git a/src/Algebra/Morphism/MonoidMonomorphism.agda b/src/Algebra/Morphism/MonoidMonomorphism.agda
index 5f2d85d86a..4a512b2687 100644
--- a/src/Algebra/Morphism/MonoidMonomorphism.agda
+++ b/src/Algebra/Morphism/MonoidMonomorphism.agda
@@ -24,7 +24,7 @@ open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; 
 
 open import Algebra.Definitions
 open import Algebra.Structures
-open import Data.Product using (map)
+open import Data.Product.Base using (map)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 
 ------------------------------------------------------------------------
diff --git a/src/Algebra/Ordered/Structures.agda b/src/Algebra/Ordered/Structures.agda
index ab211cc497..638d8783f0 100644
--- a/src/Algebra/Ordered/Structures.agda
+++ b/src/Algebra/Ordered/Structures.agda
@@ -21,7 +21,7 @@ module Algebra.Ordered.Structures
 open import Algebra.Core
 open import Algebra.Definitions _≈_
 open import Algebra.Structures _≈_
-open import Data.Product using (proj₁; proj₂)
+open import Data.Product.Base using (proj₁; proj₂)
 open import Function.Base using (flip)
 open import Level using (_⊔_)
 open import Relation.Binary.Definitions using (Transitive; Monotonic₁; Monotonic₂)
diff --git a/src/Algebra/Properties/BooleanAlgebra.agda b/src/Algebra/Properties/BooleanAlgebra.agda
index f53815b934..2e1f148701 100644
--- a/src/Algebra/Properties/BooleanAlgebra.agda
+++ b/src/Algebra/Properties/BooleanAlgebra.agda
@@ -30,7 +30,7 @@ open import Algebra.Structures _≈_
 open import Relation.Binary
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence using (_⇔_; module Equivalence)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
diff --git a/src/Algebra/Properties/CommutativeMagma/Divisibility.agda b/src/Algebra/Properties/CommutativeMagma/Divisibility.agda
index 14ad404a37..27f6ba56a5 100644
--- a/src/Algebra/Properties/CommutativeMagma/Divisibility.agda
+++ b/src/Algebra/Properties/CommutativeMagma/Divisibility.agda
@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra using (CommutativeMagma)
-open import Data.Product using (_×_; _,_; map)
+open import Data.Product.Base using (_×_; _,_; map)
 
 module Algebra.Properties.CommutativeMagma.Divisibility
   {a ℓ} (CM : CommutativeMagma a ℓ)
diff --git a/src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda b/src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda
index c17510e530..66bec51115 100644
--- a/src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda
+++ b/src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda
@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra using (CommutativeSemigroup)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 
 module Algebra.Properties.CommutativeSemigroup.Divisibility
diff --git a/src/Algebra/Properties/Lattice.agda b/src/Algebra/Properties/Lattice.agda
index 3e9e078f3f..ed5bfd00dc 100644
--- a/src/Algebra/Properties/Lattice.agda
+++ b/src/Algebra/Properties/Lattice.agda
@@ -11,7 +11,7 @@ open import Algebra.Lattice.Bundles
 open import Relation.Binary
 open import Function.Base
 open import Function.Bundles using (module Equivalence; _⇔_)
-open import Data.Product using (_,_; swap)
+open import Data.Product.Base using (_,_; swap)
 
 module Algebra.Properties.Lattice {l₁ l₂} (L : Lattice l₁ l₂) where
 
diff --git a/src/Algebra/Properties/Monoid/Divisibility.agda b/src/Algebra/Properties/Monoid/Divisibility.agda
index 5653312fd8..f2c8c1f20f 100644
--- a/src/Algebra/Properties/Monoid/Divisibility.agda
+++ b/src/Algebra/Properties/Monoid/Divisibility.agda
@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra using (Monoid)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Relation.Binary
 
 module Algebra.Properties.Monoid.Divisibility
diff --git a/src/Algebra/Properties/Semigroup/Divisibility.agda b/src/Algebra/Properties/Semigroup/Divisibility.agda
index d7a6154a32..76eaaa6edf 100644
--- a/src/Algebra/Properties/Semigroup/Divisibility.agda
+++ b/src/Algebra/Properties/Semigroup/Divisibility.agda
@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra using (Semigroup)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Relation.Binary.Definitions using (Transitive)
 
 module Algebra.Properties.Semigroup.Divisibility
diff --git a/src/Algebra/Properties/Semiring/Divisibility.agda b/src/Algebra/Properties/Semiring/Divisibility.agda
index a1b2ff2e9b..54a352d782 100644
--- a/src/Algebra/Properties/Semiring/Divisibility.agda
+++ b/src/Algebra/Properties/Semiring/Divisibility.agda
@@ -8,7 +8,7 @@
 
 open import Algebra using (Semiring)
 import Algebra.Properties.Monoid.Divisibility as MonoidDivisibility
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 
 module Algebra.Properties.Semiring.Divisibility
diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda
index 69d1a67b0b..623beaeebd 100644
--- a/src/Algebra/Solver/CommutativeMonoid.agda
+++ b/src/Algebra/Solver/CommutativeMonoid.agda
@@ -17,7 +17,7 @@ open import Data.Maybe.Base as Maybe
   using (Maybe; decToMaybe; From-just; from-just)
 open import Data.Nat as ℕ using (ℕ; zero; suc; _+_)
 open import Data.Nat.GeneralisedArithmetic using (fold)
-open import Data.Product using (_×_; uncurry)
+open import Data.Product.Base using (_×_; uncurry)
 open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate)
 
 open import Function.Base using (_∘_)
diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
index a0704ba95b..fdba81a838 100644
--- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
+++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
@@ -15,7 +15,7 @@ open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Maybe.Base as Maybe
   using (Maybe; decToMaybe; From-just; from-just)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_)
-open import Data.Product using (_×_; uncurry)
+open import Data.Product.Base using (_×_; uncurry)
 open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate)
 
 open import Function.Base using (_∘_)
diff --git a/src/Algebra/Solver/Ring/NaturalCoefficients.agda b/src/Algebra/Solver/Ring/NaturalCoefficients.agda
index 495e8cfa66..95af2b0a33 100644
--- a/src/Algebra/Solver/Ring/NaturalCoefficients.agda
+++ b/src/Algebra/Solver/Ring/NaturalCoefficients.agda
@@ -12,7 +12,7 @@ import Algebra.Properties.Semiring.Mult as SemiringMultiplication
 open import Data.Maybe.Base using (Maybe; just; nothing; map)
 open import Algebra.Solver.Ring.AlmostCommutativeRing
 open import Data.Nat.Base as ℕ
-open import Data.Product using (module Σ)
+open import Data.Product.Base using (module Σ)
 open import Function.Base using (id)
 open import Relation.Binary.PropositionalEquality using (_≡_)