diff --git a/README/Case.agda b/README/Case.agda
index 15449391d4..9de25c6e82 100644
--- a/README/Case.agda
+++ b/README/Case.agda
@@ -12,7 +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.Product
 open import Function.Base using (case_of_; case_return_of_)
 open import Relation.Nullary
 open import Relation.Binary
diff --git a/README/Data/Container/Indexed.agda b/README/Data/Container/Indexed.agda
index 7ace9736f1..adf6cbc9e5 100644
--- a/README/Data/Container/Indexed.agda
+++ b/README/Data/Container/Indexed.agda
@@ -11,7 +11,7 @@ module README.Data.Container.Indexed where
 open import Data.Unit
 open import Data.Empty
 open import Data.Nat.Base
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_∋_)
 open import Data.W.Indexed
 open import Data.Container.Indexed
diff --git a/README/Data/Integer.agda b/README/Data/Integer.agda
index e93333dcf5..23619757d3 100644
--- a/README/Data/Integer.agda
+++ b/README/Data/Integer.agda
@@ -51,7 +51,6 @@ ex₅ i j = ℤₚ.*-comm i j
 -- provides some combinators for equational reasoning.
 
 open P.≡-Reasoning
-open import Data.Product
 
 ex₆ : ∀ i j → i * (j + + 0) ≡ j * i
 ex₆ i j = begin
diff --git a/README/Data/List/Fresh.agda b/README/Data/List/Fresh.agda
index 27f7eb7ca0..4723c0631e 100644
--- a/README/Data/List/Fresh.agda
+++ b/README/Data/List/Fresh.agda
@@ -12,7 +12,7 @@ open import Data.Nat
 open import Data.List.Base
 open import Data.List.Fresh
 open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
-open import Data.Product
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Relation.Nary using (⌊_⌋; fromWitness)
 
 -- A sorted list of natural numbers can be seen as a fresh list
diff --git a/README/Data/Record.agda b/README/Data/Record.agda
index 5800d11e54..da0ae70dc4 100644
--- a/README/Data/Record.agda
+++ b/README/Data/Record.agda
@@ -11,7 +11,7 @@
 
 module README.Data.Record where
 
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Data.String
 open import Function.Base using (flip)
 open import Level
diff --git a/README/Data/Trie/NonDependent.agda b/README/Data/Trie/NonDependent.agda
index 9921942f6d..0484e6005a 100644
--- a/README/Data/Trie/NonDependent.agda
+++ b/README/Data/Trie/NonDependent.agda
@@ -56,7 +56,7 @@ import Data.Char.Properties  as Char
 open import Data.List.Base   as List using (List; []; _∷_)
 open import Data.List.Fresh  as List# using (List#; []; _∷#_)
 open import Data.Maybe       as Maybe
-open import Data.Product     as Prod
+open import Data.Product.Base as Prod using (_×_; ∃; proj₁; _,_)
 open import Data.String.Base as String using (String)
 open import Data.String.Properties as String using (_≟_)
 open import Data.These       as These
diff --git a/README/Data/Wrap.agda b/README/Data/Wrap.agda
index 35009e4ed4..b92a8a3c81 100644
--- a/README/Data/Wrap.agda
+++ b/README/Data/Wrap.agda
@@ -13,7 +13,7 @@ open import Data.Wrap
 open import Algebra
 open import Data.Nat
 open import Data.Nat.Properties
-open import Data.Product
+open import Data.Product.Base using (_,_; ∃; ∃₂; _×_)
 open import Level using (Level)
 open import Relation.Binary
 
diff --git a/README/Design/Decidability.agda b/README/Design/Decidability.agda
index cb41cf41ef..c6f086424f 100644
--- a/README/Design/Decidability.agda
+++ b/README/Design/Decidability.agda
@@ -13,7 +13,7 @@ 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)
-open import Data.Product
+open import Data.Product.Base using (uncurry)
 open import Data.Unit
 open import Function.Base using (id;  _∘_)
 open import Relation.Binary.PropositionalEquality
diff --git a/README/Foreign/Haskell.agda b/README/Foreign/Haskell.agda
index 61e757ea8f..38c6c78c4e 100644
--- a/README/Foreign/Haskell.agda
+++ b/README/Foreign/Haskell.agda
@@ -22,7 +22,7 @@ open import Data.Bool.Base using (Bool; if_then_else_)
 open import Data.Char as Char
 open import Data.List.Base as List using (List; _∷_; []; takeWhile; dropWhile)
 open import Data.Maybe.Base using (Maybe; just; nothing)
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_)
 open import Function
 open import Relation.Nullary.Decidable
 
diff --git a/README/Inspect.agda b/README/Inspect.agda
index 002005abaa..9f40a8d65a 100644
--- a/README/Inspect.agda
+++ b/README/Inspect.agda
@@ -14,7 +14,7 @@ module README.Inspect where
 
 open import Data.Nat.Base
 open import Data.Nat.Properties
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Binary.PropositionalEquality using (inspect)
 
diff --git a/README/Relation/Binary/TypeClasses.agda b/README/Relation/Binary/TypeClasses.agda
index 023e98c3e4..a836389ee4 100644
--- a/README/Relation/Binary/TypeClasses.agda
+++ b/README/Relation/Binary/TypeClasses.agda
@@ -19,7 +19,7 @@ open import Data.List.Instances
 open import Data.List.Relation.Binary.Lex.NonStrict using (Lex-≤)
 open import Data.Nat.Base renaming (_≤_ to _≤ℕ_)
 open import Data.Nat.Instances
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_; Σ)
 open import Data.Product.Instances
 open import Data.Unit.Base renaming (_≤_ to _≤⊤_)
 open import Data.Unit.Instances
diff --git a/README/Text/Pretty.agda b/README/Text/Pretty.agda
index 2525ff5242..855c599f08 100644
--- a/README/Text/Pretty.agda
+++ b/README/Text/Pretty.agda
@@ -14,7 +14,7 @@ open import Data.Bool.Base
 open import Data.List.Base as List
 open import Data.List.NonEmpty as List⁺
 open import Data.Nat.Base
-open import Data.Product
+open import Data.Product.Base using (_×_; uncurry; _,_)
 open import Data.String.Base hiding (parens; _<+>_)
 open import Data.Vec.Base as Vec
 open import Function.Base
diff --git a/src/Algebra/Apartness/Structures.agda b/src/Algebra/Apartness/Structures.agda
index 3311234945..a8c5c88982 100644
--- a/src/Algebra/Apartness/Structures.agda
+++ b/src/Algebra/Apartness/Structures.agda
@@ -17,7 +17,7 @@ module Algebra.Apartness.Structures
   where
 
 open import Level using (_⊔_; suc)
-open import Data.Product using (∃-syntax; _×_; _,_; proj₂)
+open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₂)
 open import Algebra.Definitions _≈_ using (Invertible)
 open import Algebra.Structures _≈_ using (IsCommutativeRing)
 open import Relation.Binary.Structures using (IsEquivalence; IsApartnessRelation)
diff --git a/src/Algebra/Construct/DirectProduct.agda b/src/Algebra/Construct/DirectProduct.agda
index 7722662114..5f7b042017 100644
--- a/src/Algebra/Construct/DirectProduct.agda
+++ b/src/Algebra/Construct/DirectProduct.agda
@@ -16,7 +16,7 @@
 module Algebra.Construct.DirectProduct where
 
 open import Algebra
-open import Data.Product
+open import Data.Product.Base using (_×_; zip; _,_; map; _<*>_; uncurry)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Level using (Level; _⊔_)
 
diff --git a/src/Algebra/Construct/LexProduct.agda b/src/Algebra/Construct/LexProduct.agda
index 1301ff7c04..984cdd57f2 100644
--- a/src/Algebra/Construct/LexProduct.agda
+++ b/src/Algebra/Construct/LexProduct.agda
@@ -8,7 +8,7 @@
 
 open import Algebra
 open import Data.Bool using (true; false)
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (Pointwise)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_∘_)
diff --git a/src/Algebra/Lattice/Construct/DirectProduct.agda b/src/Algebra/Lattice/Construct/DirectProduct.agda
index 9e2a825c99..0c68071a51 100644
--- a/src/Algebra/Lattice/Construct/DirectProduct.agda
+++ b/src/Algebra/Lattice/Construct/DirectProduct.agda
@@ -16,7 +16,7 @@
 open import Algebra
 open import Algebra.Lattice
 import Algebra.Construct.DirectProduct as DirectProduct
