Simplify more Data.product imports

src/Codata/Guarded/Stream/Properties.agda

@@ -16,7 +16,7 @@ open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
 open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_)
 import Data.Nat.GeneralisedArithmetic as ℕ
-open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Base as Prod using (_×_; _,_; proj₁; proj₂)
 open import Data.Vec.Base as Vec using (Vec; _∷_)
 open import Function.Base using (const; flip; id; _∘′_; _$′_; _⟨_⟩_; _∘₂′_)
 open import Level using (Level)

src/Codata/Guarded/Stream/Relation/Unary/All.agda

@@ -9,7 +9,7 @@
 module Codata.Guarded.Stream.Relation.Unary.All where
 
 open import Codata.Guarded.Stream using (Stream; head; tail)
-open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Level
 open import Relation.Unary
 

src/Codata/Musical/Covec.agda

@@ -14,7 +14,7 @@ open import Codata.Musical.Cofin using (Cofin; zero; suc)
 open import Codata.Musical.Colist as Colist using (Colist; []; _∷_)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Vec.Base using (Vec; []; _∷_)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_∋_)
 open import Level using (Level)
 open import Relation.Binary

src/Codata/Sized/Colist.agda

@@ -12,7 +12,7 @@ open import Level using (Level)
 open import Size
 open import Data.Unit.Base
 open import Data.Nat.Base
-open import Data.Product using (_×_ ; _,_)
+open import Data.Product.Base using (_×_ ; _,_)
 open import Data.These.Base using (These; this; that; these)
 open import Data.Maybe.Base using (Maybe; nothing; just)
 open import Data.List.Base using (List; []; _∷_)

src/Codata/Sized/Colist/Properties.agda

@@ -27,7 +27,7 @@ open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
 import Data.Maybe.Properties as Maybeₚ
 open import Data.Maybe.Relation.Unary.All using (All; nothing; just)
 open import Data.Nat.Base as ℕ using (zero; suc; z≤n; s≤s)
-open import Data.Product as Prod using (_×_; _,_; uncurry)
+open import Data.Product.Base as Prod using (_×_; _,_; uncurry)
 open import Data.These.Base as These using (These; this; that; these)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Function.Base

src/Codata/Sized/M/Bisimilarity.agda

@@ -14,7 +14,7 @@ open import Codata.Sized.Thunk
 open import Codata.Sized.M
 open import Data.Container.Core
 open import Data.Container.Relation.Binary.Pointwise using (Pointwise; _,_)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_∋_)
 open import Relation.Binary
 import Relation.Binary.PropositionalEquality.Core as P

src/Codata/Sized/M/Properties.agda

@@ -15,7 +15,7 @@ open import Codata.Sized.M
 open import Codata.Sized.M.Bisimilarity
 open import Data.Container.Core as C hiding (map)
 import Data.Container.Morphism as Mp
-open import Data.Product as Prod using (_,_)
+open import Data.Product.Base as Prod using (_,_)
 open import Data.Product.Properties hiding (map-cong)
 open import Function.Base using (_$′_; _∘′_)
 import Relation.Binary.PropositionalEquality.Core as P

src/Codata/Sized/Stream/Effectful.agda

@@ -8,7 +8,7 @@
 
 module Codata.Sized.Stream.Effectful where
 
-open import Data.Product using (<_,_>)
+open import Data.Product.Base using (<_,_>)
 open import Codata.Sized.Stream
 open import Effect.Functor
 open import Effect.Applicative

src/Codata/Sized/Stream/Properties.agda

@@ -20,7 +20,7 @@ open import Data.Nat.GeneralisedArithmetic using (fold; fold-pull)
 open import Data.List.Base as List using ([]; _∷_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
 import Data.List.Relation.Binary.Equality.Propositional as Eq
-open import Data.Product as Prod using (_,_)
+open import Data.Product.Base as Prod using (_,_)
 open import Data.Vec.Base as Vec using (_∷_)
 
 open import Function.Base using (id; _$_; _∘′_; const)

src/Data/AVL/IndexedMap.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.Product as Prod
+open import Data.Product.Base using (∃)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst)
 import Data.Tree.AVL.Value

src/Data/Char/Properties.agda

@@ -12,7 +12,7 @@ open import Data.Bool.Base using (Bool)
 open import Data.Char.Base
 import Data.Nat.Base as ℕ
 import Data.Nat.Properties as ℕₚ
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 
 open import Function.Base
 open import Relation.Nullary using (¬_; yes; no)

