diff --git a/src/Codata/Guarded/Stream/Properties.agda b/src/Codata/Guarded/Stream/Properties.agda
index 29ea54bb1d..df68a9c4b2 100644
--- a/src/Codata/Guarded/Stream/Properties.agda
+++ b/src/Codata/Guarded/Stream/Properties.agda
@@ -16,7 +16,7 @@ open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
 open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_)
 import Data.Nat.GeneralisedArithmetic as ℕ
-open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Base as Prod using (_×_; _,_; proj₁; proj₂)
 open import Data.Vec.Base as Vec using (Vec; _∷_)
 open import Function.Base using (const; flip; id; _∘′_; _$′_; _⟨_⟩_; _∘₂′_)
 open import Level using (Level)
diff --git a/src/Codata/Guarded/Stream/Relation/Unary/All.agda b/src/Codata/Guarded/Stream/Relation/Unary/All.agda
index ad87a7e589..69171a8960 100644
--- a/src/Codata/Guarded/Stream/Relation/Unary/All.agda
+++ b/src/Codata/Guarded/Stream/Relation/Unary/All.agda
@@ -9,7 +9,7 @@
 module Codata.Guarded.Stream.Relation.Unary.All where
 
 open import Codata.Guarded.Stream using (Stream; head; tail)
-open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Level
 open import Relation.Unary
 
diff --git a/src/Codata/Musical/Covec.agda b/src/Codata/Musical/Covec.agda
index 88b15c070b..8993fd5aa8 100644
--- a/src/Codata/Musical/Covec.agda
+++ b/src/Codata/Musical/Covec.agda
@@ -14,7 +14,7 @@ open import Codata.Musical.Cofin using (Cofin; zero; suc)
 open import Codata.Musical.Colist as Colist using (Colist; []; _∷_)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Vec.Base using (Vec; []; _∷_)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_∋_)
 open import Level using (Level)
 open import Relation.Binary
diff --git a/src/Codata/Sized/Colist.agda b/src/Codata/Sized/Colist.agda
index e57a5b632e..0675721bab 100644
--- a/src/Codata/Sized/Colist.agda
+++ b/src/Codata/Sized/Colist.agda
@@ -12,7 +12,7 @@ open import Level using (Level)
 open import Size
 open import Data.Unit.Base
 open import Data.Nat.Base
-open import Data.Product using (_×_ ; _,_)
+open import Data.Product.Base using (_×_ ; _,_)
 open import Data.These.Base using (These; this; that; these)
 open import Data.Maybe.Base using (Maybe; nothing; just)
 open import Data.List.Base using (List; []; _∷_)
diff --git a/src/Codata/Sized/Colist/Properties.agda b/src/Codata/Sized/Colist/Properties.agda
index de5925e482..5b77551b7f 100644
--- a/src/Codata/Sized/Colist/Properties.agda
+++ b/src/Codata/Sized/Colist/Properties.agda
@@ -27,7 +27,7 @@ open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
 import Data.Maybe.Properties as Maybeₚ
 open import Data.Maybe.Relation.Unary.All using (All; nothing; just)
 open import Data.Nat.Base as ℕ using (zero; suc; z≤n; s≤s)
-open import Data.Product as Prod using (_×_; _,_; uncurry)
+open import Data.Product.Base as Prod using (_×_; _,_; uncurry)
 open import Data.These.Base as These using (These; this; that; these)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Function.Base
diff --git a/src/Codata/Sized/M/Bisimilarity.agda b/src/Codata/Sized/M/Bisimilarity.agda
index 3a60a91d16..ef26860e66 100644
--- a/src/Codata/Sized/M/Bisimilarity.agda
+++ b/src/Codata/Sized/M/Bisimilarity.agda
@@ -14,7 +14,7 @@ open import Codata.Sized.Thunk
 open import Codata.Sized.M
 open import Data.Container.Core
 open import Data.Container.Relation.Binary.Pointwise using (Pointwise; _,_)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_∋_)
 open import Relation.Binary
 import Relation.Binary.PropositionalEquality.Core as P
diff --git a/src/Codata/Sized/M/Properties.agda b/src/Codata/Sized/M/Properties.agda
index 4161f4d1f1..f9801448f5 100644
--- a/src/Codata/Sized/M/Properties.agda
+++ b/src/Codata/Sized/M/Properties.agda
@@ -15,7 +15,7 @@ open import Codata.Sized.M
 open import Codata.Sized.M.Bisimilarity
 open import Data.Container.Core as C hiding (map)
 import Data.Container.Morphism as Mp
-open import Data.Product as Prod using (_,_)
+open import Data.Product.Base as Prod using (_,_)
 open import Data.Product.Properties hiding (map-cong)
 open import Function.Base using (_$′_; _∘′_)
 import Relation.Binary.PropositionalEquality.Core as P