-open import Data.Product
+open import Data.Product.Base using (_,_; _<*>_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Level using (Level; _⊔_)
 
diff --git a/src/Algebra/Module/Construct/DirectProduct.agda b/src/Algebra/Module/Construct/DirectProduct.agda
index 3c168564bd..840cc42cab 100644
--- a/src/Algebra/Module/Construct/DirectProduct.agda
+++ b/src/Algebra/Module/Construct/DirectProduct.agda
@@ -14,7 +14,7 @@ module Algebra.Module.Construct.DirectProduct where
 open import Algebra.Bundles
 open import Algebra.Construct.DirectProduct
 open import Algebra.Module.Bundles
-open import Data.Product
+open import Data.Product.Base using (map; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Level
 
diff --git a/src/Algebra/Module/Definitions/Left.agda b/src/Algebra/Module/Definitions/Left.agda
index e43f2ef38e..3c04e82cd0 100644
--- a/src/Algebra/Module/Definitions/Left.agda
+++ b/src/Algebra/Module/Definitions/Left.agda
@@ -15,8 +15,6 @@ module Algebra.Module.Definitions.Left
   {a b ℓb} (A : Set a) {B : Set b} (_≈_ : Rel B ℓb)
   where
 
-open import Data.Product
-
 ------------------------------------------------------------------------
 -- Binary operations
 
diff --git a/src/Algebra/Module/Definitions/Right.agda b/src/Algebra/Module/Definitions/Right.agda
index 875dcfc594..92b90a477c 100644
--- a/src/Algebra/Module/Definitions/Right.agda
+++ b/src/Algebra/Module/Definitions/Right.agda
@@ -15,8 +15,6 @@ module Algebra.Module.Definitions.Right
   {a b ℓb} (A : Set a) {B : Set b} (_≈_ : Rel B ℓb)
   where
 
-open import Data.Product
-
 ------------------------------------------------------------------------
 -- Binary operations
 
diff --git a/src/Algebra/Module/Morphism/ModuleHomomorphism.agda b/src/Algebra/Module/Morphism/ModuleHomomorphism.agda
index 47ae46de10..704ec3863c 100644
--- a/src/Algebra/Module/Morphism/ModuleHomomorphism.agda
+++ b/src/Algebra/Module/Morphism/ModuleHomomorphism.agda
@@ -25,7 +25,7 @@ module Algebra.Module.Morphism.ModuleHomomorphism
   where
 
 open import Axiom.DoubleNegationElimination
-open import Data.Product
+open import Data.Product.Base using (∃₂; _×_; _,_)
 open import Relation.Binary.Reasoning.MultiSetoid
 open import Relation.Nullary          using (¬_)
 open import Relation.Nullary.Negation using (contraposition)
diff --git a/src/Algebra/Morphism/Construct/Composition.agda b/src/Algebra/Morphism/Construct/Composition.agda
index e3f3a3ad71..5087de2ae3 100644
--- a/src/Algebra/Morphism/Construct/Composition.agda
+++ b/src/Algebra/Morphism/Construct/Composition.agda
@@ -10,7 +10,6 @@ module Algebra.Morphism.Construct.Composition where
 
 open import Algebra.Bundles
 open import Algebra.Morphism.Structures
-open import Data.Product
 open import Function.Base using (_∘_)
 import Function.Construct.Composition as Func
 open import Level using (Level)
diff --git a/src/Algebra/Morphism/GroupMonomorphism.agda b/src/Algebra/Morphism/GroupMonomorphism.agda
index b7a09ce92c..b862559938 100644
--- a/src/Algebra/Morphism/GroupMonomorphism.agda
+++ b/src/Algebra/Morphism/GroupMonomorphism.agda
@@ -26,7 +26,7 @@ open RawGroup G₂ renaming
 
 open import Algebra.Definitions
 open import Algebra.Structures
-open import Data.Product
+open import Data.Product.Base using (_,_)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 
 ------------------------------------------------------------------------
diff --git a/src/Algebra/Morphism/MagmaMonomorphism.agda b/src/Algebra/Morphism/MagmaMonomorphism.agda
index c952fe112e..30f19edb02 100644
--- a/src/Algebra/Morphism/MagmaMonomorphism.agda
+++ b/src/Algebra/Morphism/MagmaMonomorphism.agda
@@ -25,7 +25,7 @@ open RawMagma M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_)
 
 open import Algebra.Structures
 open import Algebra.Definitions
-open import Data.Product
+open import Data.Product.Base using (map)
 open import Data.Sum.Base using (inj₁; inj₂)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 import Relation.Binary.Morphism.RelMonomorphism isRelMonomorphism as RelMorphism
diff --git a/src/Algebra/Morphism/RingMonomorphism.agda b/src/Algebra/Morphism/RingMonomorphism.agda
index f9789e60b7..4b2c900946 100644
--- a/src/Algebra/Morphism/RingMonomorphism.agda
+++ b/src/Algebra/Morphism/RingMonomorphism.agda
@@ -28,7 +28,7 @@ open RawRing R₂ renaming
 
 open import Algebra.Definitions
 open import Algebra.Structures
-open import Data.Product
+open import Data.Product.Base using (proj₁; proj₂; _,_)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 
 ------------------------------------------------------------------------
diff --git a/src/Algebra/Properties/Loop.agda b/src/Algebra/Properties/Loop.agda
index 26bf6f4ce6..1ecb2c52f4 100644
--- a/src/Algebra/Properties/Loop.agda
+++ b/src/Algebra/Properties/Loop.agda
@@ -13,7 +13,6 @@ module Algebra.Properties.Loop {l₁ l₂} (L : Loop l₁ l₂) where
 open Loop L
 open import Algebra.Definitions _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
-open import Data.Product
 open import Algebra.Properties.Quasigroup
 
 x//x≈ε : ∀ x → x // x ≈ ε
diff --git a/src/Algebra/Properties/Magma/Divisibility.agda b/src/Algebra/Properties/Magma/Divisibility.agda
index 72907929df..d8ffc208f0 100644
--- a/src/Algebra/Properties/Magma/Divisibility.agda
+++ b/src/Algebra/Properties/Magma/Divisibility.agda
@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra using (Magma)
-open import Data.Product using (_×_; _,_; ∃; map; swap)
+open import Data.Product.Base using (_×_; _,_; ∃; map; swap)
 open import Relation.Binary.Definitions
 
 module Algebra.Properties.Magma.Divisibility {a ℓ} (M : Magma a ℓ) where
diff --git a/src/Algebra/Properties/MiddleBolLoop.agda b/src/Algebra/Properties/MiddleBolLoop.agda
index a50ce3b0d5..60f2898496 100644
--- a/src/Algebra/Properties/MiddleBolLoop.agda
+++ b/src/Algebra/Properties/MiddleBolLoop.agda
@@ -13,7 +13,6 @@ module Algebra.Properties.MiddleBolLoop {m₁ m₂} (M : MiddleBolLoop m₁ m₂
 open MiddleBolLoop M
 open import Algebra.Definitions _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
-open import Data.Product
 import Algebra.Properties.Loop as LoopProperties
 open LoopProperties loop public
 
diff --git a/src/Algebra/Properties/MoufangLoop.agda b/src/Algebra/Properties/MoufangLoop.agda
index 4740bc19b6..9b0e5ac94b 100644
--- a/src/Algebra/Properties/MoufangLoop.agda
+++ b/src/Algebra/Properties/MoufangLoop.agda
@@ -13,7 +13,7 @@ module Algebra.Properties.MoufangLoop {a ℓ} (M : MoufangLoop a ℓ) where
 open MoufangLoop M
 open import Algebra.Definitions _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
-open import Data.Product
+open import Data.Product.Base using (_,_)
 
 alternativeˡ : LeftAlternative _∙_
 alternativeˡ x y = begin
diff --git a/src/Algebra/Properties/Quasigroup.agda b/src/Algebra/Properties/Quasigroup.agda
index a583ae34f5..335a9ea7a3 100644
--- a/src/Algebra/Properties/Quasigroup.agda
+++ b/src/Algebra/Properties/Quasigroup.agda
@@ -13,7 +13,7 @@ module Algebra.Properties.Quasigroup {q₁ q₂} (Q : Quasigroup q₁ q₂) wher
 open Quasigroup Q
 open import Algebra.Definitions _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
-open import Data.Product
+open import Data.Product.Base using (_,_)
 
 cancelˡ : LeftCancellative _∙_
 cancelˡ x y z eq = begin
diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda
index 23e994821c..f80a2847f6 100644
--- a/src/Algebra/Solver/Monoid.agda
+++ b/src/Algebra/Solver/Monoid.agda
@@ -17,7 +17,7 @@ import Data.List.Relation.Binary.Equality.DecPropositional as ListEq
 open import Data.Maybe.Base as Maybe
   using (Maybe; decToMaybe; From-just; from-just)
 open import Data.Nat.Base using (ℕ)
-open import Data.Product
+open import Data.Product.Base using (_×_; uncurry)
 open import Data.Vec.Base using (Vec; lookup)
 open import Function.Base using (_∘_; _$_)
 open import Relation.Binary.Definitions using (Decidable)
diff --git a/src/Codata/Musical/Colist.agda b/src/Codata/Musical/Colist.agda
index d70a101f6a..3ef672abc7 100644
--- a/src/Codata/Musical/Colist.agda
+++ b/src/Codata/Musical/Colist.agda
@@ -21,7 +21,7 @@ open import Data.Maybe.Relation.Unary.Any using (just)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.NonEmpty using (List⁺; _∷_)
-open import Data.Product as Prod using (∃; _×_; _,_)
+open import Data.Product.Base as Prod using (∃; _×_; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Vec.Bounded as Vec≤ using (Vec≤)
 open import Function.Base
diff --git a/src/Codata/Musical/Colist/Infinite-merge.agda b/src/Codata/Musical/Colist/Infinite-merge.agda
index 677024808a..eb06c3b9cc 100644
--- a/src/Codata/Musical/Colist/Infinite-merge.agda
+++ b/src/Codata/Musical/Colist/Infinite-merge.agda
@@ -13,7 +13,7 @@ open import Codata.Musical.Colist as Colist hiding (_⋎_)
 open import Data.Nat.Base
 open import Data.Nat.Induction using (<′-wellFounded)
 open import Data.Nat.Properties
-open import Data.Product as Prod
+open import Data.Product.Base as Prod using (_×_; _,_; ∃; ∃₂; proj₁; proj₂)
 open import Data.Sum.Base
 open import Data.Sum.Properties
 open import Data.Sum.Function.Propositional using (_⊎-cong_)
diff --git a/src/Codata/Musical/Conversion.agda b/src/Codata/Musical/Conversion.agda
index d7213daba9..4e5886e000 100644
--- a/src/Codata/Musical/Conversion.agda
+++ b/src/Codata/Musical/Conversion.agda
@@ -27,7 +27,7 @@ open import Codata.Musical.Covec hiding (module Covec)
 open import Codata.Musical.M hiding (module M)
 open import Codata.Musical.Notation
 open import Codata.Musical.Stream hiding (module Stream)
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Data.Container.Core as C using (Container)
 import Size
 
diff --git a/src/Codata/Musical/M/Indexed.agda b/src/Codata/Musical/M/Indexed.agda
index 964aca0695..3eefda55e6 100644
--- a/src/Codata/Musical/M/Indexed.agda
+++ b/src/Codata/Musical/M/Indexed.agda
@@ -11,7 +11,7 @@ module Codata.Musical.M.Indexed where
 
 open import Level
 open import Codata.Musical.Notation
-open import Data.Product
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Data.Container.Indexed.Core
 open import Function.Base using (_∘_)
 open import Relation.Unary
diff --git a/src/Data/Container/Combinator.agda b/src/Data/Container/Combinator.agda
index c68536427b..01e102cd5c 100644
--- a/src/Data/Container/Combinator.agda
+++ b/src/Data/Container/Combinator.agda
@@ -10,7 +10,7 @@ module Data.Container.Combinator where
 
 open import Level using (Level; _⊔_; lower)
 open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
-open import Data.Product as P using (_,_; <_,_>; proj₁; proj₂; ∃)
+open import Data.Product.Base as P using (_,_; <_,_>; proj₁; proj₂; ∃)
 open import Data.Sum.Base as S using ([_,_]′)
 open import Data.Unit.Polymorphic.Base using (⊤)
 import Function.Base as F
diff --git a/src/Data/Container/Combinator/Properties.agda b/src/Data/Container/Combinator/Properties.agda
index b93d6c7a7a..8d347abcae 100644
--- a/src/Data/Container/Combinator/Properties.agda
+++ b/src/Data/Container/Combinator/Properties.agda
@@ -13,7 +13,7 @@ open import Data.Container.Core
 open import Data.Container.Combinator
 open import Data.Container.Relation.Unary.Any
 open import Data.Empty using (⊥-elim)
-open import Data.Product as Prod using (∃; _,_; proj₁; proj₂; <_,_>; uncurry; curry)
+open import Data.Product.Base as Prod using (∃; _,_; proj₁; proj₂; <_,_>; uncurry; curry)
 open import Data.Sum.Base as S using (inj₁; inj₂; [_,_]′; [_,_])
 open import Function.Base as F using (_∘′_)
 open import Function.Inverse as Inv using (_↔_; inverse; module Inverse)
diff --git a/src/Data/Container/Indexed/Combinator.agda b/src/Data/Container/Indexed/Combinator.agda
index 43721d4689..283a6a0314 100644
--- a/src/Data/Container/Indexed/Combinator.agda
+++ b/src/Data/Container/Indexed/Combinator.agda
@@ -12,7 +12,7 @@ open import Axiom.Extensionality.Propositional using (Extensionality)
 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.Product.Base as Prod hiding (Σ) 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 _⟨∘⟩_)
diff --git a/src/Data/Container/Indexed/Core.agda b/src/Data/Container/Indexed/Core.agda
index 91fb4b2e21..75d1a0d986 100644
--- a/src/Data/Container/Indexed/Core.agda
+++ b/src/Data/Container/Indexed/Core.agda
@@ -9,7 +9,7 @@
 module Data.Container.Indexed.Core where
 
 open import Level
-open import Data.Product
+open import Data.Product.Base using (Σ; Σ-syntax; _,_; ∃)
 open import Relation.Unary
 
 infix 5 _◃_/_
diff --git a/src/Data/Container/Indexed/FreeMonad.agda b/src/Data/Container/Indexed/FreeMonad.agda
index 1c6ee81c1a..294ab0bd34 100644
--- a/src/Data/Container/Indexed/FreeMonad.agda
+++ b/src/Data/Container/Indexed/FreeMonad.agda
@@ -15,7 +15,7 @@ open import Data.Container.Indexed
 open import Data.Container.Indexed.Combinator hiding (id; _∘_)
 open import Data.Empty
 open import Data.Sum.Base using (inj₁; inj₂)
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Data.W.Indexed
 open import Relation.Unary
 open import Relation.Unary.PredicateTransformer
diff --git a/src/Data/Container/Indexed/WithK.agda b/src/Data/Container/Indexed/WithK.agda
index ca5f18205d..9897402264 100644
--- a/src/Data/Container/Indexed/WithK.agda
+++ b/src/Data/Container/Indexed/WithK.agda
@@ -15,7 +15,8 @@ module Data.Container.Indexed.WithK where
 
 open import Axiom.Extensionality.Heterogeneous using (Extensionality)
 open import Data.Container.Indexed hiding (module PlainMorphism)
-open import Data.Product as Prod hiding (map)
+open import Data.Product.Base
+  using (_,_; -,_; _×_; ∃; proj₁; proj₂; Σ-syntax)
 open import Function.Base renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
 open import Level
 open import Relation.Unary using (Pred; _⊆_)
diff --git a/src/Data/Container/Morphism/Properties.agda b/src/Data/Container/Morphism/Properties.agda
index fc71843263..c0d84007b4 100644
--- a/src/Data/Container/Morphism/Properties.agda
+++ b/src/Data/Container/Morphism/Properties.agda
@@ -10,7 +10,7 @@ module Data.Container.Morphism.Properties where
 
 open import Level using (_⊔_; suc)
 open import Function.Base as F using (_$_)
-open import Data.Product using (∃; proj₁; proj₂; _,_)
+open import Data.Product.Base using (∃; proj₁; proj₂; _,_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)
 
diff --git a/src/Data/Container/Relation/Unary/All.agda b/src/Data/Container/Relation/Unary/All.agda
index 65d593eea4..829bd3a0c9 100644
--- a/src/Data/Container/Relation/Unary/All.agda
+++ b/src/Data/Container/Relation/Unary/All.agda
@@ -10,7 +10,7 @@ module Data.Container.Relation.Unary.All where
 
 open import Level using (_⊔_)
 open import Relation.Unary using (Pred; _⊆_)
-open import Data.Product as Prod using (_,_; proj₁; proj₂; ∃)
+open import Data.Product.Base using (_,_; proj₁; proj₂; ∃)
 open import Function.Base using (_∘′_; id)
 
 open import Data.Container.Core hiding (map)
diff --git a/src/Data/Container/Relation/Unary/Any.agda b/src/Data/Container/Relation/Unary/Any.agda
index de3937f221..121391f4d6 100644
--- a/src/Data/Container/Relation/Unary/Any.agda
+++ b/src/Data/Container/Relation/Unary/Any.agda
@@ -10,7 +10,7 @@ module Data.Container.Relation.Unary.Any where
 
 open import Level using (_⊔_)
 open import Relation.Unary using (Pred; _⊆_)
-open import Data.Product as Prod using (_,_; proj₂; ∃)
+open import Data.Product.Base using (_,_; proj₂; ∃)
 open import Function.Base using (_∘′_; id)
 
 open import Data.Container.Core hiding (map)
diff --git a/src/Data/Container/Relation/Unary/Any/Properties.agda b/src/Data/Container/Relation/Unary/Any/Properties.agda
index ceae1510c9..d1d35c5a02 100644
--- a/src/Data/Container/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Container/Relation/Unary/Any/Properties.agda
@@ -10,7 +10,7 @@ module Data.Container.Relation.Unary.Any.Properties where
 
 open import Level
 open import Algebra
-open import Data.Product as Prod using (∃; _×_; ∃₂; _,_; proj₂)
+open import Data.Product.Base using (∃; _×_; ∃₂; _,_; proj₂)
 open import Data.Product.Function.NonDependent.Propositional using (_×-cong_)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
diff --git a/src/Data/Fin/Subset.agda b/src/Data/Fin/Subset.agda
index 01926df438..b3d53106ff 100644
--- a/src/Data/Fin/Subset.agda
+++ b/src/Data/Fin/Subset.agda
@@ -13,7 +13,7 @@ open import Data.Bool using (not; _∧_; _∨_; _≟_)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base using (List; foldr; foldl)
 open import Data.Nat.Base using (ℕ)
-open import Data.Product using (∃; _×_)
+open import Data.Product.Base using (∃; _×_)
 open import Data.Vec.Base hiding (foldr; foldl)
 open import Relation.Nullary
 
diff --git a/src/Data/Graph/Acyclic.agda b/src/Data/Graph/Acyclic.agda
index 586b28e278..d40d078bd3 100644
--- a/src/Data/Graph/Acyclic.agda
+++ b/src/Data/Graph/Acyclic.agda
@@ -20,7 +20,7 @@ open import Data.Fin as Fin
   using (Fin; Fin′; zero; suc; #_; toℕ; _≟_; opposite) renaming (_ℕ-ℕ_ to _-_)
 import Data.Fin.Properties as FP
 import Data.Fin.Permutation.Components as PC
-open import Data.Product as Prod using (∃; _×_; _,_)
+open import Data.Product.Base as Prod using (∃; _×_; _,_)
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; decToMaybe)
 open import Data.Empty
 open import Data.Unit.Base using (⊤; tt)
diff --git a/src/Data/Integer/GCD.agda b/src/Data/Integer/GCD.agda
index e087da4763..3f46877f45 100644
--- a/src/Data/Integer/GCD.agda
+++ b/src/Data/Integer/GCD.agda
@@ -13,7 +13,7 @@ open import Data.Integer.Divisibility
 open import Data.Integer.Properties
 open import Data.Nat.Base
 import Data.Nat.GCD as ℕ
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Relation.Binary.PropositionalEquality
 
 open import Algebra.Definitions {A = ℤ} _≡_ as Algebra
diff --git a/src/Data/List/Countdown.agda b/src/Data/List/Countdown.agda
index f1ef43ba8e..db8dc806ad 100644
--- a/src/Data/List/Countdown.agda
+++ b/src/Data/List/Countdown.agda
@@ -23,7 +23,7 @@ open import Data.Bool.Base using (true; false)
 open import Data.List.Base hiding (lookup)
 open import Data.List.Relation.Unary.Any as Any using (here; there)
 open import Data.Nat.Base using (ℕ; zero; suc)
-open import Data.Product
+open import Data.Product.Base using (∃; _,_; _×_)
 open import Data.Sum.Base
 open import Data.Sum.Properties
 open import Relation.Nullary.Reflects using (invert)
diff --git a/src/Data/List/Fresh/Membership/Setoid/Properties.agda b/src/Data/List/Fresh/Membership/Setoid/Properties.agda
index e287147516..d2f2634bf8 100644
--- a/src/Data/List/Fresh/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Fresh/Membership/Setoid/Properties.agda
@@ -15,7 +15,7 @@ open import Level using (Level; _⊔_)
 open import Data.Empty
 open import Data.Nat.Base
 open import Data.Nat.Properties
-open import Data.Product using (∃; _×_; _,_)
+open import Data.Product.Base using (∃; _×_; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; fromInj₂)
 
 open import Function.Base using (id; _∘′_; _$_)
diff --git a/src/Data/List/Fresh/Relation/Unary/Any.agda b/src/Data/List/Fresh/Relation/Unary/Any.agda
index 9c2050472c..dbb9dd0dec 100644
--- a/src/Data/List/Fresh/Relation/Unary/Any.agda
+++ b/src/Data/List/Fresh/Relation/Unary/Any.agda
@@ -10,7 +10,7 @@ module Data.List.Fresh.Relation.Unary.Any where
 
 open import Level using (Level; _⊔_; Lift)
 open import Data.Empty
-open import Data.Product using (∃; _,_; -,_)
+open import Data.Product.Base using (∃; _,_; -,_)
 open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Relation.Nullary.Negation using (¬_)
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index f781e1678d..dfef9fa160 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -22,7 +22,7 @@ open import Data.List.Relation.Binary.Equality.Propositional
 open import Data.List.Effectful using (monad)
 open import Data.Nat.Base using (ℕ; zero; suc; pred; s≤s; _≤_; _<_; _≤ᵇ_)
 open import Data.Nat.Properties
-open import Data.Product hiding (map)
+open import Data.Product.Base hiding (map)
 open import Data.Product.Function.NonDependent.Propositional using (_×-cong_)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda
index 85ad85aab0..aec90ef8d1 100644
--- a/src/Data/List/Membership/Propositional/Properties/Core.agda
+++ b/src/Data/List/Membership/Propositional/Properties/Core.agda
@@ -17,7 +17,7 @@ open import Function.Inverse using (_↔_; inverse)
 open import Data.List.Base using (List)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.List.Membership.Propositional
-open import Data.Product as Prod
+open import Data.Product.Base as Prod
   using (_,_; proj₁; proj₂; uncurry′; ∃; _×_)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core as P
diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
index 47768eed76..2fee07309f 100644
--- a/src/Data/List/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Membership/Setoid/Properties.agda
@@ -20,7 +20,7 @@ import Data.List.Relation.Binary.Equality.Setoid as Equality
 import Data.List.Relation.Unary.Unique.Setoid as Unique
 open import Data.Nat.Base using (suc; z≤n; s≤s; _≤_; _<_)
 open import Data.Nat.Properties using (≤-trans; n≤1+n)
-open import Data.Product as Prod using (∃; _×_; _,_ ; ∃₂; proj₁; proj₂)
+open import Data.Product.Base as Prod using (∃; _×_; _,_ ; ∃₂; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (_$_; flip; _∘_; _∘′_; id)
diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index ac88bd72ef..d48b3dae45 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -23,7 +23,7 @@ open import Data.List.Relation.Binary.Subset.Propositional.Properties
   using (⊆-preorder)
 open import Data.List.Relation.Binary.Permutation.Propositional
 open import Data.List.Relation.Binary.Permutation.Propositional.Properties
-open import Data.Product as Prod hiding (map)
+open import Data.Product.Base as Prod hiding (map)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum hiding (map)
 open import Data.Sum.Properties hiding (map-cong)
diff --git a/src/Data/List/Relation/Binary/Lex/NonStrict.agda b/src/Data/List/Relation/Binary/Lex/NonStrict.agda
index 4606c9cdbd..e87e1e0b45 100644
--- a/src/Data/List/Relation/Binary/Lex/NonStrict.agda
+++ b/src/Data/List/Relation/Binary/Lex/NonStrict.agda
@@ -14,7 +14,6 @@ module Data.List.Relation.Binary.Lex.NonStrict where
 open import Data.Empty using (⊥)
 open import Function.Base
 open import Data.Unit.Base using (⊤; tt)
-open import Data.Product
 open import Data.List.Base
 open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; [])
 import Data.List.Relation.Binary.Lex.Strict as Strict
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index dc7e34db86..42430b90ea 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -21,7 +21,7 @@ open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Membership.Propositional
 open import Data.List.Membership.Propositional.Properties
 import Data.List.Properties as Lₚ
-open import Data.Product using (_,_; _×_; ∃; ∃₂)
+open import Data.Product.Base using (_,_; _×_; ∃; ∃₂)
 open import Function.Base using (_∘_; _⟨_⟩_)
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Inverse as Inv using (inverse)
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index e7d2b4039c..57233a7b2a 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -32,7 +32,7 @@ import Data.List.Properties as Lₚ
 open import Data.Nat hiding (_⊔_)
 open import Data.Nat.Induction
 open import Data.Nat.Properties
-open import Data.Product using (_,_; _×_; ∃; ∃₂; proj₁; proj₂)
+open import Data.Product.Base using (_,_; _×_; ∃; ∃₂; proj₁; proj₂)
 open import Function.Base using (_∘_; _⟨_⟩_; flip)
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Inverse as Inv using (inverse)
diff --git a/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda b/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda
index 39d4439a86..75104bd39e 100644
--- a/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda
+++ b/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda
@@ -12,7 +12,7 @@ open import Level
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Binary.Pointwise
   using (Pointwise; []; _∷_)
-open import Data.Product using (∃; _×_; _,_; uncurry)
+open import Data.Product.Base using (∃; _×_; _,_; uncurry)
 open import Relation.Binary.Core using (REL; _⇒_)
 
 module _ {a b r} {A : Set a} {B : Set b} (R : REL A B r) where
diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
index 7e7a3a090d..46d5d7d2cc 100644
--- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
@@ -24,7 +24,7 @@ open import Data.List.Relation.Binary.Sublist.Heterogeneous
 open import Data.Maybe.Relation.Unary.All as MAll using (nothing; just)
 open import Data.Nat.Base using (ℕ; _≤_; _≥_); open ℕ; open _≤_
 import Data.Nat.Properties as ℕₚ
-open import Data.Product using (∃₂; _×_; _,_; <_,_>; proj₂; uncurry)
+open import Data.Product.Base using (∃₂; _×_; _,_; <_,_>; proj₂; uncurry)
 
 open import Function.Base
 open import Function.Bundles using (_⤖_; _⇔_ ; mk⤖; mk⇔)
diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda
index a7afe038c7..e7b95805be 100644
--- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda
@@ -23,7 +23,7 @@ open import Level using (_⊔_)
 open import Data.Fin as Fin
 open import Data.Maybe.Base as M
 open import Data.Nat.Base as Nat using (ℕ)
-open import Data.Product
+open import Data.Product.Base using (Σ-syntax; _,_)
 open import Data.Vec.Base as Vec using (Vec ; lookup)
 open import Data.List.Base hiding (lookup)
 open import Data.List.Properties
diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
index 844dd1c996..c9d2ea6724 100644
--- a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
@@ -19,7 +19,7 @@ open import Data.List.Relation.Binary.Sublist.Propositional
   hiding (map)
 import Data.List.Relation.Binary.Sublist.Setoid.Properties
   as SetoidProperties
-open import Data.Product using (∃; _,_; proj₂)
+open import Data.Product.Base using (∃; _,_; proj₂)
 open import Function.Base
 open import Level using (Level)
 open import Relation.Binary.Definitions using (_Respects_)
diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid.agda b/src/Data/List/Relation/Binary/Sublist/Setoid.agda
index eff26de0aa..a07c6ffc25 100644
--- a/src/Data/List/Relation/Binary/Sublist/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Setoid.agda
@@ -24,7 +24,7 @@ import Data.List.Relation.Binary.Sublist.Heterogeneous.Core
   as HeterogeneousCore
 import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
   as HeterogeneousProperties
-open import Data.Product using (∃; ∃₂; _×_; _,_; proj₂)
+open import Data.Product.Base using (∃; ∃₂; _×_; _,_; proj₂)
 
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
index df904a0452..19fe765456 100644
--- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
@@ -17,7 +17,7 @@ open import Data.List.Relation.Unary.Any using (Any)
 import Data.Maybe.Relation.Unary.All as Maybe
 open import Data.Nat.Base using (_≤_; _≥_)
 import Data.Nat.Properties as ℕₚ
-open import Data.Product using (∃; _,_; proj₂)
+open import Data.Product.Base using (∃; _,_; proj₂)
 open import Function.Base
 open import Function.Bundles using (_⇔_; _⤖_)
 open import Level
diff --git a/src/Data/List/Relation/Ternary/Appending.agda b/src/Data/List/Relation/Ternary/Appending.agda
index 1ae20e905f..1a2bab30e1 100644
--- a/src/Data/List/Relation/Ternary/Appending.agda
+++ b/src/Data/List/Relation/Ternary/Appending.agda
@@ -11,7 +11,7 @@ module Data.List.Relation.Ternary.Appending {a b c} {A : Set a} {B : Set b} {C :
 open import Level using (Level; _⊔_)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
-open import Data.Product as Prod using (∃₂; _×_; _,_; -,_)
+open import Data.Product.Base using (∃₂; _×_; _,_; -,_)
 open import Relation.Binary.Core using (REL)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
diff --git a/src/Data/List/Relation/Ternary/Interleaving.agda b/src/Data/List/Relation/Ternary/Interleaving.agda
index 158701fc7e..8818638518 100644
--- a/src/Data/List/Relation/Ternary/Interleaving.agda
+++ b/src/Data/List/Relation/Ternary/Interleaving.agda
@@ -12,7 +12,7 @@ module Data.List.Relation.Ternary.Interleaving where
 open import Level
 open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
-open import Data.Product as Prod using (∃; ∃₂; _×_; uncurry; _,_; -,_; proj₂)
+open import Data.Product.Base as Prod using (∃; ∃₂; _×_; uncurry; _,_; -,_; proj₂)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base
 open import Relation.Binary
diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index 6a0020d269..8f3bcd640c 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -25,7 +25,7 @@ open import Data.Nat using (zero; suc; _<_; z<s; s<s; s≤s)
 open import Data.Nat.Properties using (_≟_; ≤∧≢⇒<; ≤-refl; m<n⇒m<1+n)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.Any as MAny using (just)
-open import Data.Product as Prod
+open import Data.Product.Base as Prod
   using (_×_; _,_; ∃; ∃₂; proj₁; proj₂; uncurry′)
 open import Data.Product.Properties
 open import Data.Product.Function.NonDependent.Propositional
diff --git a/src/Data/List/Relation/Unary/First.agda b/src/Data/List/Relation/Unary/First.agda
index bfe8c761b0..25eb9fc37a 100644
--- a/src/Data/List/Relation/Unary/First.agda
+++ b/src/Data/List/Relation/Unary/First.agda
@@ -15,7 +15,7 @@ open import Data.Fin.Base as Fin using (Fin; zero; suc)
 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.Product.Base using (∃; -,_; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function.Base using (id; _∘′_)
 open import Relation.Unary
diff --git a/src/Data/Maybe/Relation/Binary/Connected.agda b/src/Data/Maybe/Relation/Binary/Connected.agda
index 33bff58154..5c509e50fd 100644
--- a/src/Data/Maybe/Relation/Binary/Connected.agda
+++ b/src/Data/Maybe/Relation/Binary/Connected.agda
@@ -9,7 +9,6 @@
 module Data.Maybe.Relation.Binary.Connected where
 
 open import Level
-open import Data.Product
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Relation.Binary hiding (_⇔_)
diff --git a/src/Data/Maybe/Relation/Binary/Pointwise.agda b/src/Data/Maybe/Relation/Binary/Pointwise.agda
index 3ae5ad421e..a9946a6ef3 100644
--- a/src/Data/Maybe/Relation/Binary/Pointwise.agda
+++ b/src/Data/Maybe/Relation/Binary/Pointwise.agda
@@ -9,7 +9,7 @@
 module Data.Maybe.Relation.Binary.Pointwise where
 
 open import Level
-open import Data.Product
+open import Data.Product.Base using (∃; _×_; -,_; _,_)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Relation.Binary hiding (_⇔_)
diff --git a/src/Data/Maybe/Relation/Unary/Any.agda b/src/Data/Maybe/Relation/Unary/Any.agda
index ea81316c77..48cd402ce0 100644
--- a/src/Data/Maybe/Relation/Unary/Any.agda
+++ b/src/Data/Maybe/Relation/Unary/Any.agda
@@ -9,7 +9,7 @@
 module Data.Maybe.Relation.Unary.Any where
 
 open import Data.Maybe.Base using (Maybe; just; nothing)
-open import Data.Product as Prod using (∃; _,_; -,_)
+open import Data.Product.Base as Prod using (∃; _,_; -,_)
 open import Function.Base using (id)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level
diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda
index 2294a08968..43496f3139 100644
--- a/src/Data/Nat/Binary/Properties.agda
+++ b/src/Data/Nat/Binary/Properties.agda
@@ -21,7 +21,7 @@ open import Data.Nat.Divisibility using (∣-refl)
 import Data.Nat.Base as ℕᵇ
 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 using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; _$_; id)
 open import Function.Definitions
diff --git a/src/Data/Nat/Binary/Subtraction.agda b/src/Data/Nat/Binary/Subtraction.agda
index 5dc7c8951f..48eb4b4ae7 100644
--- a/src/Data/Nat/Binary/Subtraction.agda
+++ b/src/Data/Nat/Binary/Subtraction.agda
@@ -16,7 +16,7 @@ open import Data.Nat as ℕ using (ℕ)
 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.Product.Base using (_×_; _,_; proj₁; proj₂; ∃)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Vec.Base using ([]; _∷_)
 open import Function.Base using (_∘_; _$_)
diff --git a/src/Data/Nat/GCD.agda b/src/Data/Nat/GCD.agda
index e702c512a6..f54b09e47f 100644
--- a/src/Data/Nat/GCD.agda
+++ b/src/Data/Nat/GCD.agda
@@ -15,7 +15,8 @@ open import Data.Nat.GCD.Lemmas
 open import Data.Nat.Properties
 open import Data.Nat.Induction
   using (Acc; acc; <′-Rec; <′-recBuilder; <-wellFounded-fast)
-open import Data.Product
+open import Data.Product.Base
+  using (_×_; _,_; proj₂; proj₁; swap; uncurry′; ∃; map)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_$_; _∘_)
 open import Induction using (build)
diff --git a/src/Data/Nat/InfinitelyOften.agda b/src/Data/Nat/InfinitelyOften.agda
index 9e89841633..f85ceb196a 100644
--- a/src/Data/Nat/InfinitelyOften.agda
+++ b/src/Data/Nat/InfinitelyOften.agda
@@ -13,7 +13,7 @@ open import Level using (Level; 0ℓ)
 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.Product.Base as Prod hiding (map)
 open import Data.Sum.Base using (inj₁; inj₂; _⊎_)
 open import Function.Base using (_∘_; id)
 open import Relation.Binary.PropositionalEquality
diff --git a/src/Data/Nat/LCM.agda b/src/Data/Nat/LCM.agda
index af85ed64ad..ccb1fbbf5b 100644
--- a/src/Data/Nat/LCM.agda
+++ b/src/Data/Nat/LCM.agda
@@ -15,7 +15,7 @@ open import Data.Nat.Divisibility
 open import Data.Nat.DivMod
 open import Data.Nat.Properties
 open import Data.Nat.GCD
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_; uncurry′; ∃)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)
diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda
index 6ed6997c0b..8e72b32be0 100644
--- a/src/Data/Nat/Primality.agda
+++ b/src/Data/Nat/Primality.agda
@@ -13,7 +13,7 @@ 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.Properties
-open import Data.Product
+open import Data.Product.Base using (∃; _×_; map₂; _,_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (flip; _∘_; _∘′_)
 open import Relation.Nullary.Decidable as Dec
diff --git a/src/Data/Product/Effectful/Examples.agda b/src/Data/Product/Effectful/Examples.agda
index f11631341e..b4cc86618e 100644
--- a/src/Data/Product/Effectful/Examples.agda
+++ b/src/Data/Product/Effectful/Examples.agda
@@ -14,7 +14,7 @@ module Data.Product.Effectful.Examples
 open import Level using (Lift; lift; _⊔_)
 open import Effect.Functor using (RawFunctor)
 open import Effect.Monad using (RawMonad)
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Function.Base using (id)
 import Function.Identity.Effectful as Id
diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda
index d062e33d39..abae430992 100644
--- a/src/Data/Product/Function/Dependent/Propositional.agda
+++ b/src/Data/Product/Function/Dependent/Propositional.agda
@@ -9,7 +9,7 @@
 
 module Data.Product.Function.Dependent.Propositional where
 
-open import Data.Product
+open import Data.Product.Base using (Σ; map; _,_)
 open import Data.Product.Function.NonDependent.Setoid
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Relation.Binary hiding (_⇔_)
diff --git a/src/Data/Product/Function/Dependent/Propositional/WithK.agda b/src/Data/Product/Function/Dependent/Propositional/WithK.agda
index 0b3838e12f..df3bafe613 100644
--- a/src/Data/Product/Function/Dependent/Propositional/WithK.agda
+++ b/src/Data/Product/Function/Dependent/Propositional/WithK.agda
@@ -9,7 +9,7 @@
 
 module Data.Product.Function.Dependent.Propositional.WithK where
 
-open import Data.Product
+open import Data.Product.Base using (Σ)
 open import Data.Product.Function.Dependent.Setoid
 open import Data.Product.Relation.Binary.Pointwise.Dependent
 open import Data.Product.Relation.Binary.Pointwise.Dependent.WithK
diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda
index cc6d4a12fc..22f3f7937a 100644
--- a/src/Data/Product/Function/Dependent/Setoid.agda
+++ b/src/Data/Product/Function/Dependent/Setoid.agda
@@ -9,7 +9,7 @@
 
 module Data.Product.Function.Dependent.Setoid where
 
-open import Data.Product
+open import Data.Product.Base using (map; _,_)
 open import Data.Product.Relation.Binary.Pointwise.Dependent
 open import Function.Base
 open import Function.Equality as F using (_⟶_; _⟨$⟩_)
diff --git a/src/Data/Product/Function/Dependent/Setoid/WithK.agda b/src/Data/Product/Function/Dependent/Setoid/WithK.agda
index c9468fb939..7362b3ade0 100644
--- a/src/Data/Product/Function/Dependent/Setoid/WithK.agda
+++ b/src/Data/Product/Function/Dependent/Setoid/WithK.agda
@@ -9,7 +9,7 @@
 
 module Data.Product.Function.Dependent.Setoid.WithK where
 
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Data.Product.Function.Dependent.Setoid using (surjection)
 open import Data.Product.Relation.Binary.Pointwise.Dependent
 open import Relation.Binary
diff --git a/src/Data/Product/Function/NonDependent/Propositional.agda b/src/Data/Product/Function/NonDependent/Propositional.agda
index e686cbad6e..b4c9501304 100644
--- a/src/Data/Product/Function/NonDependent/Propositional.agda
+++ b/src/Data/Product/Function/NonDependent/Propositional.agda
@@ -9,7 +9,7 @@
 
 module Data.Product.Function.NonDependent.Propositional where
 
-open import Data.Product
+open import Data.Product.Base using (_×_; map)
 open import Data.Product.Function.NonDependent.Setoid
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Relation.Binary hiding (_⇔_)
diff --git a/src/Data/Product/Function/NonDependent/Setoid.agda b/src/Data/Product/Function/NonDependent/Setoid.agda
index eb1a369710..93e388da23 100644
--- a/src/Data/Product/Function/NonDependent/Setoid.agda
+++ b/src/Data/Product/Function/NonDependent/Setoid.agda
@@ -9,7 +9,7 @@
 
 module Data.Product.Function.NonDependent.Setoid where
 
-open import Data.Product
+open import Data.Product.Base using (map; _,_; <_,_>; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Relation.Binary
 open import Function.Equality as F using (_⟶_; _⟨$⟩_)
diff --git a/src/Data/Product/Instances.agda b/src/Data/Product/Instances.agda
index 222a254b0b..93794c3c58 100644
--- a/src/Data/Product/Instances.agda
+++ b/src/Data/Product/Instances.agda
@@ -8,7 +8,7 @@
 
 module Data.Product.Instances where
 
-open import Data.Product
+open import Data.Product.Base
   using (Σ)
 open import Data.Product.Properties
 open import Level
diff --git a/src/Data/Product/Properties/WithK.agda b/src/Data/Product/Properties/WithK.agda
index 645ea6a6c4..329cdaf675 100644
--- a/src/Data/Product/Properties/WithK.agda
+++ b/src/Data/Product/Properties/WithK.agda
@@ -8,7 +8,7 @@
 
 module Data.Product.Properties.WithK where
 
-open import Data.Product
+open import Data.Product.Base using (Σ; _,_)
 open import Function.Base using (_∋_)
 open import Relation.Binary.PropositionalEquality
 
diff --git a/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda b/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda
index 7fce761f79..d388b14f91 100644
--- a/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda
+++ b/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda
@@ -9,7 +9,7 @@
 
 module Data.Product.Relation.Binary.Pointwise.Dependent.WithK where
 
-open import Data.Product
+open import Data.Product.Base using (Σ; uncurry)
 open import Data.Product.Relation.Binary.Pointwise.Dependent
 open import Function.Base
 open import Function.Inverse using (Inverse)
diff --git a/src/Data/Sum/Relation/Binary/LeftOrder.agda b/src/Data/Sum/Relation/Binary/LeftOrder.agda
index 2d23693e2d..1ff3b18d05 100644
--- a/src/Data/Sum/Relation/Binary/LeftOrder.agda
+++ b/src/Data/Sum/Relation/Binary/LeftOrder.agda
@@ -11,7 +11,7 @@ module Data.Sum.Relation.Binary.LeftOrder where
 open import Data.Sum.Base as Sum
 open import Data.Sum.Relation.Binary.Pointwise as PW
   using (Pointwise; inj₁; inj₂)
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Data.Empty
 open import Function.Base using (_$_; _∘_)
 open import Level
diff --git a/src/Data/These/Properties.agda b/src/Data/These/Properties.agda
index a6c96a3208..e7111cfce1 100644
--- a/src/Data/These/Properties.agda
+++ b/src/Data/These/Properties.agda
@@ -8,7 +8,7 @@
 
 module Data.These.Properties where
 
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_; <_,_>; uncurry)
 open import Data.These.Base
 open import Function.Base using (_∘_)
 open import Relation.Binary.Definitions using (Decidable)
diff --git a/src/Data/Tree/AVL/Indexed.agda b/src/Data/Tree/AVL/Indexed.agda
index c322d680e3..94d1b0782b 100644
--- a/src/Data/Tree/AVL/Indexed.agda
+++ b/src/Data/Tree/AVL/Indexed.agda
@@ -13,7 +13,7 @@ module Data.Tree.AVL.Indexed
 
 open import Level using (Level; _⊔_)
 open import Data.Nat.Base using (ℕ; zero; suc; _+_)
-open import Data.Product using (Σ; ∃; _×_; _,_; proj₁)
+open import Data.Product.Base using (Σ; ∃; _×_; _,_; proj₁)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.List.Base as List using (List)
 open import Data.DifferenceList using (DiffList; []; _∷_; _++_)
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
index 2710a373b5..f8c270f1a1 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
@@ -13,7 +13,7 @@ module Data.Tree.AVL.Indexed.Relation.Unary.Any
   where
 
 open import Data.Nat.Base using (ℕ)
-open import Data.Product using (_,_; ∃; -,_; proj₁; proj₂)
+open import Data.Product.Base using (_,_; ∃; -,_; proj₁; proj₂)
 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/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index 9f4aa1aeca..02a09a098e 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -16,7 +16,7 @@ open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′)
 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.Product.Base as Prod using (∃; ∃-syntax; _×_; _,_; proj₁; proj₂)
 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/Indexed/WithK.agda b/src/Data/Tree/AVL/Indexed/WithK.agda