src/Data/Digit/Properties.agda

@@ -11,7 +11,7 @@ import Data.Char.Properties as Charₚ
 open import Data.Nat.Base using (ℕ)
 open import Data.Nat.Properties using (_≤?_)
 open import Data.Fin.Properties using (inject≤-injective)
-open import Data.Product using (_,_; proj₁)
+open import Data.Product.Base using (_,_; proj₁)
 open import Data.Vec.Relation.Unary.Unique.Propositional using (Unique)
 import Data.Vec.Relation.Unary.Unique.Propositional.Properties as Uniqueₚ
 open import Data.Vec.Relation.Unary.AllPairs using (allPairs?)

src/Data/Fin/Induction.agda

@@ -13,7 +13,7 @@ open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _∸_; s≤s)
 open import Data.Nat.Properties using (n<1+n; ≤⇒≯)
 import Data.Nat.Induction as ℕ
 import Data.Nat.Properties as ℕ
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Data.Vec.Relation.Unary.Linked as Linked using (Linked; [-]; _∷_)
 import Data.Vec.Relation.Unary.Linked.Properties as Linkedₚ

src/Data/Fin/Permutation.agda

@@ -15,7 +15,7 @@ open import Data.Fin.Patterns
 open import Data.Fin.Properties
 import Data.Fin.Permutation.Components as PC
 open import Data.Nat.Base using (ℕ; suc; zero)
-open import Data.Product using (_,_; proj₂)
+open import Data.Product.Base using (_,_; proj₂)
 open import Function.Bundles using (_↔_; Injection; Inverse; mk↔′)
 open import Function.Construct.Composition using (_↔-∘_)
 open import Function.Construct.Identity using (↔-id)

src/Data/Fin/Permutation/Components.agda

@@ -13,7 +13,7 @@ open import Data.Fin.Base
 open import Data.Fin.Properties
 open import Data.Nat.Base as ℕ using (zero; suc; _∸_)
 import Data.Nat.Properties as ℕₚ
-open import Data.Product using (proj₂)
+open import Data.Product.Base using (proj₂)
 open import Function.Base using (_∘_)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary using (does; _because_; yes; no)

src/Data/Fin/Permutation/Transposition/List.agda

@@ -14,7 +14,7 @@ open import Data.Fin.Permutation as P hiding (lift₀)
 import Data.Fin.Permutation.Components as PC
 open import Data.List.Base using (List; []; _∷_; map)
 open import Data.Nat.Base using (ℕ; suc; zero)
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Function.Base using (_∘_)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; sym; cong; module ≡-Reasoning)

src/Data/Integer/Properties.agda

@@ -21,11 +21,10 @@ open import Data.Nat as ℕ
   hiding (module ℕ)
 import Data.Nat.Properties as ℕ
 open import Data.Nat.Solver
-open import Data.Product using (proj₁; proj₂; _,_)
+open import Data.Product.Base using (proj₁; proj₂; _,_; _×_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Sign as Sign using (Sign) renaming (_*_ to _𝕊*_)
 import Data.Sign.Properties as 𝕊ₚ
-open import Data.Product using (_×_)
 open import Function.Base using (_∘_; _$_; id)
 open import Level using (0ℓ)
 open import Relation.Binary

src/Data/List/Extrema/Core.agda

@@ -15,7 +15,7 @@ open import Algebra.Core
 open import Algebra.Definitions
 import Algebra.Construct.NaturalChoice.Min as Min
 import Algebra.Construct.NaturalChoice.Max as Max
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)

src/Data/List/Extrema/Nat.agda

@@ -18,7 +18,7 @@ open import Data.List.Base using (List)
 import Data.List.Extrema
 open import Data.List.Relation.Unary.Any as Any using (Any)
 open import Data.List.Relation.Unary.All as All using (All)
-open import Data.Product using (_×_; _,_; uncurry′)
+open import Data.Product.Base using (_×_; _,_; uncurry′)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core using (_≢_)
 

src/Data/List/Fresh/Properties.agda

@@ -9,7 +9,7 @@
 module Data.List.Fresh.Properties where
 
 open import Level using (Level; _⊔_; Lift)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Relation.Nullary
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary as B using (Rel)

