diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
index 77badd1b90..07b75806c2 100644
--- a/src/Algebra/Consequences/Setoid.agda
+++ b/src/Algebra/Consequences/Setoid.agda
@@ -15,7 +15,7 @@ open Setoid S renaming (Carrier to A)
 open import Algebra.Core
 open import Algebra.Definitions _≈_
 open import Data.Sum.Base using (inj₁; inj₂)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_$_)
 import Function.Definitions as FunDefs
 import Relation.Binary.Consequences as Bin
diff --git a/src/Algebra/Construct/LexProduct/Base.agda b/src/Algebra/Construct/LexProduct/Base.agda
index 6076d1afc3..85686fd20c 100644
--- a/src/Algebra/Construct/LexProduct/Base.agda
+++ b/src/Algebra/Construct/LexProduct/Base.agda
@@ -8,10 +8,10 @@
 
 open import Algebra.Core using (Op₂)
 open import Data.Bool.Base using (true; false)
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary.Decidable using (does; yes; no)
+open import Relation.Nullary.Decidable.Core using (does; yes; no)
 
 module Algebra.Construct.LexProduct.Base
   {a b ℓ} {A : Set a} {B : Set b}
diff --git a/src/Algebra/Construct/NaturalChoice/MinMaxOp.agda b/src/Algebra/Construct/NaturalChoice/MinMaxOp.agda
index 4b7d0e20e8..a0b7a945f2 100644
--- a/src/Algebra/Construct/NaturalChoice/MinMaxOp.agda
+++ b/src/Algebra/Construct/NaturalChoice/MinMaxOp.agda
@@ -11,7 +11,7 @@ open import Algebra.Core
 open import Algebra.Bundles
 open import Algebra.Construct.NaturalChoice.Base
 open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (id; _∘_; flip)
 open import Relation.Binary
 open import Relation.Binary.Consequences
diff --git a/src/Algebra/Construct/NaturalChoice/MinOp.agda b/src/Algebra/Construct/NaturalChoice/MinOp.agda
index 37ed331c7e..563e1662f1 100644
--- a/src/Algebra/Construct/NaturalChoice/MinOp.agda
+++ b/src/Algebra/Construct/NaturalChoice/MinOp.agda
@@ -11,7 +11,7 @@ open import Algebra.Core
 open import Algebra.Bundles
 open import Algebra.Construct.NaturalChoice.Base
 open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (id; _∘_)
 open import Relation.Binary
 open import Relation.Binary.Consequences
diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index e64fc4f30b..ae0566a4bf 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -15,17 +15,17 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core
-open import Relation.Nullary.Negation using (¬_)
+open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
+open import Relation.Nullary.Negation.Core using (¬_)
 
 module Algebra.Definitions
   {a ℓ} {A : Set a}   -- The underlying set
   (_≈_ : Rel A ℓ)     -- The underlying equality
   where
 
-open import Algebra.Core
-open import Data.Product
-open import Data.Sum.Base
+open import Algebra.Core using (Op₁; Op₂)
+open import Data.Product.Base using (_×_; ∃-syntax)
+open import Data.Sum.Base using (_⊎_)
 
 ------------------------------------------------------------------------
 -- Properties of operations
diff --git a/src/Algebra/Definitions/RawMagma.agda b/src/Algebra/Definitions/RawMagma.agda
index 5189e02fb8..dc96fedc76 100644
--- a/src/Algebra/Definitions/RawMagma.agda
+++ b/src/Algebra/Definitions/RawMagma.agda
@@ -11,7 +11,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles using (RawMagma)
-open import Data.Product using (_×_; ∃)
+open import Data.Product.Base using (_×_; ∃)
 open import Level using (_⊔_)
 open import Relation.Binary.Core
 open import Relation.Nullary.Negation using (¬_)
diff --git a/src/Algebra/Lattice/Properties/BooleanAlgebra.agda b/src/Algebra/Lattice/Properties/BooleanAlgebra.agda
index 85295c9366..cf90b022b9 100644
--- a/src/Algebra/Lattice/Properties/BooleanAlgebra.agda
+++ b/src/Algebra/Lattice/Properties/BooleanAlgebra.agda
@@ -23,9 +23,9 @@ open import Algebra.Bundles
 open import Algebra.Lattice.Structures _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
 open import Relation.Binary
-open import Function.Base
+open import Function.Base using (id; _$_; _⟨_⟩_)
 open import Function.Bundles using (_⇔_; module Equivalence)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 
 ------------------------------------------------------------------------
 -- Export properties from distributive lattices
diff --git a/src/Algebra/Lattice/Properties/Lattice.agda b/src/Algebra/Lattice/Properties/Lattice.agda
index 747541e49c..b5908f57b1 100644
--- a/src/Algebra/Lattice/Properties/Lattice.agda
+++ b/src/Algebra/Lattice/Properties/Lattice.agda
@@ -11,7 +11,7 @@ import Algebra.Lattice.Properties.Semilattice as SemilatticeProperties
 open import Relation.Binary
 import Relation.Binary.Lattice as R
 open import Function.Base
-open import Data.Product using (_,_; swap)
+open import Data.Product.Base using (_,_; swap)
 
 module Algebra.Lattice.Properties.Lattice
   {l₁ l₂} (L : Lattice l₁ l₂) where
diff --git a/src/Algebra/Lattice/Properties/Semilattice.agda b/src/Algebra/Lattice/Properties/Semilattice.agda
index 4b8fc114fc..38554aedfa 100644
--- a/src/Algebra/Lattice/Properties/Semilattice.agda
+++ b/src/Algebra/Lattice/Properties/Semilattice.agda
@@ -6,11 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Lattice
-open import Algebra.Structures
-open import Function
-open import Data.Product
-open import Relation.Binary
+open import Algebra.Lattice.Bundles using (Semilattice)
+open import Relation.Binary.Bundles using (Poset)
 import Relation.Binary.Lattice as B
 import Relation.Binary.Properties.Poset as PosetProperties
 
diff --git a/src/Algebra/Lattice/Structures.agda b/src/Algebra/Lattice/Structures.agda
index 8e80c4a87b..b02787eee0 100644
--- a/src/Algebra/Lattice/Structures.agda
+++ b/src/Algebra/Lattice/Structures.agda
@@ -14,7 +14,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Core
-open import Data.Product using (proj₁; proj₂)
+open import Data.Product.Base using (proj₁; proj₂)
 open import Level using (_⊔_)
 open import Relation.Binary using (Rel; Setoid; IsEquivalence)
 
diff --git a/src/Algebra/Properties/CommutativeSemigroup.agda b/src/Algebra/Properties/CommutativeSemigroup.agda
index 25d1ac0152..e09253ece7 100644
--- a/src/Algebra/Properties/CommutativeSemigroup.agda
+++ b/src/Algebra/Properties/CommutativeSemigroup.agda
@@ -16,7 +16,7 @@ open CommutativeSemigroup CS
 
 open import Algebra.Definitions _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
-open import Data.Product
+open import Data.Product.Base using (_,_)
 
 ------------------------------------------------------------------------------
 -- Re-export the contents of semigroup
diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda
index 469245b11c..7cdf88c9fe 100644
--- a/src/Algebra/Properties/Group.agda
+++ b/src/Algebra/Properties/Group.agda
@@ -13,8 +13,8 @@ module Algebra.Properties.Group {g₁ g₂} (G : Group g₁ g₂) where
 open Group G
 open import Algebra.Definitions _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
-open import Function
-open import Data.Product
+open import Function.Base using (_$_; _⟨_⟩_)
+open import Data.Product.Base using (_,_; proj₂)
 
 ε⁻¹≈ε : ε ⁻¹ ≈ ε
 ε⁻¹≈ε = begin
diff --git a/src/Algebra/Properties/Ring.agda b/src/Algebra/Properties/Ring.agda
index e310202a37..22dabbac29 100644
--- a/src/Algebra/Properties/Ring.agda
+++ b/src/Algebra/Properties/Ring.agda
@@ -16,7 +16,6 @@ import Algebra.Properties.AbelianGroup as AbelianGroupProperties
 open import Function.Base using (_$_)
 open import Relation.Binary.Reasoning.Setoid setoid
 open import Algebra.Definitions _≈_
-open import Data.Product
 
 ------------------------------------------------------------------------
 -- Export properties of abelian groups
diff --git a/src/Algebra/Properties/Semigroup.agda b/src/Algebra/Properties/Semigroup.agda
index 4147b612e2..22aab4e66e 100644
--- a/src/Algebra/Properties/Semigroup.agda
+++ b/src/Algebra/Properties/Semigroup.agda
@@ -12,7 +12,7 @@ module Algebra.Properties.Semigroup {a ℓ} (S : Semigroup a ℓ) where
 
 open Semigroup S
 open import Algebra.Definitions _≈_
-open import Data.Product
+open import Data.Product.Base using (_,_)
 
 x∙yz≈xy∙z : ∀ x y z → x ∙ (y ∙ z) ≈ (x ∙ y) ∙ z
 x∙yz≈xy∙z x y z = sym (assoc x y z)
diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index 0a904276db..eb9d49b2c9 100644
--- a/src/Algebra/Structures.agda
+++ b/src/Algebra/Structures.agda
@@ -22,7 +22,7 @@ module Algebra.Structures
 open import Algebra.Core
 open import Algebra.Definitions _≈_
 import Algebra.Consequences.Setoid as Consequences
-open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Level using (_⊔_)
 
 ------------------------------------------------------------------------
diff --git a/src/Algebra/Structures/Biased.agda b/src/Algebra/Structures/Biased.agda
index c03e1236eb..0aa549c66c 100644
--- a/src/Algebra/Structures/Biased.agda
+++ b/src/Algebra/Structures/Biased.agda
@@ -9,7 +9,7 @@
 
 open import Algebra.Core
 open import Algebra.Consequences.Setoid
-open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Level using (_⊔_)
 open import Relation.Binary using (Rel; Setoid; IsEquivalence)
 