index 7467a3813f..169427e986 100644
--- a/src/Data/Tree/AVL/Indexed/WithK.agda
+++ b/src/Data/Tree/AVL/Indexed/WithK.agda
@@ -15,7 +15,6 @@ module Data.Tree.AVL.Indexed.WithK
 
 strictTotalOrder = record { isStrictTotalOrder = isStrictTotalOrder }
 
-open import Data.Product
 open import Data.Tree.AVL.Indexed strictTotalOrder as AVL hiding (Value)
 
 module _ {v} {V′ : Key → Set v} where
diff --git a/src/Data/Tree/AVL/IndexedMap.agda b/src/Data/Tree/AVL/IndexedMap.agda
index cb16cd6220..7b46f3391a 100644
--- a/src/Data/Tree/AVL/IndexedMap.agda
+++ b/src/Data/Tree/AVL/IndexedMap.agda
@@ -6,7 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.Product as Prod
+open import Data.Product.Base
+  using (map₁; map₂; ∃; _×_; Σ-syntax; proj₁; _,_; -,_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst)
 import Data.Tree.AVL.Value
@@ -76,10 +77,10 @@ member : ∀ {i} → Key i → Map → Bool
 member k = AVL.member (-, k)
 
 headTail : Map → Maybe (KV × Map)