diff --git a/src/Codata/Sized/Stream/Effectful.agda b/src/Codata/Sized/Stream/Effectful.agda
index 00fe7eb2b1..a9636ad027 100644
--- a/src/Codata/Sized/Stream/Effectful.agda
+++ b/src/Codata/Sized/Stream/Effectful.agda
@@ -8,7 +8,7 @@
 
 module Codata.Sized.Stream.Effectful where
 
-open import Data.Product using (<_,_>)
+open import Data.Product.Base using (<_,_>)
 open import Codata.Sized.Stream
 open import Effect.Functor
 open import Effect.Applicative
diff --git a/src/Codata/Sized/Stream/Properties.agda b/src/Codata/Sized/Stream/Properties.agda
index 51b0719c7d..69685e12b2 100644
--- a/src/Codata/Sized/Stream/Properties.agda
+++ b/src/Codata/Sized/Stream/Properties.agda
@@ -20,7 +20,7 @@ open import Data.Nat.GeneralisedArithmetic using (fold; fold-pull)
 open import Data.List.Base as List using ([]; _∷_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
 import Data.List.Relation.Binary.Equality.Propositional as Eq
-open import Data.Product as Prod using (_,_)
+open import Data.Product.Base as Prod using (_,_)
 open import Data.Vec.Base as Vec using (_∷_)
 
 open import Function.Base using (id; _$_; _∘′_; const)
diff --git a/src/Data/AVL/IndexedMap.agda b/src/Data/AVL/IndexedMap.agda
index 25bccdee5f..84dbcceba4 100644
--- a/src/Data/AVL/IndexedMap.agda
+++ b/src/Data/AVL/IndexedMap.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.Product as Prod
+open import Data.Product.Base using (∃)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst)
 import Data.Tree.AVL.Value
diff --git a/src/Data/Char/Properties.agda b/src/Data/Char/Properties.agda
index 2bbf63ab17..52a997fd81 100644
--- a/src/Data/Char/Properties.agda
+++ b/src/Data/Char/Properties.agda
@@ -12,7 +12,7 @@ open import Data.Bool.Base using (Bool)
 open import Data.Char.Base
 import Data.Nat.Base as ℕ
 import Data.Nat.Properties as ℕₚ
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 
 open import Function.Base
 open import Relation.Nullary using (¬_; yes; no)
diff --git a/src/Data/Digit/Properties.agda b/src/Data/Digit/Properties.agda
index 37ead69a28..113bdde6ca 100644
--- a/src/Data/Digit/Properties.agda
+++ b/src/Data/Digit/Properties.agda
@@ -11,7 +11,7 @@ import Data.Char.Properties as Charₚ
 open import Data.Nat.Base using (ℕ)
 open import Data.Nat.Properties using (_≤?_)
 open import Data.Fin.Properties using (inject≤-injective)
-open import Data.Product using (_,_; proj₁)
+open import Data.Product.Base using (_,_; proj₁)
 open import Data.Vec.Relation.Unary.Unique.Propositional using (Unique)
 import Data.Vec.Relation.Unary.Unique.Propositional.Properties as Uniqueₚ
 open import Data.Vec.Relation.Unary.AllPairs using (allPairs?)
diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda
index 3c9bf54546..b0cf553d0d 100644
--- a/src/Data/Fin/Induction.agda
+++ b/src/Data/Fin/Induction.agda
@@ -13,7 +13,7 @@ open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _∸_; s≤s)
 open import Data.Nat.Properties using (n<1+n; ≤⇒≯)
 import Data.Nat.Induction as ℕ
 import Data.Nat.Properties as ℕ
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Data.Vec.Relation.Unary.Linked as Linked using (Linked; [-]; _∷_)
 import Data.Vec.Relation.Unary.Linked.Properties as Linkedₚ
diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index f6a7820b52..852a609779 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -15,7 +15,7 @@ open import Data.Fin.Patterns
 open import Data.Fin.Properties
 import Data.Fin.Permutation.Components as PC
 open import Data.Nat.Base using (ℕ; suc; zero)
-open import Data.Product using (_,_; proj₂)
+open import Data.Product.Base using (_,_; proj₂)
 open import Function.Bundles using (_↔_; Injection; Inverse; mk↔′)
 open import Function.Construct.Composition using (_↔-∘_)
 open import Function.Construct.Identity using (↔-id)
diff --git a/src/Data/Fin/Permutation/Components.agda b/src/Data/Fin/Permutation/Components.agda
index b053cee86b..e75fa29eb2 100644
--- a/src/Data/Fin/Permutation/Components.agda
+++ b/src/Data/Fin/Permutation/Components.agda
@@ -13,7 +13,7 @@ open import Data.Fin.Base
 open import Data.Fin.Properties
 open import Data.Nat.Base as ℕ using (zero; suc; _∸_)
 import Data.Nat.Properties as ℕₚ