diff --git a/src/Codata/Sized/Cowriter.agda b/src/Codata/Sized/Cowriter.agda
index 2a6ef961ec..7206c83c86 100644
--- a/src/Codata/Sized/Cowriter.agda
+++ b/src/Codata/Sized/Cowriter.agda
@@ -16,9 +16,9 @@ open import Codata.Sized.Delay using (Delay; later; now)
 open import Codata.Sized.Stream as Stream using (Stream; _∷_)
 open import Data.Unit.Base
 open import Data.List.Base using (List; []; _∷_)
-open import Data.List.NonEmpty using (List⁺; _∷_)
+open import Data.List.NonEmpty.Base using (List⁺; _∷_)
 open import Data.Nat.Base as Nat using (ℕ; zero; suc)
-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.Base using (Vec; []; _∷_)
 open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤; _,_)
diff --git a/src/Codata/Sized/Stream.agda b/src/Codata/Sized/Stream.agda
index 85cd886b5f..4b7d6bd37d 100644
--- a/src/Codata/Sized/Stream.agda
+++ b/src/Codata/Sized/Stream.agda
@@ -15,10 +15,10 @@ open import Data.Nat.Base
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; _∷⁺_)
 open import Data.Vec.Base using (Vec; []; _∷_)
-open import Data.Product as P hiding (map)
-open import Function.Base
+open import Data.Product.Base as P using (Σ; _×_; _,_; <_,_>; proj₁; proj₂)
+open import Function.Base using (id; _∘_)
 open import Level using (Level)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 private
   variable
diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index fe232885eb..ef963f6511 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -13,9 +13,9 @@ open import Algebra.Lattice.Bundles
 import Algebra.Lattice.Properties.BooleanAlgebra as BooleanAlgebraProperties
 open import Data.Bool.Base
 open import Data.Empty
-open import Data.Product
-open import Data.Sum.Base
-open import Function.Base
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
+open import Function.Base using (_⟨_⟩_; const; id)
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence
   using (_⇔_; equivalence; module Equivalence)
@@ -23,8 +23,8 @@ open import Induction.WellFounded using (WellFounded; Acc; acc)
 open import Level using (Level; 0ℓ)
 open import Relation.Binary hiding (_⇔_)
 open import Relation.Binary.PropositionalEquality hiding ([_])
-open import Relation.Nullary using (ofʸ; ofⁿ; does; proof; yes; no)
-open import Relation.Nullary.Decidable using (True)
+open import Relation.Nullary.Reflects using (ofʸ; ofⁿ)
+open import Relation.Nullary.Decidable.Core using (True; does; proof; yes; no)
 import Relation.Unary as U
 
 open import Algebra.Definitions {A = Bool} _≡_
diff --git a/src/Data/Digit.agda b/src/Data/Digit.agda
index 9c47fd544b..7e7c1c7555 100644
--- a/src/Data/Digit.agda
+++ b/src/Data/Digit.agda
@@ -9,21 +9,20 @@
 module Data.Digit where
 
 open import Data.Nat.Base
-open import Data.Nat.Properties
-open import Data.Nat.Solver
+open import Data.Nat.Properties using (_≤?_; _<?_; ≤⇒≤′; module ≤-Reasoning; m≤m+n)
+open import Data.Nat.Solver using (module +-*-Solver)
 open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ)
 open import Data.Bool.Base using (Bool; true; false)
-open import Data.Char using (Char)
+open import Data.Char.Base using (Char)
 open import Data.List.Base
-open import Data.Product
+open import Data.Product.Base using (∃; _,_)
 open import Data.Vec.Base as Vec using (Vec; _∷_; [])
 open import Data.Nat.DivMod
 open import Data.Nat.Induction
-open import Relation.Nullary.Decidable using (does)
-open import Relation.Nullary.Decidable
-open import Relation.Binary using (Decidable)
+open import Relation.Nullary.Decidable using (True; does; toWitness)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
-open import Function
+open import Function.Base using (_$_)
 
 ------------------------------------------------------------------------
 -- Digits
diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index 20a2636216..b591301ac0 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -14,7 +14,7 @@ module Data.Fin.Base where
 open import Data.Bool.Base using (Bool; true; false; T; not)
 open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; _^_)
-open import Data.Product as Product using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (id; _∘_; _on_; flip)
 open import Level using (0ℓ)
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index d7a963f9fd..e181a291e9 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -18,11 +18,13 @@ open import Data.Bool.Base using (Bool; true; false; not; _∧_; _∨_)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Fin.Base
 open import Data.Fin.Patterns
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; s≤s; z≤n; z<s; s<s; _∸_; _^_)
+open import Data.Nat.Base as ℕ
+  using (ℕ; zero; suc; s≤s; z≤n; z<s; s<s; _∸_; _^_)
 import Data.Nat.Properties as ℕₚ
 open import Data.Nat.Solver
 open import Data.Unit using (⊤; tt)
-open import Data.Product using (Σ-syntax; ∃; ∃₂; ∄; _×_; _,_; map; proj₁; proj₂; uncurry; <_,_>)
+open import Data.Product.Base as Prod
+  using (∃; ∃₂; _×_; _,_; map; proj₁; proj₂; uncurry; <_,_>)
 open import Data.Product.Properties using (,-injective)
 open import Data.Product.Algebra using (×-cong)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
@@ -619,7 +621,7 @@ splitAt-≥ (suc m) (suc i) (s≤s i≥m) = cong (Sum.map suc id) (splitAt-≥ m
 remQuot-combine : ∀ {n k} (i : Fin n) j → remQuot k (combine i j) ≡ (i , j)
 remQuot-combine {suc n} {k} zero    j rewrite splitAt-↑ˡ k j (n ℕ.* k) = refl
 remQuot-combine {suc n} {k} (suc i) j rewrite splitAt-↑ʳ k   (n ℕ.* k) (combine i j) =
-  cong (Data.Product.map₁ suc) (remQuot-combine i j)
+  cong (Prod.map₁ suc) (remQuot-combine i j)
 
 combine-remQuot : ∀ {n} k (i : Fin (n ℕ.* k)) → uncurry combine (remQuot {n} k i) ≡ i
 combine-remQuot {suc n} k i with splitAt k i in eq
@@ -1158,4 +1160,3 @@ Please use <⇒<′ instead."
 "Warning: <′⇒≺ was deprecated in v2.0.
 Please use <′⇒< instead."
 #-}
-
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 48a5840bf4..2b25ece003 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -17,7 +17,7 @@ open import Data.Bool.Base as Bool
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _*_ ; _≤_ ; s≤s)
-open import Data.Product as Prod using (_×_; _,_; map₁; map₂′)
+open import Data.Product.Base as Prod using (_×_; _,_; map₁; map₂′)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
 open import Function.Base using (id; _∘_ ; _∘′_; _∘₂_; const; flip)
diff --git a/src/Data/List/Fresh.agda b/src/Data/List/Fresh.agda
index 8665267dd5..72c372003a 100644
--- a/src/Data/List/Fresh.agda
+++ b/src/Data/List/Fresh.agda
@@ -16,7 +16,7 @@ module Data.List.Fresh where
 open import Level using (Level; _⊔_)
 open import Data.Bool.Base using (true; false)
 open import Data.Unit.Polymorphic.Base using (⊤)
-open import Data.Product using (∃; _×_; _,_; -,_; proj₁; proj₂)
+open import Data.Product.Base using (∃; _×_; _,_; -,_; proj₁; proj₂)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
diff --git a/src/Data/List/Fresh/NonEmpty.agda b/src/Data/List/Fresh/NonEmpty.agda
index 1ed72bd9d4..e4b55cb11b 100644
--- a/src/Data/List/Fresh/NonEmpty.agda
+++ b/src/Data/List/Fresh/NonEmpty.agda
@@ -11,9 +11,9 @@ module Data.List.Fresh.NonEmpty where
 open import Level using (Level; _⊔_)
 open import Data.List.Fresh as List# using (List#; []; cons; fresh)
 open import Data.Maybe.Base using (Maybe; nothing; just)
-open import Data.Nat using (ℕ; suc)
-open import Data.Product using (_×_; _,_)
-open import Relation.Binary as B using (Rel)
+open import Data.Nat.Base using (ℕ; suc)
+open import Data.Product.Base using (_×_; _,_)
+open import Relation.Binary.Core using (Rel)
 
 private
   variable
diff --git a/src/Data/List/Kleene/Base.agda b/src/Data/List/Kleene/Base.agda
index c8476318b7..8eb83ba864 100644
--- a/src/Data/List/Kleene/Base.agda
+++ b/src/Data/List/Kleene/Base.agda
@@ -8,11 +8,12 @@
 
 module Data.List.Kleene.Base where
 
-open import Data.Product as Product using (_×_; _,_; map₂; map₁; proj₁; proj₂)
-open import Data.Nat     as ℕ       using (ℕ; suc; zero)
-open import Data.Maybe   as Maybe   using (Maybe; just; nothing)
-open import Data.Sum     as Sum     using (_⊎_; inj₁; inj₂)
-open import Level        as Level   using (Level)
+open import Data.Product.Base as Product
+  using (_×_; _,_; map₂; map₁; proj₁; proj₂)
+open import Data.Nat.Base as ℕ using (ℕ; suc; zero)
+open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
+open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
+open import Level using (Level)
 
 open import Algebra.Core using (Op₂)
 open import Function.Base
diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
index ca48b933d1..047620041d 100644
--- a/src/Data/List/Membership/Setoid.agda
+++ b/src/Data/List/Membership/Setoid.agda
@@ -14,7 +14,7 @@ open import Function.Base using (_∘_; id; flip)
 open import Data.List.Base as List using (List; []; _∷_; length; lookup)
 open import Data.List.Relation.Unary.Any
   using (Any; index; map; here; there)
-open import Data.Product as Prod using (∃; _×_; _,_)
+open import Data.Product.Base as Prod using (∃; _×_; _,_)
 open import Relation.Unary using (Pred)
 open import Relation.Nullary.Negation using (¬_)
 
diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda
index 3cc83a3447..320cacd4b6 100644
--- a/src/Data/List/NonEmpty/Base.agda
+++ b/src/Data/List/NonEmpty/Base.agda
@@ -14,7 +14,7 @@ open import Data.Bool.Properties using (T?)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.Maybe.Base using (Maybe ; nothing; just)
 open import Data.Nat.Base as ℕ
-open import Data.Product as Prod using (∃; _×_; proj₁; proj₂; _,_; -,_)
+open import Data.Product.Base as Prod using (∃; _×_; proj₁; proj₂; _,_; -,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 58d5b39680..9df56d4781 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -25,7 +25,8 @@ open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Nat.Base
 open import Data.Nat.Divisibility
 open import Data.Nat.Properties
-open import Data.Product as Prod hiding (map; zip)
+open import Data.Product.Base as Prod
+  using (_×_; _,_; uncurry; uncurry′; proj₁; proj₂; <_,_>)
 import Data.Product.Relation.Unary.All as Prod using (All)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
diff --git a/src/Data/List/Relation/Binary/Lex/Core.agda b/src/Data/List/Relation/Binary/Lex/Core.agda
index 3c90bf3c9f..96549e013b 100644
--- a/src/Data/List/Relation/Binary/Lex/Core.agda
+++ b/src/Data/List/Relation/Binary/Lex/Core.agda
@@ -10,7 +10,7 @@ module Data.List.Relation.Binary.Lex.Core where
 
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Unit.Base using (⊤; tt)
-open import Data.Product using (_×_; _,_; proj₁; proj₂; uncurry)
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; uncurry)
 open import Data.List.Base using (List; []; _∷_)
 open import Function.Base using (_∘_; flip; id)
 open import Level using (Level; _⊔_)
diff --git a/src/Data/List/Relation/Binary/Pointwise/Base.agda b/src/Data/List/Relation/Binary/Pointwise/Base.agda
index 8e24dcd2dc..e547aea169 100644
--- a/src/Data/List/Relation/Binary/Pointwise/Base.agda
+++ b/src/Data/List/Relation/Binary/Pointwise/Base.agda
@@ -8,9 +8,9 @@
 
 module Data.List.Relation.Binary.Pointwise.Base where
 
-open import Data.Product using (_×_; <_,_>)
+open import Data.Product.Base using (_×_; <_,_>)
 open import Data.List.Base using (List; []; _∷_)
-open import Level
+open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (REL; _⇒_)
 
 private
diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda
index 674a8e33d5..090af7e6b6 100644
--- a/src/Data/List/Relation/Unary/All.agda
+++ b/src/Data/List/Relation/Unary/All.agda
@@ -15,11 +15,11 @@ open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.List.Membership.Propositional renaming (_∈_ to _∈ₚ_)
 import Data.List.Membership.Setoid as SetoidMembership
-open import Data.Product as Prod
+open import Data.Product.Base as Prod
   using (∃; -,_; _×_; _,_; proj₁; proj₂; uncurry)
 open import Data.Sum.Base as Sum using (inj₁; inj₂)
-open import Function
-open import Level
+open import Function.Base using (_∘_; _∘′_; id; const)
+open import Level using (Level; _⊔_)
 open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec
 open import Relation.Unary hiding (_∈_)
diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda
index 19af845152..eb010e2a39 100644
--- a/src/Data/List/Relation/Unary/Any.agda
+++ b/src/Data/List/Relation/Unary/Any.agda
@@ -11,7 +11,7 @@ module Data.List.Relation.Unary.Any where
 open import Data.Empty
 open import Data.Fin.Base using (Fin; 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.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Level using (Level; _⊔_)
 open import Relation.Nullary using (¬_; yes; no; _⊎-dec_)
diff --git a/src/Data/Maybe/Base.agda b/src/Data/Maybe/Base.agda
index 0cb8c473bf..b0ae001f46 100644
--- a/src/Data/Maybe/Base.agda
+++ b/src/Data/Maybe/Base.agda
@@ -14,7 +14,7 @@ open import Level
 open import Data.Bool.Base using (Bool; true; false; not)
 open import Data.Unit.Base using (⊤)
 open import Data.These.Base using (These; this; that; these)
-open import Data.Product as Prod using (_×_; _,_)
+open import Data.Product.Base as Prod using (_×_; _,_)
 open import Function.Base
 open import Relation.Nullary.Reflects
 open import Relation.Nullary.Decidable.Core
diff --git a/src/Data/Nat/DivMod/Core.agda b/src/Data/Nat/DivMod/Core.agda
index 02b1c917c6..fed1a1ae0d 100644
--- a/src/Data/Nat/DivMod/Core.agda
+++ b/src/Data/Nat/DivMod/Core.agda
@@ -14,7 +14,7 @@ open import Agda.Builtin.Nat using ()
 open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Negation using (contradiction)
diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda
index 07a80bcdd9..c202d740ba 100644
--- a/src/Data/Nat/Divisibility.agda
+++ b/src/Data/Nat/Divisibility.agda
@@ -12,14 +12,12 @@ open import Algebra
 open import Data.Nat.Base
 open import Data.Nat.DivMod
 open import Data.Nat.Properties
-open import Data.Product
-open import Data.Unit using (tt)
-open import Function.Base
+open import Data.Unit.Base using (tt)
+open import Function.Base using (_∘′_; _$_)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (0ℓ)
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Decidable as Dec using (False)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable as Dec using (False; yes; no)
+open import Relation.Nullary.Negation.Core using (contradiction)
 open import Relation.Binary
 import Relation.Binary.Reasoning.Preorder as PreorderReasoning
 open import Relation.Binary.PropositionalEquality as PropEq
diff --git a/src/Data/Nat/Induction.agda b/src/Data/Nat/Induction.agda
index ea68692a51..209f9f60bb 100644
--- a/src/Data/Nat/Induction.agda
+++ b/src/Data/Nat/Induction.agda
@@ -10,9 +10,8 @@ module Data.Nat.Induction where
 
 open import Data.Nat.Base
 open import Data.Nat.Properties using (<⇒<′)
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_)
 open import Data.Unit.Polymorphic.Base
-open import Function.Base
 open import Induction
 open import Induction.WellFounded as WF
 open import Level using (Level)
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 27725b98ad..ac8a4dcaa5 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -23,7 +23,7 @@ open import Data.Bool.Base using (Bool; false; true; T)
 open import Data.Bool.Properties using (T?)
 open import Data.Empty using (⊥)
 open import Data.Nat.Base
-open import Data.Product using (∄; ∃; _×_; _,_)
+open import Data.Product.Base using (∃; _×_; _,_)
 open import Data.Sum.Base as Sum
 open import Data.Unit using (tt)
 open import Function.Base
@@ -2172,7 +2172,7 @@ module _ {p} {P : Pred ℕ p} (P? : U.Decidable P) where
   ... | _      | yes (n , n<v , Pn) = yes (n , m≤n⇒m≤1+n n<v , Pn)
   ... | no ¬Pv | no ¬Pn<v           = no ¬Pn<1+v
     where
-    ¬Pn<1+v : ∄ λ n → n < suc v × P n
+    ¬Pn<1+v : (∃ λ n → n < suc v × P n) → ⊥
     ¬Pn<1+v (n , s≤s n≤v , Pn) with n ≟ v
     ... | yes refl = ¬Pv Pn
     ... | no  n≢v  = ¬Pn<v (n , ≤∧≢⇒< n≤v n≢v , Pn)
diff --git a/src/Data/Nat/Show.agda b/src/Data/Nat/Show.agda
index 9f0fdf2bb5..1777aca9d3 100644
--- a/src/Data/Nat/Show.agda
+++ b/src/Data/Nat/Show.agda
@@ -16,9 +16,9 @@ open import Data.List.Effectful using (module TraversableA)
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; _<∣>_; when)
 import Data.Maybe.Effectful as Maybe
 open import Data.Nat
-open import Data.Product using (proj₁)
-open import Data.String.Base using (toList; fromList; String)
-open import Function.Base
+open import Data.Product.Base using (proj₁)
+open import Data.String.Base as String using (String; fromList; toList)
+open import Function.Base using (_∘′_; _∘_)
 open import Relation.Nullary.Decidable using (True)
 
 ------------------------------------------------------------------------
@@ -62,7 +62,7 @@ toDecimalChars : ℕ → List Char
 toDecimalChars = List.map toDigitChar ∘′ toNatDigits 10
 
 show : ℕ → String
-show = fromList ∘ toDecimalChars
+show = fromList ∘′ toDecimalChars
 
 -- Arbitrary base betwen 2 & 16.
 -- Warning: when compiled the time complexity of `showInBase b n` is
diff --git a/src/Data/Product.agda b/src/Data/Product.agda
index 08c0aa0c7f..02bf53a97b 100644
--- a/src/Data/Product.agda
+++ b/src/Data/Product.agda
@@ -23,18 +23,11 @@ private
 open import Data.Product.Base public
 
 ------------------------------------------------------------------------
--- Existential quantifiers
-
-∃ : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
-∃ = Σ _
+-- Negation of existential quantifier
 
 ∄ : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
 ∄ P = ¬ ∃ P
 
-∃₂ : ∀ {A : Set a} {B : A → Set b}
-     (C : (x : A) → B x → Set c) → Set (a ⊔ b ⊔ c)
-∃₂ C = ∃ λ a → ∃ λ b → C a b
-
 -- Unique existence (parametrised by an underlying equality).
 
 ∃! : {A : Set a} → (A → A → Set ℓ) → (A → Set b) → Set (a ⊔ b ⊔ ℓ)
@@ -42,13 +35,6 @@ open import Data.Product.Base public
 
 -- Syntax
 
-infix 2 ∃-syntax
-
-∃-syntax : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
-∃-syntax = ∃
-
-syntax ∃-syntax (λ x → B) = ∃[ x ] B
-
 infix 2 ∄-syntax
 
 ∄-syntax : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