-headTail m = Maybe.map (Prod.map₁ (toKV ∘′ AVL.toPair)) (AVL.headTail m)
+headTail m = Maybe.map (map₁ (toKV ∘′ AVL.toPair)) (AVL.headTail m)
 
 initLast : Map → Maybe (Map × KV)
-initLast m = Maybe.map (Prod.map₂ (toKV ∘′ AVL.toPair)) (AVL.initLast m)
+initLast m = Maybe.map (map₂ (toKV ∘′ AVL.toPair)) (AVL.initLast m)
 
 foldr : (∀ {k} → Value k → A → A) → A → Map → A
 foldr cons = AVL.foldr cons
diff --git a/src/Data/Tree/AVL/Key.agda b/src/Data/Tree/AVL/Key.agda
index dd41ffb9fd..5c47ccbacc 100644
--- a/src/Data/Tree/AVL/Key.agda
+++ b/src/Data/Tree/AVL/Key.agda
@@ -16,7 +16,7 @@ module Data.Tree.AVL.Key
 open import Level
 open import Data.Empty
 open import Data.Unit
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_ ; refl)
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Construct.Add.Extrema
diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional.agda b/src/Data/Tree/AVL/Map/Membership/Propositional.agda
index 0873c66cd2..0a3ecd2337 100644
--- a/src/Data/Tree/AVL/Map/Membership/Propositional.agda
+++ b/src/Data/Tree/AVL/Map/Membership/Propositional.agda
@@ -15,7 +15,7 @@ module Data.Tree.AVL.Map.Membership.Propositional
 
 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.Base using (_×_; ∃-syntax; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent renaming (Pointwise to _×ᴿ_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; _∘′_)
diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
index aef88a23d7..64eb574b04 100644
--- a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
+++ b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
@@ -15,7 +15,7 @@ module Data.Tree.AVL.Map.Membership.Propositional.Properties
 
 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.Base as Prod using (_×_; ∃-syntax; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent renaming (Pointwise to _×ᴿ_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; _∘′_)
diff --git a/src/Data/Tree/AVL/Map/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Map/Relation/Unary/Any.agda
index 8a347bd5ff..5ad457d54f 100644
--- a/src/Data/Tree/AVL/Map/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Map/Relation/Unary/Any.agda
@@ -12,7 +12,7 @@ module Data.Tree.AVL.Map.Relation.Unary.Any
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
   where
 
-open import Data.Product as Prod using (_×_; ∃; _,_)
+open import Data.Product.Base as Prod using (_×_; ∃; _,_)
 open import Function.Base using (_∘_; _∘′_; id)
 open import Level using (Level; _⊔_)
 
diff --git a/src/Data/Tree/AVL/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Relation/Unary/Any.agda
index a9429d4ed2..dfa96935ac 100644
--- a/src/Data/Tree/AVL/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Relation/Unary/Any.agda
@@ -12,7 +12,7 @@ module Data.Tree.AVL.Relation.Unary.Any
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
   where
 
-open import Data.Product as Prod using (∃)
+open import Data.Product.Base as Prod using (∃)
 open import Function.Base using (_∘_; _$_)
 open import Level using (Level; _⊔_)
 
diff --git a/src/Data/Trie.agda b/src/Data/Trie.agda
index 694d7afe7b..3c2de5daf1 100644
--- a/src/Data/Trie.agda
+++ b/src/Data/Trie.agda
@@ -19,7 +19,7 @@ open import Size
 open import Data.List.Base using (List; []; _∷_; _++_)
 import Data.List.NonEmpty as List⁺
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing; maybe′)
-open import Data.Product as Prod using (∃)
+open import Data.Product.Base using (∃)
 open import Data.These.Base as These using (These)
 open import Function.Base using (_∘′_; const)
 open import Relation.Unary using (IUniversal; _⇒_)
diff --git a/src/Data/Trie/NonEmpty.agda b/src/Data/Trie/NonEmpty.agda
index 96378d25e6..f32d20d92f 100644
--- a/src/Data/Trie/NonEmpty.agda
+++ b/src/Data/Trie/NonEmpty.agda
@@ -13,7 +13,7 @@ module Data.Trie.NonEmpty {k e r} (S : StrictTotalOrder k e r) where
 open import Level
 open import Size
 open import Effect.Monad
-open import Data.Product as Prod using (∃; uncurry; -,_)
+open import Data.Product.Base as Prod using (∃; uncurry; -,_)
 open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; [_]; concatMap)
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′) hiding (module Maybe)
diff --git a/src/Data/Universe.agda b/src/Data/Universe.agda
index 516e0bd2a4..9bbfb4620b 100644
--- a/src/Data/Universe.agda
+++ b/src/Data/Universe.agda
@@ -8,7 +8,6 @@
 
 module Data.Universe where
 