src/Data/List/Fresh/Relation/Unary/All.agda

@@ -9,7 +9,7 @@
 module Data.List.Fresh.Relation.Unary.All where
 
 open import Level using (Level; _⊔_; Lift)
-open import Data.Product using (_×_; _,_; proj₁; uncurry)
+open import Data.Product.Base using (_×_; _,_; proj₁; uncurry)
 open import Data.Sum.Base as Sum using (inj₁; inj₂)
 open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_)
 open import Relation.Unary  as U

src/Data/List/Fresh/Relation/Unary/All/Properties.agda

@@ -11,7 +11,7 @@ module Data.List.Fresh.Relation.Unary.All.Properties where
 open import Level using (Level; _⊔_; Lift)
 open import Data.Empty
 open import Data.Nat.Base using (ℕ; zero; suc)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘′_)
 open import Relation.Nullary
 open import Relation.Unary  as U

src/Data/List/Fresh/Relation/Unary/Any/Properties.agda

@@ -12,7 +12,7 @@ open import Level using (Level; _⊔_; Lift)
 open import Data.Bool.Base using (true; false)
 open import Data.Empty
 open import Data.Nat.Base using (ℕ; zero; suc)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘′_)
 open import Relation.Nullary.Reflects using (invert)

src/Data/List/Nary/NonDependent.agda

@@ -10,7 +10,7 @@ module Data.List.Nary.NonDependent where
 
 open import Data.Nat.Base using (zero; suc)
 open import Data.List.Base as List using (List; []; _∷_)
-open import Data.Product as Prod using (_,_)
+open import Data.Product.Base as Prod using (_,_)
 open import Data.Product.Nary.NonDependent using (Product)
 open import Function.Base using ()
 open import Function.Nary.NonDependent.Base

src/Data/List/NonEmpty/Effectful.agda

@@ -11,7 +11,7 @@ module Data.List.NonEmpty.Effectful where
 open import Agda.Builtin.List
 import Data.List.Effectful as List
 open import Data.List.NonEmpty.Base
-open import Data.Product using (uncurry)
+open import Data.Product.Base using (uncurry)
 open import Effect.Functor
 open import Effect.Applicative
 open import Effect.Monad

src/Data/List/Relation/Binary/Disjoint/Setoid.agda

@@ -15,7 +15,7 @@ open import Relation.Nullary.Negation using (¬_)
 open import Function.Base using (_∘_)
 open import Data.List.Base using (List; []; [_]; _∷_)
 open import Data.List.Relation.Unary.Any using (here; there)
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 
 open Setoid S renaming (Carrier to A)
 open import Data.List.Membership.Setoid S using (_∈_; _∉_)

src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda

@@ -14,7 +14,7 @@ import Data.List.Relation.Unary.Any as Any
 open import Data.List.Relation.Unary.All as All
 open import Data.List.Relation.Unary.All.Properties using (¬Any⇒All¬)
 open import Data.List.Relation.Unary.Any.Properties using (++⁻)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Relation.Binary
 open import Relation.Nullary.Negation using (¬_)

src/Data/List/Relation/Binary/Lex/Strict.agda

@@ -14,7 +14,7 @@ module Data.List.Relation.Binary.Lex.Strict where
 open import Data.Empty using (⊥)
 open import Data.Unit.Base using (⊤; tt)
 open import Function.Base using (_∘_; id)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.List.Base using (List; []; _∷_)
 open import Level using (_⊔_)

src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda

@@ -13,7 +13,7 @@ open import Algebra.Definitions
 open import Algebra.Structures
 open import Data.Bool.Base using (Bool; true; false)
 open import Data.Nat using (suc)
-open import Data.Product using (-,_; proj₂)
+open import Data.Product.Base using (-,_; proj₂)
 open import Data.List.Base as List
 open import Data.List.Relation.Binary.Permutation.Propositional
 open import Data.List.Relation.Unary.Any using (Any; here; there)

src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda

@@ -19,7 +19,7 @@ open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
 open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix hiding (PrefixView; _++_)
 open import Data.Nat.Base using (ℕ; zero; suc; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (suc-injective)
-open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂; uncurry)
+open import Data.Product.Base as Prod using (_×_; _,_; proj₁; proj₂; uncurry)
 open import Function.Base
 
 open import Relation.Nullary.Negation using (¬_)