diff --git a/src/Data/Product/Algebra.agda b/src/Data/Product/Algebra.agda
index f11045d778..c64057dcc0 100644
--- a/src/Data/Product/Algebra.agda
+++ b/src/Data/Product/Algebra.agda
@@ -11,9 +11,9 @@ module Data.Product.Algebra where
 open import Algebra
 open import Data.Bool.Base using (true; false)
 open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
-open import Data.Product
+open import Data.Product.Base
 open import Data.Product.Properties
-open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
+open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Sum.Algebra
 open import Data.Unit.Polymorphic using (⊤; tt)
 open import Function.Base using (_∘′_)
diff --git a/src/Data/Product/Base.agda b/src/Data/Product/Base.agda
index 7ee638392c..02f7e52697 100644
--- a/src/Data/Product/Base.agda
+++ b/src/Data/Product/Base.agda
@@ -9,7 +9,7 @@
 module Data.Product.Base where
 
 open import Function.Base
-open import Level
+open import Level using (Level; _⊔_)
 
 private
   variable
@@ -31,6 +31,19 @@ open import Agda.Builtin.Sigma public
 module Σ = Agda.Builtin.Sigma.Σ
   renaming (fst to proj₁; snd to proj₂)
 
+------------------------------------------------------------------------
+-- Existential quantifiers
+
+∃ : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
+∃ = Σ _
+
+∃₂ : ∀ {A : Set a} {B : A → Set b}
+     (C : (x : A) → B x → Set c) → Set (a ⊔ b ⊔ c)
+∃₂ C = ∃ λ a → ∃ λ b → C a b
+
+------------------------------------------------------------------------
+-- Syntaxes
+
 -- The syntax declaration below is attached to Σ-syntax, to make it
 -- easy to import Σ without the special syntax.
 
@@ -41,6 +54,13 @@ infix 2 Σ-syntax
 
 syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B
 
+infix 2 ∃-syntax
+
+∃-syntax : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
+∃-syntax = ∃
+
+syntax ∃-syntax (λ x → B) = ∃[ x ] B
+
 ------------------------------------------------------------------------
 -- Definition of non-dependent products
 
diff --git a/src/Data/Product/Effectful/Left.agda b/src/Data/Product/Effectful/Left.agda
index 66362621ee..279555b9c9 100644
--- a/src/Data/Product/Effectful/Left.agda
+++ b/src/Data/Product/Effectful/Left.agda
@@ -18,7 +18,7 @@ open import Level
 module Data.Product.Effectful.Left
   {a e} (A : RawMonoid a e) (b : Level) where
 
-open import Data.Product
+open import Data.Product.Base
 import Data.Product.Effectful.Left.Base as Base
 open import Effect.Applicative using (RawApplicative)
 open import Effect.Monad using (RawMonad; RawMonadT; mkRawMonad)
diff --git a/src/Data/Product/Effectful/Left/Base.agda b/src/Data/Product/Effectful/Left/Base.agda
index d5b0b42c92..e3f7edef69 100644
--- a/src/Data/Product/Effectful/Left/Base.agda
+++ b/src/Data/Product/Effectful/Left/Base.agda
@@ -17,7 +17,7 @@ open import Level
 module Data.Product.Effectful.Left.Base
   {a} (A : Set a) (b : Level) where
 
-open import Data.Product using (_×_; map₂; proj₁; proj₂; <_,_>)
+open import Data.Product.Base using (_×_; map₂; proj₁; proj₂; <_,_>)
 open import Effect.Functor using (RawFunctor)
 open import Effect.Comonad using (RawComonad)
 
diff --git a/src/Data/Product/Effectful/Right.agda b/src/Data/Product/Effectful/Right.agda
index 640b4e908d..fd5cb9b423 100644
--- a/src/Data/Product/Effectful/Right.agda
+++ b/src/Data/Product/Effectful/Right.agda
@@ -18,7 +18,7 @@ open import Level
 module Data.Product.Effectful.Right
   (a : Level) {b e} (B : RawMonoid b e) where
 
-open import Data.Product
+open import Data.Product.Base
 import Data.Product.Effectful.Right.Base as Base
 open import Effect.Applicative using (RawApplicative)
 open import Effect.Monad using (RawMonad; RawMonadT; mkRawMonad)
diff --git a/src/Data/Product/Effectful/Right/Base.agda b/src/Data/Product/Effectful/Right/Base.agda
index 273185bf8e..556483f66f 100644
--- a/src/Data/Product/Effectful/Right/Base.agda
+++ b/src/Data/Product/Effectful/Right/Base.agda
@@ -17,7 +17,7 @@ open import Level
 module Data.Product.Effectful.Right.Base
   {b} (B : Set b) (a : Level) where
 
-open import Data.Product using (_×_; map₁; proj₁; proj₂; <_,_>)
+open import Data.Product.Base using (_×_; map₁; proj₁; proj₂; <_,_>)
 open import Effect.Functor using (RawFunctor)
 open import Effect.Comonad using (RawComonad)
 
diff --git a/src/Data/Product/Nary/NonDependent.agda b/src/Data/Product/Nary/NonDependent.agda
index 1d5678e00c..cb421f16b6 100644
--- a/src/Data/Product/Nary/NonDependent.agda
+++ b/src/Data/Product/Nary/NonDependent.agda
@@ -16,15 +16,15 @@ module Data.Product.Nary.NonDependent where
 
 open import Level as L using (Level; _⊔_; Lift; 0ℓ)
 open import Agda.Builtin.Unit
-open import Data.Product as Prod
+open import Data.Product.Base as Prod
 import Data.Product.Properties as Prodₚ
 open import Data.Sum.Base using (_⊎_)
 open import Data.Nat.Base using (ℕ; zero; suc; pred)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Function.Base using (const; _∘′_; _∘_)
-open import Relation.Nullary.Decidable using (Dec; yes; no; _×-dec_)
-open import Relation.Binary using (Rel)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no; _×-dec_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
 
 open import Function.Nary.NonDependent.Base
 
diff --git a/src/Data/Product/Properties.agda b/src/Data/Product/Properties.agda
index fa4909e955..1cc3c2383e 100644
--- a/src/Data/Product/Properties.agda
+++ b/src/Data/Product/Properties.agda
@@ -9,8 +9,9 @@
 module Data.Product.Properties where
 
 open import Axiom.UniquenessOfIdentityProofs
-open import Data.Product
-open import Function
+open import Data.Product.Base
+open import Function.Base using (_∋_; _∘_; id)
+open import Function.Bundles using (_↔_; mk↔′)
 open import Level using (Level)
 open import Relation.Binary using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality
diff --git a/src/Data/Product/Relation/Unary/All.agda b/src/Data/Product/Relation/Unary/All.agda
index 8c1b67dc50..1257de57c2 100644
--- a/src/Data/Product/Relation/Unary/All.agda
+++ b/src/Data/Product/Relation/Unary/All.agda
@@ -8,10 +8,8 @@
 
 module Data.Product.Relation.Unary.All where
 
-open import Level
-open import Data.Product
-open import Function.Base
-open import Relation.Unary
+open import Level using (Level; _⊔_)
+open import Data.Product.Base using (_×_; _,_)
 
 private
   variable
diff --git a/src/Data/String/Base.agda b/src/Data/String/Base.agda
index b3556026db..1a56376f59 100644
--- a/src/Data/String/Base.agda
+++ b/src/Data/String/Base.agda
@@ -8,7 +8,6 @@
 
 module Data.String.Base where
 
-open import Level using (zero)
 open import Data.Bool.Base using (Bool; true; false)
 open import Data.Char.Base as Char using (Char)
 open import Data.List.Base as List using (List; [_]; _∷_; [])
@@ -17,13 +16,13 @@ open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise)
 open import Data.List.Relation.Binary.Lex.Core using (Lex-<; Lex-≤)
 open import Data.Maybe.Base as Maybe using (Maybe)
 open import Data.Nat.Base using (ℕ; _∸_; ⌊_/2⌋; ⌈_/2⌉)
-open import Data.Product using (proj₁; proj₂)
+open import Data.Product.Base using (proj₁; proj₂)
 open import Function.Base using (_on_; _∘′_; _∘_)