-open import Data.Product
 open import Level
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Universe/Indexed.agda b/src/Data/Universe/Indexed.agda
index cb6d9f4e56..9807e38eb5 100644
--- a/src/Data/Universe/Indexed.agda
+++ b/src/Data/Universe/Indexed.agda
@@ -8,7 +8,7 @@
 
 module Data.Universe.Indexed where
 
-open import Data.Product
+open import Data.Product.Base using (∃; proj₂)
 open import Data.Universe
 open import Function.Base using (_∘_)
 open import Level
diff --git a/src/Data/Vec/Functional/Relation/Unary/Any.agda b/src/Data/Vec/Functional/Relation/Unary/Any.agda
index de6c3570cb..f41295bf04 100644
--- a/src/Data/Vec/Functional/Relation/Unary/Any.agda
+++ b/src/Data/Vec/Functional/Relation/Unary/Any.agda
@@ -11,7 +11,7 @@ module Data.Vec.Functional.Relation.Unary.Any where
 open import Data.Fin.Base using (zero; suc)
 open import Data.Fin.Properties using (any?)
 open import Data.Nat.Base
-open import Data.Product as Σ using (Σ; ∃; _×_; _,_; proj₁; proj₂)
+open import Data.Product.Base as Σ using (Σ; ∃; _×_; _,_; proj₁; proj₂)
 open import Data.Vec.Functional as VF hiding (map)
 open import Function.Base using (id)
 open import Level using (Level)