-open import Data.Product using (proj₂)
+open import Data.Product.Base using (proj₂)
 open import Function.Base using (_∘_)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary using (does; _because_; yes; no)
diff --git a/src/Data/Fin/Permutation/Transposition/List.agda b/src/Data/Fin/Permutation/Transposition/List.agda
index 07feee0020..4da8f08d37 100644
--- a/src/Data/Fin/Permutation/Transposition/List.agda
+++ b/src/Data/Fin/Permutation/Transposition/List.agda
@@ -14,7 +14,7 @@ open import Data.Fin.Permutation as P hiding (lift₀)
 import Data.Fin.Permutation.Components as PC
 open import Data.List.Base using (List; []; _∷_; map)
 open import Data.Nat.Base using (ℕ; suc; zero)
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Function.Base using (_∘_)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; sym; cong; module ≡-Reasoning)
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 518c1456f4..78011e54b1 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -21,11 +21,10 @@ open import Data.Nat as ℕ
   hiding (module ℕ)
 import Data.Nat.Properties as ℕ
 open import Data.Nat.Solver
-open import Data.Product using (proj₁; proj₂; _,_)
+open import Data.Product.Base using (proj₁; proj₂; _,_; _×_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Sign as Sign using (Sign) renaming (_*_ to _𝕊*_)
 import Data.Sign.Properties as 𝕊ₚ
-open import Data.Product using (_×_)
 open import Function.Base using (_∘_; _$_; id)
 open import Level using (0ℓ)
 open import Relation.Binary
diff --git a/src/Data/List/Extrema/Core.agda b/src/Data/List/Extrema/Core.agda
index 1fb59ae06d..0ed9dbe159 100644
--- a/src/Data/List/Extrema/Core.agda
+++ b/src/Data/List/Extrema/Core.agda
@@ -15,7 +15,7 @@ open import Algebra.Core
 open import Algebra.Definitions
 import Algebra.Construct.NaturalChoice.Min as Min
 import Algebra.Construct.NaturalChoice.Max as Max
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
diff --git a/src/Data/List/Extrema/Nat.agda b/src/Data/List/Extrema/Nat.agda
index 6e2899b8e6..89f513e2bf 100644
--- a/src/Data/List/Extrema/Nat.agda
+++ b/src/Data/List/Extrema/Nat.agda
@@ -18,7 +18,7 @@ open import Data.List.Base using (List)
 import Data.List.Extrema
 open import Data.List.Relation.Unary.Any as Any using (Any)
 open import Data.List.Relation.Unary.All as All using (All)
-open import Data.Product using (_×_; _,_; uncurry′)
+open import Data.Product.Base using (_×_; _,_; uncurry′)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core using (_≢_)
 
diff --git a/src/Data/List/Fresh/Properties.agda b/src/Data/List/Fresh/Properties.agda
index cc8925eca6..b22347f92e 100644
--- a/src/Data/List/Fresh/Properties.agda
+++ b/src/Data/List/Fresh/Properties.agda
@@ -9,7 +9,7 @@
 module Data.List.Fresh.Properties where
 
 open import Level using (Level; _⊔_; Lift)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Relation.Nullary
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary as B using (Rel)
diff --git a/src/Data/List/Fresh/Relation/Unary/All.agda b/src/Data/List/Fresh/Relation/Unary/All.agda
index c013f934bb..b0e2115ce1 100644
--- a/src/Data/List/Fresh/Relation/Unary/All.agda
+++ b/src/Data/List/Fresh/Relation/Unary/All.agda
@@ -9,7 +9,7 @@
 module Data.List.Fresh.Relation.Unary.All where
 
 open import Level using (Level; _⊔_; Lift)
-open import Data.Product using (_×_; _,_; proj₁; uncurry)
+open import Data.Product.Base using (_×_; _,_; proj₁; uncurry)
 open import Data.Sum.Base as Sum using (inj₁; inj₂)
 open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_)
 open import Relation.Unary  as U
diff --git a/src/Data/List/Fresh/Relation/Unary/All/Properties.agda b/src/Data/List/Fresh/Relation/Unary/All/Properties.agda
index f2c47657b5..8c2f0c80b4 100644
--- a/src/Data/List/Fresh/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Fresh/Relation/Unary/All/Properties.agda
@@ -11,7 +11,7 @@ module Data.List.Fresh.Relation.Unary.All.Properties where
 open import Level using (Level; _⊔_; Lift)
 open import Data.Empty
 open import Data.Nat.Base using (ℕ; zero; suc)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘′_)
 open import Relation.Nullary
 open import Relation.Unary  as U