-open import Level using (Level)
+open import Level using (Level; 0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary.Decidable using (does)
+open import Relation.Nullary.Decidable.Core using (does)
 
 ------------------------------------------------------------------------
 -- From Agda.Builtin: type and renamed primitives
@@ -47,17 +46,17 @@ open String public using ( String )
 -- Pointwise equality on Strings
 
 infix 4 _≈_
-_≈_ : Rel String zero
+_≈_ : Rel String 0ℓ
 _≈_ = Pointwise _≡_ on toList
 
 -- Lexicographic ordering on Strings
 
 infix 4 _<_
-_<_ : Rel String zero
+_<_ : Rel String 0ℓ
 _<_ = Lex-< _≡_ Char._<_ on toList
 
 infix 4 _≤_
-_≤_ : Rel String zero
+_≤_ : Rel String 0ℓ
 _≤_ = Lex-≤ _≡_ Char._<_ on toList
 
 ------------------------------------------------------------------------
diff --git a/src/Data/String/Unsafe.agda b/src/Data/String/Unsafe.agda
index 91a62a61d1..9c001365a3 100644
--- a/src/Data/String/Unsafe.agda
+++ b/src/Data/String/Unsafe.agda
@@ -12,7 +12,7 @@ import Data.List.Base as List
 import Data.List.Properties as Listₚ
 open import Data.Maybe.Base using (maybe′)
 open import Data.Nat.Base using (zero; suc; _+_)
-open import Data.Product using (proj₂)
+open import Data.Product.Base using (proj₂)
 open import Data.String.Base
 open import Function.Base using (_∘′_)
 
diff --git a/src/Data/Sum/Algebra.agda b/src/Data/Sum/Algebra.agda
index 717bc347c1..f69988942b 100644
--- a/src/Data/Sum/Algebra.agda
+++ b/src/Data/Sum/Algebra.agda
@@ -10,7 +10,7 @@ module Data.Sum.Algebra where
 
 open import Algebra
 open import Data.Empty.Polymorphic using (⊥)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Data.Sum.Base
 open import Data.Sum.Properties
 open import Data.Unit.Polymorphic using (⊤; tt)
diff --git a/src/Data/Unit/Polymorphic/Properties.agda b/src/Data/Unit/Polymorphic/Properties.agda
index 8513229ba1..dce385f19e 100644
--- a/src/Data/Unit/Polymorphic/Properties.agda
+++ b/src/Data/Unit/Polymorphic/Properties.agda
@@ -11,7 +11,7 @@ module Data.Unit.Polymorphic.Properties where
 
 open import Level
 open import Function.Bundles using (_↔_; mk↔)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Data.Sum.Base using (inj₁)
 open import Data.Unit.Base renaming (⊤ to ⊤*)
 open import Data.Unit.Polymorphic.Base using (⊤; tt)
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 911766496a..9f6d86b792 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -12,12 +12,12 @@ open import Data.Bool.Base using (Bool; true; false; if_then_else_)
 open import Data.Nat.Base
 open import Data.Fin.Base using (Fin; 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.These.Base as These using (These; this; that; these)
 open import Function.Base using (const; _∘′_; id; _∘_)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
-open import Relation.Nullary.Decidable using (does)
+open import Relation.Nullary.Decidable.Core using (does)
 open import Relation.Unary using (Pred; Decidable)
 
 private
diff --git a/src/Data/Vec/Bounded/Base.agda b/src/Data/Vec/Bounded/Base.agda
index 9c874ec89e..17b33ef7be 100644
--- a/src/Data/Vec/Bounded/Base.agda
+++ b/src/Data/Vec/Bounded/Base.agda
@@ -8,7 +8,6 @@
 
 module Data.Vec.Bounded.Base where
 
-open import Level using (Level)
 open import Data.Nat.Base
 import Data.Nat.Properties as ℕₚ
 open import Data.List.Base as List using (List)
@@ -16,13 +15,13 @@ open import Data.List.Extrema ℕₚ.≤-totalOrder
 open import Data.List.Relation.Unary.All as All using (All)
 import Data.List.Relation.Unary.All.Properties as Allₚ
 open import Data.List.Membership.Propositional using (mapWith∈)
-open import Data.Product using (∃; _×_; _,_; proj₁; proj₂)
+open import Data.Product.Base using (∃; _×_; _,_; proj₁; proj₂)
 open import Data.Vec.Base as Vec using (Vec)
 open import Data.These.Base as These using (These)
-open import Function
-open import Relation.Nullary
-open import Relation.Unary
-open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
+open import Function.Base using (_∘_; id; _$_)
+open import Level using (Level)
+open import Relation.Nullary.Decidable.Core using (recompute)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
 
 private
   variable
diff --git a/src/Data/Vec/Functional.agda b/src/Data/Vec/Functional.agda
index 26e8f32160..091886bef5 100644
--- a/src/Data/Vec/Functional.agda
+++ b/src/Data/Vec/Functional.agda
@@ -18,10 +18,10 @@ module Data.Vec.Functional where
 open import Data.Fin.Base
 open import Data.List.Base as L using (List)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero; pred)
-open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂; uncurry)
+open import Data.Product.Base using (Σ; ∃; _×_; _,_; proj₁; proj₂; uncurry)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Vec.Base as V using (Vec)
-open import Function.Base
+open import Function.Base using (_∘_; const; flip; _ˢ_; id)
 open import Level using (Level)
 
 infixr 5 _∷_ _++_
diff --git a/src/Data/Vec/N-ary.agda b/src/Data/Vec/N-ary.agda
index 7e10c5567c..197552d753 100644
--- a/src/Data/Vec/N-ary.agda
+++ b/src/Data/Vec/N-ary.agda
@@ -11,14 +11,13 @@ module Data.Vec.N-ary where
 open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Function.Bundles using (_↔_; Inverse; mk↔′)
 open import Data.Nat.Base hiding (_⊔_)
-open import Data.Product as Prod
-open import Data.Vec.Base
-open import Function.Base
+open import Data.Product.Base as Prod using (∃; _,_)
+open import Data.Vec.Base using (Vec; []; _∷_; head; tail)
+open import Function.Base using (_∘_; id; flip; constᵣ)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (Level; _⊔_)
-open import Relation.Binary hiding (_⇔_)
-open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary.Decidable
+open import Relation.Binary.Core using (REL)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
 private
   variable
diff --git a/src/Data/Vec/Recursive.agda b/src/Data/Vec/Recursive.agda
index 765db00991..0ecc16f687 100644
--- a/src/Data/Vec/Recursive.agda
+++ b/src/Data/Vec/Recursive.agda
@@ -16,15 +16,12 @@
 
 module Data.Vec.Recursive where
 
-open import Level using (Level; lift)
-open import Function.Bundles using (mk↔′)
-open import Function.Properties.Inverse using (↔-isEquivalence; ↔-refl; ↔-sym; ↔-trans)
 open import Data.Nat.Base as Nat using (ℕ; zero; suc; NonZero; pred)
 open import Data.Nat.Properties using (+-comm; *-comm)
 open import Data.Empty.Polymorphic
 open import Data.Fin.Base as Fin using (Fin; zero; suc)
 open import Data.Fin.Properties using (1↔⊤; *↔×)
-open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Base as Prod using (_×_; _,_; proj₁; proj₂)
 open import Data.Product.Algebra using (×-cong)
 open import Data.Sum.Base as Sum using (_⊎_)
 open import Data.Unit.Base using (tt)
@@ -32,8 +29,11 @@ open import Data.Unit.Polymorphic.Base using (⊤)
 open import Data.Unit.Polymorphic.Properties using (⊤↔⊤*)
 open import Data.Vec.Base as Vec using (Vec; _∷_)
 open import Data.Vec.N-ary using (N-ary)
-open import Function
-open import Relation.Unary
+open import Function.Base using (_∘′_; _∘_; id)
+open import Function.Bundles using (_↔_; mk↔′; mk↔)
+open import Function.Properties.Inverse using (↔-isEquivalence; ↔-refl; ↔-sym; ↔-trans)
+open import Level using (Level; lift)
+open import Relation.Unary using (IUniversal; Universal; _⇒_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; trans; cong; subst)
 open import Relation.Binary.Structures using (IsEquivalence)
 
diff --git a/src/Data/W.agda b/src/Data/W.agda
index 3f2b35909f..159c0883a5 100644
--- a/src/Data/W.agda
+++ b/src/Data/W.agda
@@ -8,9 +8,9 @@
 
 module Data.W where
 
-open import Level
+open import Level using (Level; _⊔_)
 open import Function.Base using (_$_; _∘_; const)
-open import Data.Product using (_,_; -,_; proj₂)
+open import Data.Product.Base using (_,_; -,_; proj₂)
 open import Data.Container.Core using (Container; ⟦_⟧; Shape; Position; _⇒_; ⟪_⟫)
 open import Data.Container.Relation.Unary.All using (□; all)
 open import Relation.Nullary.Negation using (¬_)
diff --git a/src/Effect/Applicative.agda b/src/Effect/Applicative.agda
index 51f7d21368..729966752c 100644
--- a/src/Effect/Applicative.agda
+++ b/src/Effect/Applicative.agda
@@ -12,7 +12,7 @@
 module Effect.Applicative where
 
 open import Data.Bool.Base using (Bool; true; false)
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.Unit.Polymorphic.Base using (⊤)
 
 open import Effect.Choice using (RawChoice)
diff --git a/src/Effect/Monad/State/Transformer/Base.agda b/src/Effect/Monad/State/Transformer/Base.agda
index 0680a2207b..3b5d60fd6e 100644
--- a/src/Effect/Monad/State/Transformer/Base.agda
+++ b/src/Effect/Monad/State/Transformer/Base.agda
@@ -9,7 +9,7 @@
 
 module Effect.Monad.State.Transformer.Base where
 
-open import Data.Product using (_×_; proj₁; proj₂)
+open import Data.Product.Base using (_×_; proj₁; proj₂)
 open import Data.Unit.Polymorphic.Base using (⊤)
 open import Function.Base using (_∘′_; const; id)
 open import Level using (Level; suc; _⊔_)
diff --git a/src/Effect/Monad/Writer/Transformer/Base.agda b/src/Effect/Monad/Writer/Transformer/Base.agda
index bf3c254fc3..4f910b101d 100644
--- a/src/Effect/Monad/Writer/Transformer/Base.agda
+++ b/src/Effect/Monad/Writer/Transformer/Base.agda
@@ -9,7 +9,7 @@
 module Effect.Monad.Writer.Transformer.Base where
 
 open import Algebra using (RawMonoid)
-open import Data.Product using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Data.Unit.Polymorphic using (⊤; tt)
 open import Function.Base using (id; _∘′_)
 open import Level using (Level; suc; _⊔_)
diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda
index 6284182845..d113f14858 100644
--- a/src/Function/Bundles.agda
+++ b/src/Function/Bundles.agda
@@ -23,7 +23,7 @@ open import Function.Base using (_∘_)
 import Function.Definitions as FunctionDefinitions
 import Function.Structures as FunctionStructures
 open import Level using (Level; _⊔_; suc)
-open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Relation.Binary hiding (_⇔_)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_)
diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda
index 2b7603deea..e8c6a0f498 100644
--- a/src/Function/Consequences.agda
+++ b/src/Function/Consequences.agda
@@ -8,13 +8,12 @@
 
 module Function.Consequences where
 
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Function.Definitions
-open import Level
+open import Level using (Level)
 open import Relation.Binary
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
-open import Relation.Nullary.Negation using (¬_)
-open import Relation.Nullary.Negation.Core using (contraposition)
+open import Relation.Nullary.Negation.Core using (¬_; contraposition)
 
 private
   variable