diff --git a/src/Data/Vec/Membership/Propositional/Properties.agda b/src/Data/Vec/Membership/Propositional/Properties.agda
index f4722c9899..205622c17a 100644
--- a/src/Data/Vec/Membership/Propositional/Properties.agda
+++ b/src/Data/Vec/Membership/Propositional/Properties.agda
@@ -9,7 +9,7 @@
 module Data.Vec.Membership.Propositional.Properties where
 
 open import Data.Fin.Base using (Fin; zero; suc)
-open import Data.Product as Prod using (_,_; ∃; _×_; -,_)
+open import Data.Product.Base using (_,_; ∃; _×_; -,_; map₁; map₂)
 open import Data.Vec.Base
 open import Data.Vec.Relation.Unary.Any using (here; there)
 open import Data.List.Base using ([]; _∷_)
@@ -109,7 +109,7 @@ module _ {P : Pred A p} where
 
   fromAny : ∀ {n} {xs : Vec A n} → Any P xs → ∃ λ x → x ∈ xs × P x
   fromAny (here px) = -, here refl , px
-  fromAny (there v) = Prod.map₂ (Prod.map₁ there) (fromAny v)
+  fromAny (there v) = map₂ (map₁ there) (fromAny v)
 
   toAny : ∀ {n x} {xs : Vec A n} → x ∈ xs → P x → Any P xs
   toAny (here refl) px = here px