diff --git a/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda b/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda
index 09ec3d5333..8b47063949 100644
--- a/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda
@@ -12,7 +12,7 @@ open import Level using (Level; _⊔_; Lift)
 open import Data.Bool.Base using (true; false)
 open import Data.Empty
 open import Data.Nat.Base using (ℕ; zero; suc)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘′_)
 open import Relation.Nullary.Reflects using (invert)
diff --git a/src/Data/List/Nary/NonDependent.agda b/src/Data/List/Nary/NonDependent.agda
index 6fff2b0dac..f95da6345c 100644
--- a/src/Data/List/Nary/NonDependent.agda
+++ b/src/Data/List/Nary/NonDependent.agda
@@ -10,7 +10,7 @@ module Data.List.Nary.NonDependent where
 
 open import Data.Nat.Base using (zero; suc)
 open import Data.List.Base as List using (List; []; _∷_)
-open import Data.Product as Prod using (_,_)
+open import Data.Product.Base as Prod using (_,_)
 open import Data.Product.Nary.NonDependent using (Product)
 open import Function.Base using ()
 open import Function.Nary.NonDependent.Base
diff --git a/src/Data/List/NonEmpty/Effectful.agda b/src/Data/List/NonEmpty/Effectful.agda
index 654002c839..5b37642808 100644
--- a/src/Data/List/NonEmpty/Effectful.agda
+++ b/src/Data/List/NonEmpty/Effectful.agda
@@ -11,7 +11,7 @@ module Data.List.NonEmpty.Effectful where
 open import Agda.Builtin.List
 import Data.List.Effectful as List
 open import Data.List.NonEmpty.Base
-open import Data.Product using (uncurry)
+open import Data.Product.Base using (uncurry)
 open import Effect.Functor
 open import Effect.Applicative
 open import Effect.Monad
diff --git a/src/Data/List/Relation/Binary/Disjoint/Setoid.agda b/src/Data/List/Relation/Binary/Disjoint/Setoid.agda
index d5003aab4e..6ea7e15cf7 100644
--- a/src/Data/List/Relation/Binary/Disjoint/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Disjoint/Setoid.agda
@@ -15,7 +15,7 @@ open import Relation.Nullary.Negation using (¬_)
 open import Function.Base using (_∘_)
 open import Data.List.Base using (List; []; [_]; _∷_)
 open import Data.List.Relation.Unary.Any using (here; there)
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 
 open Setoid S renaming (Carrier to A)
 open import Data.List.Membership.Setoid S using (_∈_; _∉_)
diff --git a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
index 3f0701a8ef..43a67d4d7d 100644
--- a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
@@ -14,7 +14,7 @@ import Data.List.Relation.Unary.Any as Any
 open import Data.List.Relation.Unary.All as All
 open import Data.List.Relation.Unary.All.Properties using (¬Any⇒All¬)
 open import Data.List.Relation.Unary.Any.Properties using (++⁻)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Relation.Binary
 open import Relation.Nullary.Negation using (¬_)
diff --git a/src/Data/List/Relation/Binary/Lex/Strict.agda b/src/Data/List/Relation/Binary/Lex/Strict.agda
index fef11ad07e..c0428b347d 100644
--- a/src/Data/List/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/List/Relation/Binary/Lex/Strict.agda
@@ -14,7 +14,7 @@ module Data.List.Relation.Binary.Lex.Strict where
 open import Data.Empty using (⊥)
 open import Data.Unit.Base using (⊤; tt)
 open import Function.Base using (_∘_; id)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.List.Base using (List; []; _∷_)
 open import Level using (_⊔_)
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index 135d5a778d..dc7e34db86 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -13,7 +13,7 @@ open import Algebra.Definitions
 open import Algebra.Structures
 open import Data.Bool.Base using (Bool; true; false)
 open import Data.Nat using (suc)
-open import Data.Product using (-,_; proj₂)
+open import Data.Product.Base using (-,_; proj₂)
 open import Data.List.Base as List
 open import Data.List.Relation.Binary.Permutation.Propositional
 open import Data.List.Relation.Unary.Any using (Any; here; there)
diff --git a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
index da5a26e6e0..21e61b4aa4 100644
--- a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
@@ -19,7 +19,7 @@ open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
 open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix hiding (PrefixView; _++_)
 open import Data.Nat.Base using (ℕ; zero; suc; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (suc-injective)
-open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂; uncurry)
+open import Data.Product.Base as Prod using (_×_; _,_; proj₁; proj₂; uncurry)
 open import Function.Base
 
 open import Relation.Nullary.Negation using (¬_)