diff --git a/src/Function/Construct/Composition.agda b/src/Function/Construct/Composition.agda
index 242456d212..a18b4b87b1 100644
--- a/src/Function/Construct/Composition.agda
+++ b/src/Function/Construct/Composition.agda
@@ -8,10 +8,10 @@
 
 module Function.Construct.Composition where
 
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function
 open import Level using (Level)
-open import Relation.Binary as B hiding (_⇔_; IsEquivalence)
+open import Relation.Binary hiding (_⇔_; IsEquivalence)
 
 private
   variable
diff --git a/src/Function/Construct/Identity.agda b/src/Function/Construct/Identity.agda
index 1b69165dda..32660bee09 100644
--- a/src/Function/Construct/Identity.agda
+++ b/src/Function/Construct/Identity.agda
@@ -8,12 +8,12 @@
 
 module Function.Construct.Identity where
 
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
 open import Function.Bundles
 import Function.Definitions as Definitions
 import Function.Structures as Structures
-open import Level
+open import Level using (Level)
 open import Relation.Binary as B hiding (_⇔_; IsEquivalence)
 open import Relation.Binary.PropositionalEquality using (_≡_; setoid)
 
diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda
index ea86704a57..86fa273c57 100644
--- a/src/Function/Construct/Symmetry.agda
+++ b/src/Function/Construct/Symmetry.agda
@@ -8,7 +8,7 @@
 
 module Function.Construct.Symmetry where
 
-open import Data.Product using (_,_; swap; proj₁; proj₂)
+open import Data.Product.Base using (_,_; swap; proj₁; proj₂)
 open import Function
 open import Level using (Level)
 open import Relation.Binary hiding (_⇔_)
diff --git a/src/Function/Definitions.agda b/src/Function/Definitions.agda
index ac805d9472..bfeff3c05c 100644
--- a/src/Function/Definitions.agda
+++ b/src/Function/Definitions.agda
@@ -8,7 +8,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary
+open import Relation.Binary.Core using (Rel)
 
 module Function.Definitions
   {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
@@ -16,10 +16,9 @@ module Function.Definitions
   (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain
   where
 
-open import Data.Product using (∃; _×_)
+open import Data.Product.Base using (_×_)
 import Function.Definitions.Core1 as Core₁
 import Function.Definitions.Core2 as Core₂
-open import Function.Base
 open import Level using (_⊔_)
 
 ------------------------------------------------------------------------
diff --git a/src/Function/Definitions/Core1.agda b/src/Function/Definitions/Core1.agda
index c81e841af9..b11ca26fea 100644
--- a/src/Function/Definitions/Core1.agda
+++ b/src/Function/Definitions/Core1.agda
@@ -9,7 +9,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary
+open import Relation.Binary.Core using (Rel)
 
 module Function.Definitions.Core1
   {a b ℓ₁} {A : Set a} {B : Set b} (_≈₁_ : Rel A ℓ₁)
diff --git a/src/Function/Definitions/Core2.agda b/src/Function/Definitions/Core2.agda
index 313f331063..74973d8433 100644
--- a/src/Function/Definitions/Core2.agda
+++ b/src/Function/Definitions/Core2.agda
@@ -9,13 +9,13 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary
+open import Relation.Binary.Core using (Rel)
 
 module Function.Definitions.Core2
   {a b ℓ₂} {A : Set a} {B : Set b} (_≈₂_ : Rel B ℓ₂)
   where
 
-open import Data.Product using (∃)
+open import Data.Product.Base using (∃)
 open import Level using (Level; _⊔_)
 
 ------------------------------------------------------------------------
diff --git a/src/Function/Equality.agda b/src/Function/Equality.agda
index 97bb752ceb..bb32bca8cd 100644
--- a/src/Function/Equality.agda
+++ b/src/Function/Equality.agda
@@ -14,7 +14,7 @@
 module Function.Equality where
 
 import Function.Base as Fun
-open import Level
+open import Level using (Level; _⊔_)
 open import Relation.Binary using (Setoid)
 open import Relation.Binary.Indexed.Heterogeneous
   using (IndexedSetoid; _=[_]⇒_)
diff --git a/src/Function/Metric/Definitions.agda b/src/Function/Metric/Definitions.agda
index 6c6d471aef..f0be9cb724 100644
--- a/src/Function/Metric/Definitions.agda
+++ b/src/Function/Metric/Definitions.agda
@@ -11,7 +11,7 @@
 module Function.Metric.Definitions where
 
 open import Algebra.Core using (Op₂)
-open import Data.Product using (∃)
+open import Data.Product.Base using (∃)
 open import Function.Metric.Core using (DistanceFunction)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_)
diff --git a/src/Function/Nary/NonDependent/Base.agda b/src/Function/Nary/NonDependent/Base.agda
index 72e093b3a7..efb24aec57 100644
--- a/src/Function/Nary/NonDependent/Base.agda
+++ b/src/Function/Nary/NonDependent/Base.agda
@@ -16,7 +16,7 @@ module Function.Nary.NonDependent.Base where
 
 open import Level using (Level; 0ℓ; _⊔_)
 open import Data.Nat.Base using (ℕ; zero; suc)
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.Unit.Polymorphic.Base
 open import Function.Base using (_∘′_; _$′_; const; flip)
 
diff --git a/src/Function/Properties/Inverse.agda b/src/Function/Properties/Inverse.agda
index 6310a8479f..508a8664be 100644
--- a/src/Function/Properties/Inverse.agda
+++ b/src/Function/Properties/Inverse.agda
@@ -10,7 +10,7 @@
 module Function.Properties.Inverse where
 
 open import Axiom.Extensionality.Propositional using (Extensionality)
-open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Function.Bundles
 open import Level using (Level)
 open import Relation.Binary using (Setoid; IsEquivalence)
diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda
index 31004c2db4..770dab600e 100644
--- a/src/Function/Structures.agda
+++ b/src/Function/Structures.agda
@@ -15,8 +15,7 @@ module Function.Structures {a b ℓ₁ ℓ₂}
   {B : Set b} (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain
   where
 
-open import Data.Product using (∃; _×_; _,_)
-open import Function.Base
+open import Data.Product.Base using (_,_)
 open import Function.Definitions
 open import Level using (_⊔_)
 
diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda
index d580452f0f..c1e206a0af 100644
--- a/src/Induction/WellFounded.agda
+++ b/src/Induction/WellFounded.agda
@@ -6,15 +6,14 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary
-
 module Induction.WellFounded where
 
-open import Data.Product
-open import Function
+open import Data.Product.Base using (Σ; _,_; proj₁)
+open import Function.Base using (_on_)
 open import Induction
-open import Level
-open import Relation.Binary.PropositionalEquality hiding (trans)
+open import Level using (Level; _⊔_)
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Unary
 
 private
diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index ff82600c03..cd560ec995 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -10,7 +10,7 @@ module Relation.Binary.Consequences where
 
 open import Data.Maybe.Base using (just; nothing; decToMaybe)
 open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Data.Empty.Irrelevant using (⊥-elim)
 open import Function.Base using (_∘_; _∘₂_; _$_; flip)
 open import Level using (Level)
diff --git a/src/Relation/Binary/Construct/Flip/EqAndOrd.agda b/src/Relation/Binary/Construct/Flip/EqAndOrd.agda
index 1d3e9430d9..c3c4dc2a18 100644
--- a/src/Relation/Binary/Construct/Flip/EqAndOrd.agda
+++ b/src/Relation/Binary/Construct/Flip/EqAndOrd.agda
@@ -12,7 +12,7 @@ open import Relation.Binary
 
 module Relation.Binary.Construct.Flip.EqAndOrd 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/NaturalOrder/Left.agda b/src/Relation/Binary/Construct/NaturalOrder/Left.agda
index db1d0f5aff..e0ab59e9ca 100644
--- a/src/Relation/Binary/Construct/NaturalOrder/Left.agda
+++ b/src/Relation/Binary/Construct/NaturalOrder/Left.agda
@@ -8,7 +8,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Core
-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/Relation/Binary/Construct/NaturalOrder/Right.agda b/src/Relation/Binary/Construct/NaturalOrder/Right.agda
index 7c4a6ab119..5278f0b116 100644
--- a/src/Relation/Binary/Construct/NaturalOrder/Right.agda
+++ b/src/Relation/Binary/Construct/NaturalOrder/Right.agda
@@ -8,7 +8,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Core using (Op₂)
-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/Relation/Binary/Core.agda b/src/Relation/Binary/Core.agda
index d9c19173a1..079bf296cc 100644
--- a/src/Relation/Binary/Core.agda
+++ b/src/Relation/Binary/Core.agda
@@ -10,7 +10,7 @@
 
 module Relation.Binary.Core where
 
-open import Data.Product using (_×_)
+open import Data.Product.Base using (_×_)
 open import Function.Base using (_on_)
 open import Level using (Level; _⊔_; suc)
 
diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda
index a44f2d058e..2ed315191b 100644
--- a/src/Relation/Binary/Definitions.agda
+++ b/src/Relation/Binary/Definitions.agda
@@ -13,7 +13,7 @@ module Relation.Binary.Definitions where
 open import Agda.Builtin.Equality using (_≡_)
 
 open import Data.Maybe.Base using (Maybe)
-open import Data.Product using (_×_)
+open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_on_; flip)
 open import Level
diff --git a/src/Relation/Binary/Lattice/Definitions.agda b/src/Relation/Binary/Lattice/Definitions.agda
index 61102f19f9..2cdc32a1c3 100644
--- a/src/Relation/Binary/Lattice/Definitions.agda
+++ b/src/Relation/Binary/Lattice/Definitions.agda
@@ -12,10 +12,10 @@
 module Relation.Binary.Lattice.Definitions where
 
 open import Algebra.Core
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Function.Base using (flip)
-open import Relation.Binary
-open import Level
+open import Relation.Binary.Core using (Rel)
+open import Level using (Level)
 
 private
   variable
diff --git a/src/Relation/Binary/Lattice/Structures.agda b/src/Relation/Binary/Lattice/Structures.agda
index 10178af05d..07dbfad6a5 100644
--- a/src/Relation/Binary/Lattice/Structures.agda
+++ b/src/Relation/Binary/Lattice/Structures.agda
@@ -19,7 +19,7 @@ module Relation.Binary.Lattice.Structures
 
 open import Algebra.Core
 open import Algebra.Definitions
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Level using (suc; _⊔_)
 
 open import Relation.Binary.Lattice.Definitions
diff --git a/src/Relation/Binary/Morphism/Structures.agda b/src/Relation/Binary/Morphism/Structures.agda
index 39a333e1b7..86eceac6e4 100644
--- a/src/Relation/Binary/Morphism/Structures.agda
+++ b/src/Relation/Binary/Morphism/Structures.agda
@@ -6,15 +6,15 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core
+open import Relation.Binary.Core using (Rel)
 
 module Relation.Binary.Morphism.Structures
   {a b} {A : Set a} {B : Set b}
   where
 
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Definitions
-open import Level
+open import Level using (Level; _⊔_)
 open import Relation.Binary.Morphism.Definitions A B
 
 private
diff --git a/src/Relation/Binary/Properties/Preorder.agda b/src/Relation/Binary/Properties/Preorder.agda
index 1a215b639c..e09bd0f3f1 100644
--- a/src/Relation/Binary/Properties/Preorder.agda
+++ b/src/Relation/Binary/Properties/Preorder.agda
@@ -11,8 +11,8 @@ open import Relation.Binary
 module Relation.Binary.Properties.Preorder
   {p₁ p₂ p₃} (P : Preorder p₁ p₂ p₃) where
 
-open import Function.Base
-open import Data.Product as Prod
+open import Function.Base using (flip)
+open import Data.Product.Base as Prod using (_×_; _,_; swap)
 import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
 
 open Preorder P
diff --git a/src/Relation/Binary/Properties/Setoid.agda b/src/Relation/Binary/Properties/Setoid.agda
index 137641d49b..cca28fb5ad 100644
--- a/src/Relation/Binary/Properties/Setoid.agda
+++ b/src/Relation/Binary/Properties/Setoid.agda
@@ -6,9 +6,9 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘_; id; _$_; flip)
-open import Relation.Nullary.Negation using (¬_)
+open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Binary
 