diff --git a/src/Data/Vec/Membership/Setoid.agda b/src/Data/Vec/Membership/Setoid.agda
index 57476d5f35..72e57e15f3 100644
--- a/src/Data/Vec/Membership/Setoid.agda
+++ b/src/Data/Vec/Membership/Setoid.agda
@@ -15,7 +15,7 @@ open import Function.Base using (_∘_; flip)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Data.Vec.Relation.Unary.Any as Any
   using (Any; here; there; index)
-open import Data.Product using (∃; _×_; _,_)
+open import Data.Product.Base using (∃; _×_; _,_)
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Unary using (Pred)
 
diff --git a/src/Data/Vec/Recursive/Properties.agda b/src/Data/Vec/Recursive/Properties.agda
index 7a6a6e960b..85fa8e44e6 100644
--- a/src/Data/Vec/Recursive/Properties.agda
+++ b/src/Data/Vec/Recursive/Properties.agda
@@ -10,7 +10,7 @@ module Data.Vec.Recursive.Properties where
 
 open import Level using (Level)
 open import Data.Nat.Base hiding (_^_)
-open import Data.Product
+open import Data.Product.Base
 open import Data.Vec.Recursive
 open import Data.Vec.Base using (Vec; _∷_)
 open import Function.Bundles using (_↔_; mk↔′)
diff --git a/src/Data/Vec/Relation/Unary/Any.agda b/src/Data/Vec/Relation/Unary/Any.agda
index dcf142bcd6..de901fe571 100644
--- a/src/Data/Vec/Relation/Unary/Any.agda
+++ b/src/Data/Vec/Relation/Unary/Any.agda
@@ -13,7 +13,7 @@ open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Nat.Base using (ℕ; zero; suc; NonZero)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Vec.Base as Vec using (Vec; []; [_]; _∷_)
-open import Data.Product as Prod using (∃; _,_)
+open import Data.Product.Base as Prod using (∃; _,_)
 open import Level using (Level; _⊔_)
 open import Relation.Nullary.Negation using (¬_; contradiction)
 open import Relation.Nullary.Decidable as Dec using (yes; no; _⊎-dec_)
diff --git a/src/Data/Vec/Relation/Unary/Any/Properties.agda b/src/Data/Vec/Relation/Unary/Any/Properties.agda
index fd6455da55..96f8874bd7 100644
--- a/src/Data/Vec/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Any/Properties.agda
@@ -15,7 +15,7 @@ open import Data.List.Base using ([]; _∷_)
 import Data.List.Relation.Unary.Any as List
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Sum.Function.Propositional using (_⊎-cong_)
-open import Data.Product as Prod using (∃; ∃₂; _×_; _,_; proj₁; proj₂)
+open import Data.Product.Base as Prod using (∃; ∃₂; _×_; _,_; proj₁; proj₂)
 open import Data.Vec.Base hiding (here; there)
 open import Data.Vec.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.Vec.Membership.Propositional
diff --git a/src/Data/W/Indexed.agda b/src/Data/W/Indexed.agda
index b356a22533..fbf3910427 100644
--- a/src/Data/W/Indexed.agda
+++ b/src/Data/W/Indexed.agda
@@ -10,7 +10,7 @@ module Data.W.Indexed where
 
 open import Level
 open import Data.Container.Indexed.Core
-open import Data.Product
+open import Data.Product.Base using (_,_; Σ)
 open import Relation.Unary
 
 -- The family of indexed W-types.
diff --git a/src/Data/W/WithK.agda b/src/Data/W/WithK.agda
index 0646bfb315..e88fb7cda5 100644
--- a/src/Data/W/WithK.agda
+++ b/src/Data/W/WithK.agda
@@ -8,7 +8,7 @@
 
 module Data.W.WithK where
 
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Data.Container.Core
 open import Data.W
 open import Agda.Builtin.Equality
diff --git a/src/Effect/Applicative/Predicate.agda b/src/Effect/Applicative/Predicate.agda
index bcfec53170..5d696b37b2 100644
--- a/src/Effect/Applicative/Predicate.agda
+++ b/src/Effect/Applicative/Predicate.agda
@@ -12,7 +12,7 @@
 module Effect.Applicative.Predicate where
 
 open import Effect.Functor.Predicate
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Function.Base using (const; constᵣ)
 open import Level
 open import Relation.Unary
diff --git a/src/Effect/Monad/Predicate.agda b/src/Effect/Monad/Predicate.agda
index df3e58347c..1210de7959 100644
--- a/src/Effect/Monad/Predicate.agda
+++ b/src/Effect/Monad/Predicate.agda
@@ -14,7 +14,7 @@ open import Effect.Applicative.Indexed
 open import Effect.Monad
 open import Effect.Monad.Indexed
 open import Data.Unit
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Function.Base using (const; id; _∘_)
 open import Level
 open import Relation.Binary.PropositionalEquality
diff --git a/src/Effect/Monad/State.agda b/src/Effect/Monad/State.agda
index 222f6e7f48..41fc3336d8 100644
--- a/src/Effect/Monad/State.agda
+++ b/src/Effect/Monad/State.agda
@@ -9,7 +9,7 @@
 
 module Effect.Monad.State where
 
-open import Data.Product
+open import Data.Product.Base using (_×_)
 open import Effect.Choice
 open import Effect.Empty
 open import Effect.Functor
diff --git a/src/Effect/Monad/State/Indexed.agda b/src/Effect/Monad/State/Indexed.agda
index 1fc27655d8..4150554ac9 100644
--- a/src/Effect/Monad/State/Indexed.agda
+++ b/src/Effect/Monad/State/Indexed.agda
@@ -12,7 +12,7 @@ open import Effect.Applicative.Indexed
 open import Effect.Monad
 open import Function.Identity.Effectful as Id using (Identity)
 open import Effect.Monad.Indexed
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_; uncurry)
 open import Data.Unit
 open import Function.Base
 open import Level
diff --git a/src/Foreign/Haskell/Coerce.agda b/src/Foreign/Haskell/Coerce.agda
index f593d10af3..3eb411c325 100644
--- a/src/Foreign/Haskell/Coerce.agda
+++ b/src/Foreign/Haskell/Coerce.agda
@@ -39,7 +39,7 @@ import IO.Primitive            as STD
 import Data.List.Base          as STD
 import Data.List.NonEmpty.Base as STD
 import Data.Maybe.Base         as STD
-import Data.Product            as STD
+import Data.Product.Base       as STD
 import Data.Sum.Base           as STD
 
 import Foreign.Haskell.Pair          as FFI
diff --git a/src/Foreign/Haskell/Pair.agda b/src/Foreign/Haskell/Pair.agda
index 1f10b05169..84d4b8180b 100644
--- a/src/Foreign/Haskell/Pair.agda
+++ b/src/Foreign/Haskell/Pair.agda
@@ -9,7 +9,7 @@
 module Foreign.Haskell.Pair where
 
 open import Level
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 
 private
   variable
diff --git a/src/Function/Bijection.agda b/src/Function/Bijection.agda
index 1de607e957..8c7ce78ef3 100644
--- a/src/Function/Bijection.agda
+++ b/src/Function/Bijection.agda
@@ -13,7 +13,6 @@
 
 module Function.Bijection where
 
-open import Data.Product
 open import Level
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P
diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda
index b02976db88..9d7974294c 100644
--- a/src/Function/Endomorphism/Setoid.agda
+++ b/src/Function/Endomorphism/Setoid.agda
@@ -21,7 +21,7 @@ open import Algebra.Morphism; open Definitions
 open import Function.Equality
 open import Data.Nat.Base using (ℕ; _+_); open ℕ
 open import Data.Nat.Properties
-open import Data.Product
+open import Data.Product.Base using (_,_)
 
 import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial as Trivial
 
diff --git a/src/Function/LeftInverse.agda b/src/Function/LeftInverse.agda
index f06fbc6c8a..23f9b4a900 100644
--- a/src/Function/LeftInverse.agda
+++ b/src/Function/LeftInverse.agda
@@ -13,7 +13,6 @@
 
 module Function.LeftInverse where
 
-open import Data.Product
 open import Level
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 open import Relation.Binary
diff --git a/src/Function/Properties/RightInverse.agda b/src/Function/Properties/RightInverse.agda
index 531b7236e7..681e3e2b5a 100644
--- a/src/Function/Properties/RightInverse.agda
+++ b/src/Function/Properties/RightInverse.agda
@@ -12,7 +12,7 @@ open import Function.Base
 open import Function.Bundles
 open import Function.Consequences using (inverseˡ⇒surjective)
 open import Level using (Level)
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence)
 
diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda
index fce294be76..e0fccc598b 100644
--- a/src/Function/Properties/Surjection.agda
+++ b/src/Function/Properties/Surjection.agda
@@ -12,7 +12,7 @@ open import Function.Base
 open import Function.Definitions
 open import Function.Bundles
 open import Level using (Level)
-open import Data.Product
+open import Data.Product.Base using (proj₁; proj₂)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary using (Setoid)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda
index 58cf6bab88..9922c69fcf 100644
--- a/src/Function/Related/TypeIsomorphisms.agda
+++ b/src/Function/Related/TypeIsomorphisms.agda
@@ -15,7 +15,8 @@ open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Data.Bool.Base using (true; false)
 open import Data.Empty using (⊥-elim)
 open import Data.Empty.Polymorphic using (⊥) renaming (⊥-elim to ⊥ₚ-elim)
-open import Data.Product as Prod hiding (swap)
+open import Data.Product.Base as Prod
+  using (_×_; Σ; curry; uncurry; _,_; -,_; <_,_>; proj₁; proj₂; ∃₂; ∃)
 open import Data.Product.Function.NonDependent.Propositional
 open import Data.Sum.Base as Sum
 open import Data.Sum.Properties using (swap-involutive)
diff --git a/src/Function/Surjection.agda b/src/Function/Surjection.agda
index 12f4490f3e..6861979551 100644
--- a/src/Function/Surjection.agda
+++ b/src/Function/Surjection.agda
@@ -19,7 +19,6 @@ open import Function.Equality as F
 open import Function.Equivalence using (Equivalence)
 open import Function.Injection           hiding (id; _∘_; injection)
 open import Function.LeftInverse as Left hiding (id; _∘_)
-open import Data.Product
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
diff --git a/src/Induction/Lexicographic.agda b/src/Induction/Lexicographic.agda
index 303f2c8dfa..6acd96b7f1 100644
--- a/src/Induction/Lexicographic.agda
+++ b/src/Induction/Lexicographic.agda
@@ -8,7 +8,7 @@
 
 module Induction.Lexicographic where
 