@@ -16,7 +16,6 @@ module Relation.Binary.Properties.Setoid {a ℓ} (S : Setoid a ℓ) where
 
 open Setoid S
 
-
 ------------------------------------------------------------------------------
 -- Every setoid is a preorder and partial order with respect to propositional
 -- equality
diff --git a/src/Relation/Binary/Properties/TotalOrder.agda b/src/Relation/Binary/Properties/TotalOrder.agda
index da4f316892..18e7095985 100644
--- a/src/Relation/Binary/Properties/TotalOrder.agda
+++ b/src/Relation/Binary/Properties/TotalOrder.agda
@@ -13,14 +13,12 @@ module Relation.Binary.Properties.TotalOrder
 
 open TotalOrder T
 
-open import Data.Product using (proj₁)
+open import Data.Product.Base using (proj₁)
 open import Data.Sum.Base using (inj₁; inj₂)
 import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
 import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict
 import Relation.Binary.Properties.Poset poset as PosetProperties
 open import Relation.Binary.Consequences
-open import Relation.Nullary.Negation using (¬_)
-open import Relation.Nullary.Negation using (contradiction)
 
 ------------------------------------------------------------------------
 -- Total orders are almost decidable total orders
diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda
index 4764635449..37c891312b 100644
--- a/src/Relation/Binary/PropositionalEquality.agda
+++ b/src/Relation/Binary/PropositionalEquality.agda
@@ -13,10 +13,9 @@ open import Axiom.UniquenessOfIdentityProofs
 open import Function.Base using (id; _∘_)
 open import Function.Equality using (Π; _⟶_; ≡-setoid)
 open import Level using (Level; _⊔_)
-open import Data.Product using (∃)
+open import Data.Product.Base using (∃)
 
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Decidable
+open import Relation.Nullary.Decidable using (yes; no; dec-yes-irr; dec-no)
 open import Relation.Binary
 open import Relation.Binary.Indexed.Heterogeneous
   using (IndexedSetoid)
@@ -132,4 +131,3 @@ Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/
 "Warning: inspect was deprecated in v2.0.
 Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality instead."
 #-}
-
diff --git a/src/Relation/Binary/PropositionalEquality/Core.agda b/src/Relation/Binary/PropositionalEquality/Core.agda
index 83c406b8aa..c0c4030b83 100644
--- a/src/Relation/Binary/PropositionalEquality/Core.agda
+++ b/src/Relation/Binary/PropositionalEquality/Core.agda
@@ -11,7 +11,7 @@
 
 module Relation.Binary.PropositionalEquality.Core where
 
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘_)
 open import Level
 open import Relation.Binary.Core
diff --git a/src/Relation/Binary/PropositionalEquality/Properties.agda b/src/Relation/Binary/PropositionalEquality/Properties.agda
index 0953c68cbd..ad936254ff 100644
--- a/src/Relation/Binary/PropositionalEquality/Properties.agda
+++ b/src/Relation/Binary/PropositionalEquality/Properties.agda
@@ -13,7 +13,7 @@
 module Relation.Binary.PropositionalEquality.Properties where
 
 open import Function.Base using (id; _∘_)
-open import Level
+open import Level using (Level)
 open import Relation.Binary
 import Relation.Binary.Properties.Setoid as Setoid
 open import Relation.Binary.PropositionalEquality.Core
diff --git a/src/Relation/Binary/Reasoning/Base/Double.agda b/src/Relation/Binary/Reasoning/Base/Double.agda
index f40a32bc9b..07761c5144 100644
--- a/src/Relation/Binary/Reasoning/Base/Double.agda
+++ b/src/Relation/Binary/Reasoning/Base/Double.agda
@@ -16,13 +16,13 @@ module Relation.Binary.Reasoning.Base.Double {a ℓ₁ ℓ₂} {A : Set a}
   {_≈_ : Rel A ℓ₁} {_∼_ : Rel A ℓ₂} (isPreorder : IsPreorder _≈_ _∼_)
   where
 
-open import Data.Product using (proj₁; proj₂)
+open import Data.Product.Base using (proj₁; proj₂)
 open import Level using (Level; _⊔_; Lift; lift)
 open import Function.Base using (case_of_; id)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; sym)
-open import Relation.Nullary.Decidable using (Dec; yes; no)
-open import Relation.Nullary.Decidable using (True; toWitness)
+open import Relation.Nullary.Decidable.Core
+  using (Dec; yes; no; True; toWitness)
 
 open IsPreorder isPreorder
 
diff --git a/src/Relation/Binary/Reasoning/Base/Triple.agda b/src/Relation/Binary/Reasoning/Base/Triple.agda
index 8e5ba6e159..c18aa9bf94 100644
--- a/src/Relation/Binary/Reasoning/Base/Triple.agda
+++ b/src/Relation/Binary/Reasoning/Base/Triple.agda
@@ -19,13 +19,13 @@ module Relation.Binary.Reasoning.Base.Triple {a ℓ₁ ℓ₂ ℓ₃} {A : Set a
   (<-≤-trans : Trans _<_ _≤_ _<_) (≤-<-trans : Trans _≤_ _<_ _<_)
   where
 
-open import Data.Product using (proj₁; proj₂)
+open import Data.Product.Base using (proj₁; proj₂)
 open import Function.Base using (case_of_; id)
 open import Level using (Level; _⊔_; Lift; lift)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; sym)
-open import Relation.Nullary.Decidable using (Dec; yes; no)
-open import Relation.Nullary.Decidable using (True; toWitness)
+open import Relation.Nullary.Decidable.Core
+  using (Dec; yes; no; True; toWitness)
 
 open IsPreorder isPreorder
   renaming
diff --git a/src/Relation/Binary/Reflection.agda b/src/Relation/Binary/Reflection.agda
index 8b682a0407..5a9ec838fb 100644
--- a/src/Relation/Binary/Reflection.agda
+++ b/src/Relation/Binary/Reflection.agda
@@ -7,12 +7,12 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.Fin.Base
-open import Data.Nat.Base
-open import Data.Vec.Base as Vec
-open import Function.Base
+open import Data.Fin.Base using (Fin)
+open import Data.Nat.Base using (ℕ)
+open import Data.Vec.Base as Vec using (Vec; allFin)
+open import Function.Base using (id; _⟨_⟩_)
 open import Function.Bundles using (module Equivalence)
-open import Level
+open import Level using (Level)
 open import Relation.Binary
 import Relation.Binary.PropositionalEquality as P
 
@@ -41,7 +41,7 @@ module Relation.Binary.Reflection
          where
 
 open import Data.Vec.N-ary
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 import Relation.Binary.Reasoning.Setoid as Eq
 
 open Setoid Sem
diff --git a/src/Relation/Binary/Structures.agda b/src/Relation/Binary/Structures.agda
index 058ca5135c..965e41691b 100644
--- a/src/Relation/Binary/Structures.agda
+++ b/src/Relation/Binary/Structures.agda
@@ -15,7 +15,7 @@ module Relation.Binary.Structures
   (_≈_ : Rel A ℓ)   -- The underlying equality relation
   where
 
-open import Data.Product using (proj₁; proj₂; _,_)
+open import Data.Product.Base using (proj₁; proj₂; _,_)
 open import Level using (Level; _⊔_)
 open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index a8970d9df5..b41a410391 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -11,7 +11,7 @@ module Relation.Nullary.Decidable where
 open import Level using (Level)
 open import Data.Bool.Base using (true; false; if_then_else_)
 open import Data.Empty using (⊥-elim)