-open import Data.Product
+open import Data.Product.Base using (Σ; _,_; _×_)
 open import Induction
 open import Level
 
diff --git a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
index 80a0727fc1..e4c8f3a974 100644
--- a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
+++ b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
@@ -15,7 +15,7 @@ module Relation.Binary.Construct.Add.Infimum.Strict
   {a ℓ} {A : Set a} (_<_ : Rel A ℓ) where
 
 open import Level using (_⊔_)
-open import Data.Product
+open import Data.Product.Base using (_,_; map)
 open import Function.Base
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl)
diff --git a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
index 0bbefc05fa..b09432961d 100644
--- a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
+++ b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
@@ -15,7 +15,7 @@ module Relation.Binary.Construct.Add.Supremum.Strict
   {a r} {A : Set a} (_<_ : Rel A r) where
 
 open import Level using (_⊔_)
-open import Data.Product
+open import Data.Product.Base using (_,_; map)
 open import Function.Base
 open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec
diff --git a/src/Relation/Binary/Construct/Composition.agda b/src/Relation/Binary/Construct/Composition.agda
index e34550fb58..7f8ba241b0 100644
--- a/src/Relation/Binary/Construct/Composition.agda
+++ b/src/Relation/Binary/Construct/Composition.agda
@@ -8,7 +8,7 @@
 
 module Relation.Binary.Construct.Composition where
 
-open import Data.Product
+open import Data.Product.Base using (∃; _×_; _,_)
 open import Function.Base
 open import Level
 open import Relation.Binary
diff --git a/src/Relation/Binary/Construct/Flip/Ord.agda b/src/Relation/Binary/Construct/Flip/Ord.agda
index ecfc4b6df4..4a2eea690f 100644
--- a/src/Relation/Binary/Construct/Flip/Ord.agda
+++ b/src/Relation/Binary/Construct/Flip/Ord.agda
@@ -12,7 +12,7 @@ open import Relation.Binary
 
 module Relation.Binary.Construct.Flip.Ord where
 
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Function.Base using (flip; _∘_)
 open import Level using (Level)
 
diff --git a/src/Relation/Binary/Construct/FromPred.agda b/src/Relation/Binary/Construct/FromPred.agda
index c95f95fb6f..e08997b9a7 100644
--- a/src/Relation/Binary/Construct/FromPred.agda
+++ b/src/Relation/Binary/Construct/FromPred.agda
@@ -16,7 +16,6 @@ module Relation.Binary.Construct.FromPred
   where
 
 open import Function.Base
-open import Data.Product
 
 open module Eq = Setoid S using (_≈_) renaming (Carrier to A)
 
diff --git a/src/Relation/Binary/Construct/FromRel.agda b/src/Relation/Binary/Construct/FromRel.agda
index fb842b7810..13fc1774c7 100644
--- a/src/Relation/Binary/Construct/FromRel.agda
+++ b/src/Relation/Binary/Construct/FromRel.agda
@@ -15,7 +15,6 @@ module Relation.Binary.Construct.FromRel
   {a r} {A : Set a} (_R_ : REL A (Carrier S) r) -- The relation
   where
 
-open import Data.Product
 open import Function.Base
 open import Level using (_⊔_)
 
diff --git a/src/Relation/Binary/Construct/On.agda b/src/Relation/Binary/Construct/On.agda
index 5206276f95..122b0d6584 100644
--- a/src/Relation/Binary/Construct/On.agda
+++ b/src/Relation/Binary/Construct/On.agda
@@ -8,7 +8,7 @@
 
 module Relation.Binary.Construct.On where
 
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_on_; _∘_)
 open import Induction.WellFounded using (WellFounded; Acc; acc)
 open import Level using (Level)
diff --git a/src/Relation/Binary/HeterogeneousEquality.agda b/src/Relation/Binary/HeterogeneousEquality.agda
index 1ca855e122..3152bbf0cb 100644
--- a/src/Relation/Binary/HeterogeneousEquality.agda
+++ b/src/Relation/Binary/HeterogeneousEquality.agda
@@ -9,7 +9,6 @@
 module Relation.Binary.HeterogeneousEquality where
 
 import Axiom.Extensionality.Heterogeneous as Ext
-open import Data.Product
 open import Data.Unit.NonEta
 open import Function.Base
 open import Function.Inverse using (Inverse)
diff --git a/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda b/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda
index d2825a3548..2dbd39344a 100644
--- a/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda
+++ b/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda
@@ -15,7 +15,7 @@ open import Relation.Binary.HeterogeneousEquality hiding (isEquivalence)
 import Relation.Binary.PropositionalEquality.Core as ≡
 open import Data.Nat.Base
 open import Data.Nat.Properties
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_)
 open import Function.Base
 
 open ≅-Reasoning
diff --git a/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda b/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda
index b75cfa7093..a86918081f 100644
--- a/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda
+++ b/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda
@@ -16,7 +16,7 @@ open BoundedJoinSemilattice J
 open import Algebra.Definitions _≈_
 open import Algebra.Ordered.Structures using (IsCommutativePomonoid)
 open import Algebra.Ordered.Bundles using (CommutativePomonoid)
-open import Data.Product
+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/Lattice/Properties/BoundedMeetSemilattice.agda b/src/Relation/Binary/Lattice/Properties/BoundedMeetSemilattice.agda
index b6c7be5a5c..622c8b6b0c 100644
--- a/src/Relation/Binary/Lattice/Properties/BoundedMeetSemilattice.agda
+++ b/src/Relation/Binary/Lattice/Properties/BoundedMeetSemilattice.agda
@@ -14,7 +14,6 @@ module Relation.Binary.Lattice.Properties.BoundedMeetSemilattice
 open BoundedMeetSemilattice M
 
 open import Algebra.Definitions _≈_
-open import Data.Product
 open import Function.Base using (_∘_; flip)
 open import Relation.Binary
 open import Relation.Binary.Properties.Poset poset
diff --git a/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda b/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda
index fb85a17fe0..faa51120cd 100644
--- a/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda
+++ b/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda
@@ -18,7 +18,7 @@ import Algebra.Structures as Alg
 open import Algebra.Definitions _≈_
 open import Algebra.Ordered.Structures using (IsPosemigroup)
 open import Algebra.Ordered.Bundles using (Posemigroup)
-open import Data.Product
+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/Lattice/Properties/MeetSemilattice.agda b/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda
index 34e4252f92..f072cb2199 100644
--- a/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda
+++ b/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda
@@ -14,7 +14,6 @@ module Relation.Binary.Lattice.Properties.MeetSemilattice
 open MeetSemilattice M
 
 open import Algebra.Definitions _≈_
-open import Data.Product
 open import Function.Base using (flip)
 open import Relation.Binary
 open import Relation.Binary.Properties.Poset poset
diff --git a/src/Relation/Binary/Rewriting.agda b/src/Relation/Binary/Rewriting.agda
index 9006765413..10d760e23b 100644
--- a/src/Relation/Binary/Rewriting.agda
+++ b/src/Relation/Binary/Rewriting.agda
@@ -10,7 +10,7 @@
 module Relation.Binary.Rewriting where
 
 open import Agda.Builtin.Equality using (_≡_ ; refl)
-open import Data.Product using (_×_ ; ∃ ; -,_; _,_ ; proj₁ ; proj₂)
+open import Data.Product.Base using (_×_ ; ∃ ; -,_; _,_ ; proj₁ ; proj₂)
 open import Data.Empty
 open import Function.Base using (flip)
 open import Induction.WellFounded
diff --git a/src/Relation/Unary/Indexed.agda b/src/Relation/Unary/Indexed.agda
index 1acfdc8cef..d1cdbb01f5 100644
--- a/src/Relation/Unary/Indexed.agda
+++ b/src/Relation/Unary/Indexed.agda
@@ -8,7 +8,7 @@
 
 module Relation.Unary.Indexed  where
 
-open import Data.Product using (∃; _×_)
+open import Data.Product.Base using (∃; _×_)
 open import Level
 open import Relation.Nullary.Negation using (¬_)
 
diff --git a/src/Relation/Unary/PredicateTransformer.agda b/src/Relation/Unary/PredicateTransformer.agda
index 0ae725588a..cd52a78985 100644
--- a/src/Relation/Unary/PredicateTransformer.agda
+++ b/src/Relation/Unary/PredicateTransformer.agda
@@ -8,7 +8,7 @@
 
 module Relation.Unary.PredicateTransformer where
 
-open import Data.Product
+open import Data.Product.Base using (∃)
 open import Function.Base using (_∘_)
 open import Level hiding (_⊔_)
 open import Relation.Nullary
diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda
index 515d904872..b7accfcc08 100644
--- a/src/Tactic/Cong.agda
+++ b/src/Tactic/Cong.agda
@@ -34,7 +34,7 @@ open import Data.Maybe.Base  as Maybe using (Maybe; just; nothing)
 open import Data.Nat.Base    as Nat   using (ℕ; zero; suc; _≡ᵇ_; _+_)
 open import Data.Unit.Base            using (⊤)
 open import Data.Word.Base   as Word  using (toℕ)
-open import Data.Product
+open import Data.Product.Base         using (_×_; map₁; _,_)
 
 open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_; refl; cong)
 
diff --git a/src/Tactic/RingSolver/NonReflective.agda b/src/Tactic/RingSolver/NonReflective.agda
index 6aa8997bb0..cc0b747037 100644
--- a/src/Tactic/RingSolver/NonReflective.agda
+++ b/src/Tactic/RingSolver/NonReflective.agda
@@ -23,7 +23,7 @@ open import Data.Bool.Base using (Bool; true; false; T; if_then_else_)
 open import Data.Maybe.Base
 open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base using (ℕ)
-open import Data.Product
+open import Data.Product.Base using (_×_; proj₁; proj₂; _,_)
 open import Data.Vec.Base using (Vec)
 open import Data.Vec.N-ary
 
diff --git a/src/Text/Format/Generic.agda b/src/Text/Format/Generic.agda
index 8a304f9c9a..9969801832 100644
--- a/src/Text/Format/Generic.agda
+++ b/src/Text/Format/Generic.agda
@@ -14,7 +14,7 @@ open import Data.Char.Base using (Char)
 open import Data.List.Base as List
 open import Data.Maybe.Base as Maybe
 open import Data.Nat.Base
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Data.Product.Nary.NonDependent
 open import Data.Sum.Base
 open import Data.String.Base