-open import Data.Product as Prod hiding (map)
+open import Data.Product.Base as Prod hiding (map)
 open import Data.Sum.Base as Sum hiding (map)
 open import Function.Base
 open import Function.Bundles using
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index c8d92f9375..e06dc32239 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -16,7 +16,7 @@ open import Data.Bool.Base using (Bool; false; true; not; T; _∧_; _∨_)
 open import Data.Unit.Base using (⊤)
 open import Data.Empty using (⊥)
 open import Data.Empty.Irrelevant using (⊥-elim)
-open import Data.Product using (_×_)
+open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_∘_; const; _$_; flip)
 open import Relation.Nullary.Reflects
diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda
index 6f663e73ac..5111db897f 100644
--- a/src/Relation/Nullary/Negation.agda
+++ b/src/Relation/Nullary/Negation.agda
@@ -8,16 +8,15 @@
 
 module Relation.Nullary.Negation where
 
-open import Effect.Monad
+open import Effect.Monad using (RawMonad; mkRawMonad)
 open import Data.Bool.Base using (Bool; false; true; if_then_else_; not)
-open import Data.Empty
-open import Data.Product as Prod
+open import Data.Empty using (⊥-elim)
+open import Data.Product.Base as Prod using (_,_; Σ; Σ-syntax; ∃; curry; uncurry)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
-open import Function.Base
-open import Level
-open import Relation.Nullary.Negation.Core
-open import Relation.Nullary.Decidable.Core
-open import Relation.Unary
+open import Function.Base using (flip; _∘_; const; _∘′_)
+open import Level using (Level)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no; excluded-middle)
+open import Relation.Unary using (Universal)
 
 private
   variable
@@ -89,7 +88,7 @@ independence-of-premise : {R : Q → Set r} →
 independence-of-premise {P = P} q f = ¬¬-map helper excluded-middle
   where
   helper : Dec P → _
-  helper (yes p) = Prod.map id const (f p)
+  helper (yes p) = Prod.map₂ const (f p)
   helper (no ¬p) = (q , ⊥-elim ∘′ ¬p)
 
 -- The independence of premise rule for binary sums.
diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 76c064836b..f6d7cb13b0 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -8,12 +8,12 @@
 
 module Relation.Unary where
 
-open import Data.Empty
+open import Data.Empty using (⊥)
 open import Data.Unit.Base using (⊤)
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_; Σ-syntax; ∃; uncurry; swap)
 open import Data.Sum.Base using (_⊎_; [_,_])
-open import Function.Base
-open import Level
+open import Function.Base using (_∘_; _|>_)
+open import Level using (Level; _⊔_; 0ℓ; suc; Lift)
 open import Relation.Nullary.Decidable.Core using (Dec; True)
 open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
@@ -285,7 +285,7 @@ _⟨→⟩_ : Pred A ℓ₁ → Pred B ℓ₂ → Pred (A → B) _
 -- Product.
 
 _⟨·⟩_ : (P : Pred A ℓ₁) (Q : Pred B ℓ₂) →
-        (P ⟨×⟩ (P ⟨→⟩ Q)) ⊆ Q ∘ uncurry (flip _$_)
+        (P ⟨×⟩ (P ⟨→⟩ Q)) ⊆ Q ∘ uncurry _|>_
 (P ⟨·⟩ Q) (p , f) = f p
 
 -- Converse.
diff --git a/src/Relation/Unary/Closure/Base.agda b/src/Relation/Unary/Closure/Base.agda
index 5a210104b4..992e87df65 100644
--- a/src/Relation/Unary/Closure/Base.agda
+++ b/src/Relation/Unary/Closure/Base.agda
@@ -11,7 +11,7 @@ open import Relation.Binary
 module Relation.Unary.Closure.Base {a b} {A : Set a} (R : Rel A b) where
 
 open import Level
-open import Data.Product using (Σ-syntax; _×_; _,_; -,_)
+open import Data.Product.Base using (Σ-syntax; _×_; _,_; -,_)
 open import Function.Base using (flip)
 open import Relation.Unary using (Pred)
 
diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index e0b059f0b4..f30a9e59b4 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -8,10 +8,10 @@
 
 module Relation.Unary.Properties where
 
-open import Data.Product as Product using (_×_; _,_; swap; proj₁; zip′)
+open import Data.Product.Base as Product using (_×_; _,_; swap; proj₁; zip′)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Unit.Base using (tt)
-open import Level
+open import Level using (Level)
 open import Relation.Binary.Core as Binary
 open import Relation.Binary.Definitions hiding (Decidable; Universal; Irrelevant)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
diff --git a/src/Tactic/RingSolver.agda b/src/Tactic/RingSolver.agda
index 3ae3451e68..6441342e40 100644
--- a/src/Tactic/RingSolver.agda
+++ b/src/Tactic/RingSolver.agda
@@ -18,7 +18,7 @@ open import Data.Nat.Base              using (ℕ; suc; zero; _<ᵇ_)
 open import Data.Bool.Base             using (Bool; if_then_else_; true; false)
 open import Data.Unit.Base             using (⊤)
 open import Data.String.Base as String using (String; _++_; parens)
-open import Data.Product               using (_,_; proj₁)
+open import Data.Product.Base          using (_,_; proj₁)
 open import Function.Base
 open import Relation.Nullary.Decidable
 
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Base.agda b/src/Tactic/RingSolver/Core/Polynomial/Base.agda
index d762794b5e..6cfece2d45 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Base.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Base.agda
@@ -50,15 +50,15 @@ module Tactic.RingSolver.Core.Polynomial.Base
 
 open RawCoeff coeffs
 
-open import Data.Bool              using (Bool; true; false; T)
+open import Data.Bool.Base         using (Bool; true; false; T)
 open import Data.Empty             using (⊥)
 open import Data.Fin.Base as Fin        using (Fin; zero; suc)
 open import Data.List.Kleene
 open import Data.Nat.Base as ℕ          using (ℕ; suc; zero; _≤′_; compare; ≤′-refl; ≤′-step; _<′_)
 open import Data.Nat.Properties    using (z≤′n; ≤′-trans)
 open import Data.Nat.Induction
-open import Data.Product           using (_×_; _,_; map₁; curry; uncurry)
-open import Data.Unit              using (⊤; tt)
+open import Data.Product.Base      using (_×_; _,_; map₁; curry; uncurry)
+open import Data.Unit.Base         using (⊤; tt)
 open import Function.Base
 open import Relation.Nullary       using (¬_; Dec; yes; no)
 
diff --git a/src/Text/Pretty.agda b/src/Text/Pretty.agda
index 08c60701bf..0bdfe0cf2f 100644
--- a/src/Text/Pretty.agda
+++ b/src/Text/Pretty.agda
@@ -13,14 +13,14 @@ open import Data.Nat.Base using (ℕ)
 module Text.Pretty (width : ℕ) where
 
 import Level
-open import Data.Char.Base     using (Char)
+open import Data.Char.Base using (Char)
 open import Data.List.Base
   using (List; _∷_; []; [_]; uncons; _++_; map; filter)
 open import Data.List.NonEmpty as List⁺ using (foldr₁)
-open import Data.Maybe.Base    using (maybe′)
-open import Data.Product       using (uncurry)
-open import Data.String.Base   using (String; fromList; replicate)
-open import Function.Base
+open import Data.Maybe.Base using (maybe′)
+open import Data.Product.Base using (uncurry)
+open import Data.String.Base using (String; fromList; replicate)
+open import Function.Base using (_∘_; _∘′_; _$_)
 
 open import Effect.Monad using (RawMonad)
 import Data.List.Effectful as Cat
diff --git a/src/Text/Pretty/Core.agda b/src/Text/Pretty/Core.agda
index f546bc5962..a97db1dda2 100644
--- a/src/Text/Pretty/Core.agda
+++ b/src/Text/Pretty/Core.agda
@@ -17,7 +17,7 @@ open import Data.Irrelevant as Irrelevant using (Irrelevant) hiding (module Irre
 open import Data.List.Base as List   using (List; []; _∷_)
 open import Data.Nat.Base            using (ℕ; zero; suc; _+_; _⊔_; _≤_; z≤n)
 open import Data.Nat.Properties
-open import Data.Product as Prod using (_×_; _,_; uncurry; proj₁; proj₂)
+open import Data.Product.Base as Prod using (_×_; _,_; uncurry; proj₁; proj₂)
 import Data.Product.Relation.Unary.All as Allᴾ
 
 open import Data.Tree.Binary as Tree using (Tree; leaf; node; #nodes; mapₙ)
diff --git a/src/Text/Printf.agda b/src/Text/Printf.agda
index 7397f908f0..057b2718b8 100644
--- a/src/Text/Printf.agda
+++ b/src/Text/Printf.agda
@@ -8,17 +8,8 @@
 
 module Text.Printf where
 
-open import Level using (0ℓ; Lift)
-open import Data.List.Base as List using (List; []; _∷_)
-open import Data.Nat.Base using (ℕ)
-open import Data.Product
-open import Data.Product.Nary.NonDependent
-open import Data.String.Base
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Data.Unit using (⊤)
-open import Function.Nary.NonDependent
-open import Function
-open import Function.Strict
+open import Data.String.Base using (String; fromChar; concat)
+open import Function.Base using (id)
 
 import Data.Char.Base    as Cₛ
 import Data.Integer.Show as ℤₛ
diff --git a/src/Text/Regex/Base.agda b/src/Text/Regex/Base.agda
index 7fe7d56cbf..839bad4181 100644
--- a/src/Text/Regex/Base.agda
+++ b/src/Text/Regex/Base.agda
@@ -16,12 +16,9 @@ open import Data.Bool.Base using (Bool)
 open import Data.List.Base as L using (List; []; _∷_)
 open import Data.List.Relation.Unary.Any using (Any)
 open import Data.List.Relation.Unary.All using (All)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Data.Sum.Base using (_⊎_)
 
-open import Relation.Nullary.Negation using (¬_)
-open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Unary using (Pred)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary.Negation.Core using (¬_)
 
 open Preorder P using (_≈_) renaming (Carrier to A; _∼_ to _≤_)
 open import Data.List.Relation.Ternary.Appending.Propositional {A = A}