Simplify more Data.Product imports to Data.Product.Base (#2036)

* Simplify more `Data.Product` import to `Data.Product.Base`

* Simplify more `Data.Product` import to `Data.Product.Base`

* Indent

src/Function/Endomorphism/Propositional.agda

@@ -16,7 +16,7 @@ open import Algebra.Morphism; open Definitions
 
 open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Data.Nat.Properties using (+-0-monoid; +-semigroup)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 
 open import Function.Base using (id; _∘′_; _∋_)
 open import Function.Equality using (_⟨$⟩_)

src/Function/Nary/NonDependent.agda

@@ -17,7 +17,7 @@ module Function.Nary.NonDependent where
 open import Level using (Level; 0ℓ; _⊔_; Lift)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Fin.Base using (Fin; zero; suc)
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.Product.Nary.NonDependent
 open import Function.Base using (_∘′_; _$′_; const; flip)
 open import Relation.Unary using (IUniversal)

src/Function/Properties/Bijection.agda

@@ -13,7 +13,7 @@ open import Level using (Level)
 open import Relation.Binary hiding (_⇔_)
 import Relation.Binary.PropositionalEquality.Properties as P
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
-open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Function.Base using (_∘_)
 open import Function.Properties.Inverse using (Inverse⇒Equivalence)
 

src/Function/Related.agda

@@ -20,7 +20,7 @@ open import Function.Surjection as Surj using (Surjection)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as P
-open import Data.Product using (_,_; proj₁; proj₂; <_,_>)
+open import Data.Product.Base using (_,_; proj₁; proj₂; <_,_>)
 
 import Function.Related.Propositional as R
 import Function.Bundles as B

src/Function/Related/TypeIsomorphisms/Solver.agda

@@ -13,7 +13,7 @@ module Function.Related.TypeIsomorphisms.Solver where
 open import Algebra using (CommutativeSemiring)
 import Algebra.Solver.Ring.NaturalCoefficients.Default
 open import Data.Empty.Polymorphic using (⊥)
-open import Data.Product using (_×_)
+open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
 open import Data.Unit.Polymorphic using (⊤)
 open import Level using (Level)

src/Reflection/AST/Abstraction.agda

@@ -8,7 +8,7 @@
 
 module Reflection.AST.Abstraction where
 
-open import Data.Product  using (_×_; <_,_>; uncurry)
+open import Data.Product.Base using (_×_; <_,_>; uncurry)
 open import Data.String as String using (String)
 open import Level
 open import Relation.Nullary.Decidable using (Dec; map′; _×-dec_)

src/Reflection/AST/Argument.agda

@@ -9,7 +9,7 @@
 module Reflection.AST.Argument where
 
 open import Data.List.Base as List using (List; []; _∷_)
-open import Data.Product  using (_×_; <_,_>; uncurry)
+open import Data.Product.Base using (_×_; <_,_>; uncurry)
 open import Relation.Nullary.Decidable using (Dec; map′; _×-dec_)
 open import Relation.Binary using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)

src/Reflection/AST/Definition.agda

@@ -10,7 +10,7 @@ module Reflection.AST.Definition where
 
 import Data.List.Properties as Listₚ using (≡-dec)
 import Data.Nat.Properties as ℕₚ using (_≟_)
-open import Data.Product  using (_×_; <_,_>; uncurry)
+open import Data.Product.Base using (_×_; <_,_>; uncurry)
 open import Relation.Nullary.Decidable using (map′; _×-dec_; yes; no)
 open import Relation.Binary using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)

src/Reflection/AST/Show.agda

@@ -15,7 +15,7 @@ import Data.Char as Char using (show)
 import Data.Float as Float using (show)
 open import Data.List.Base hiding (_++_; intersperse)
 import Data.Nat.Show as ℕ using (show)
-open import Data.Product  using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.String as String
  using (String; _++_; intersperse; braces; parens; parensIfSpace; _<+>_)
 import Data.Word as Word using (toℕ)

src/Reflection/AST/Term.agda

@@ -10,8 +10,8 @@ module Reflection.AST.Term where
 
 open import Data.List.Base as List hiding (_++_)
 open import Data.List.Properties using (∷-dec)
-open import Data.Nat as ℕ using (ℕ; zero; suc)
-open import Data.Product  using (_×_; _,_; <_,_>; uncurry; map₁)
+open import Data.Nat as ℕ  using (ℕ; zero; suc)
+open import Data.Product.Base using (_×_; _,_; <_,_>; uncurry; map₁)
 open import Data.Product.Properties using (,-injective)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.String as String using (String)

src/Reflection/AST/Traversal.agda

@@ -13,7 +13,7 @@ module Reflection.AST.Traversal
 
 open import Data.Nat using (ℕ; zero; suc; _+_)
 open import Data.List.Base using (List; []; _∷_; _++_; reverse; length)
-open import Data.Product  using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.String using (String)
 open import Function.Base using (_∘_)
 open import Reflection hiding (pure)

src/Reflection/AST/Universe.agda

@@ -10,7 +10,7 @@ module Reflection.AST.Universe where
 
 open import Data.List.Base using (List)
 open import Data.String.Base using (String)
-open import Data.Product  using (_×_)
+open import Data.Product.Base using (_×_)
 open import Reflection.AST.Argument using (Arg)
 open import Reflection.AST.Abstraction using (Abs)
 open import Reflection.AST.Term using (Term; Pattern; Sort; Clause)

src/Reflection/AnnotatedAST.agda

@@ -17,7 +17,7 @@ open import Effect.Applicative using (RawApplicative)
 open import Data.Bool.Base using (Bool; false; true; if_then_else_)
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.Relation.Unary.All using (All; _∷_; [])
-open import Data.Product  using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Data.String.Base using (String)
 
 open import Reflection hiding (pure)

src/Reflection/AnnotatedAST/Free.agda

@@ -12,7 +12,7 @@ open import Data.Bool.Base using (if_then_else_)
 open import Data.Nat.Base using (ℕ; _∸_; compare; _<ᵇ_; less; equal; greater)
 open import Data.List.Base using (List; []; _∷_; [_]; concatMap; length)
 open import Data.List.Relation.Unary.All using (_∷_)
-open import Data.Product  using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Data.String.Base using (String)
 
 open import Reflection

src/Reflection/External.agda

@@ -12,7 +12,7 @@ import Agda.Builtin.Reflection.External as Builtin
 
 open import Data.Nat.Base using (ℕ; suc; zero; NonZero)
 open import Data.List.Base using (List; _∷_; [])
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.String.Base as String using (String; _++_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Unit.Base using (⊤; tt)

src/Relation/Binary/Construct/Subst/Equality.agda

@@ -9,7 +9,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.Product as Prod
+open import Data.Product.Base as Prod
 open import Relation.Binary
 
 module Relation.Binary.Construct.Subst.Equality

src/Relation/Binary/Indexed/Homogeneous/Bundles.agda

@@ -11,7 +11,7 @@
 
 module Relation.Binary.Indexed.Homogeneous.Bundles where
 
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_⟨_⟩_)
 open import Level using (Level; _⊔_; suc)
 open import Relation.Binary.Core using (_⇒_; Rel)

src/Relation/Binary/Indexed/Homogeneous/Core.agda

@@ -12,7 +12,7 @@
 module Relation.Binary.Indexed.Homogeneous.Core where
 
 open import Level using (Level; _⊔_)
-open import Data.Product using (_×_)
+open import Data.Product.Base using (_×_)
 open import Relation.Binary.Core as B using (REL; Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 import Relation.Binary.Indexed.Heterogeneous as I

src/Relation/Binary/Indexed/Homogeneous/Definitions.agda

@@ -11,7 +11,7 @@
 
 module Relation.Binary.Indexed.Homogeneous.Definitions where
 
-open import Data.Product using (_×_)
+open import Data.Product.Base using (_×_)
 open import Level using (Level)
 import Relation.Binary as B
 open import Relation.Unary.Indexed using (IPred)

src/Relation/Binary/Indexed/Homogeneous/Structures.agda

@@ -17,7 +17,7 @@ module Relation.Binary.Indexed.Homogeneous.Structures
  (_≈ᵢ_ : IRel A ℓ) -- The underlying indexed equality relation
  where
 
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_⟨_⟩_)
 open import Level using (Level; _⊔_; suc)
 open import Relation.Binary.Core using (_⇒_)

src/Relation/Binary/Lattice/Properties/BoundedLattice.agda

@@ -14,7 +14,7 @@ module Relation.Binary.Lattice.Properties.BoundedLattice
 open BoundedLattice L
 
 open import Algebra.Definitions _≈_
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Lattice.Properties.MeetSemilattice meetSemilattice
 open import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice

src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda

@@ -14,7 +14,7 @@ module Relation.Binary.Lattice.Properties.DistributiveLattice
 open DistributiveLattice L hiding (refl)
 
 open import Algebra.Definitions _≈_
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Relation.Binary
 open import Relation.Binary.Reasoning.Setoid setoid
 open import Relation.Binary.Lattice.Properties.Lattice lattice

src/Relation/Binary/Lattice/Properties/Lattice.agda

@@ -16,7 +16,7 @@ open Lattice L
 import Algebra.Lattice as Alg
 import Algebra.Structures as Alg
 open import Algebra.Definitions _≈_
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (flip)
 open import Relation.Binary
 open import Relation.Binary.Properties.Poset poset

src/Relation/Binary/Morphism/Construct/Identity.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
 open import Level using (Level)
 open import Relation.Binary

src/Relation/Binary/Morphism/OrderMonomorphism.agda

@@ -11,7 +11,7 @@
 
 open import Algebra.Morphism.Definitions
 open import Function.Base
-open import Data.Product using (_,_; map)
+open import Data.Product.Base using (_,_; map)
 open import Relation.Binary
 open import Relation.Binary.Morphism
 import Relation.Binary.Morphism.RelMonomorphism as RawRelation

src/Relation/Binary/Properties/HeytingAlgebra.agda

@@ -15,7 +15,7 @@ open HeytingAlgebra L
 
 open import Algebra.Core
 open import Algebra.Definitions _≈_
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_$_; flip; _∘_)
 open import Level using (_⊔_)
 open import Relation.Binary

src/Relation/Nary.agda

@@ -19,7 +19,7 @@ open import Data.Unit.Base
 open import Data.Bool.Base using (true; false)
 open import Data.Empty
 open import Data.Nat.Base using (zero; suc)
-open import Data.Product as Prod using (_×_; _,_)
+open import Data.Product.Base as Prod using (_×_; _,_)
 open import Data.Product.Nary.NonDependent
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_$_; _∘′_)

src/Relation/Nullary/Universe.agda

@@ -19,7 +19,7 @@ import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
  as Trivial
 open import Data.Sum.Base as Sum hiding (map)
 open import Data.Sum.Relation.Binary.Pointwise
-open import Data.Product as Prod hiding (map)
+open import Data.Product.Base as Prod hiding (map)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Function.Base using (_∘_; id)
 import Function.Equality as FunS

src/Relation/Unary/Algebra.agda

@@ -14,7 +14,7 @@ open import Algebra.Lattice.Bundles
 import Algebra.Lattice.Structures as AlgebraicLatticeStructures
 import Algebra.Structures as AlgebraicStructures
 open import Data.Empty.Polymorphic using (⊥-elim)
-open import Data.Product as Product using (_,_; proj₁; proj₂; <_,_>; curry; uncurry)
+open import Data.Product.Base as Product using (_,_; proj₁; proj₂; <_,_>; curry; uncurry)
 open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
 open import Data.Unit.Polymorphic using (tt)
 open import Function.Base using (id; const; _∘_)

src/System/Environment.agda

@@ -11,7 +11,7 @@ module System.Environment where
 open import IO using (IO; lift; run; ignore)
 open import Data.List.Base using (List)
 open import Data.Maybe.Base using (Maybe)
-open import Data.Product using (_×_)
+open import Data.Product.Base using (_×_)
 open import Data.String.Base using (String)
 open import Data.Unit.Polymorphic using (⊤)
 open import Foreign.Haskell.Coerce

src/System/FilePath/Posix.agda

@@ -13,7 +13,7 @@ open import Agda.Builtin.List using (List)
 open import Agda.Builtin.String using (String)
 open import IO.Base using (IO; lift)
 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 Foreign.Haskell.Coerce

src/System/Process.agda

@@ -10,7 +10,7 @@ module System.Process where
 
 open import Level using (Level)
 open import Data.List.Base using (List)
-open import Data.Product using (_×_; proj₁)
+open import Data.Product.Base using (_×_; proj₁)
 open import Data.String.Base using (String)
 open import Data.Unit.Polymorphic using (⊤)
 open import Foreign.Haskell.Coerce

src/Tactic/MonoidSolver.agda

@@ -79,7 +79,7 @@ open import Data.Bool as Bool using (Bool; _∨_; if_then_else_)
 open import Data.Maybe as Maybe using (Maybe; just; nothing; maybe)
 open import Data.List.Base as List using (List; _∷_; [])
 open import Data.Nat as ℕ using (ℕ; suc; zero)
-open import Data.Product  as Product using (_×_; _,_)
+open import Data.Product.Base as Product using (_×_; _,_)
 
 open import Reflection.AST
 open import Reflection.AST.Term

src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda

@@ -15,7 +15,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Addition
 
 open import Data.Nat as ℕ using (ℕ; suc; zero; compare; _≤′_; ≤′-step; ≤′-refl)
 open import Data.Nat.Properties as ℕₚ using (≤′-trans)
-open import Data.Product  using (_,_; _×_; proj₂)
+open import Data.Product.Base using (_,_; _×_; proj₂)
 open import Data.List.Base using (_∷_; [])
 open import Data.List.Kleene
 open import Data.Vec using (Vec)

src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda

@@ -16,7 +16,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Exponentiation
 open import Function.Base using (_⟨_⟩_)
 
 open import Data.Nat.Base as ℕ using (ℕ; suc; zero; compare)
-open import Data.Product using (_,_; _×_; proj₁; proj₂)
+open import Data.Product.Base using (_,_; _×_; proj₁; proj₂)
 open import Data.List.Kleene
 open import Data.Vec using (Vec)
 

src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda

@@ -21,7 +21,7 @@ open import Data.Fin using (Fin; zero; su
 open import Data.List.Base using (_∷_; [])
 open import Data.Unit using (tt)
 open import Data.List.Kleene
-open import Data.Product  using (_,_; proj₁; proj₂; map₁; _×_)
+open import Data.Product.Base using (_,_; proj₁; proj₂; map₁; _×_)
 open import Data.Maybe using (nothing; just)
 open import Function.Base using (_⟨_⟩_)
 open import Level using (lift)

src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda

@@ -16,7 +16,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Multiplication
 open import Data.Nat.Base as ℕ using (ℕ; suc; zero; _<′_; _≤′_; ≤′-step; ≤′-refl)
 open import Data.Nat.Properties using (≤′-trans)
 open import Data.Nat.Induction
-open import Data.Product  using (_×_; _,_; proj₁; proj₂; map₁)
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; map₁)
 open import Data.List.Kleene
 open import Data.Vec using (Vec)
 open import Function.Base using (_⟨_⟩_; flip)

src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda

@@ -13,7 +13,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Negation
  (homo : Homomorphism r₁ r₂ r₃ r₄)
  where
 
-open import Data.Product  using (_,_)
+open import Data.Product.Base using (_,_)
 open import Data.Vec using (Vec)
 open import Data.Nat using (_<′_)
 open import Data.Nat.Induction

src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Variables.agda

@@ -13,7 +13,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Variables
  (homo : Homomorphism r₁ r₂ r₃ r₄)
  where
 
-open import Data.Product  using (_,_)
+open import Data.Product.Base using (_,_)
 open import Data.Vec.Base as Vec using (Vec)
 open import Data.Fin using (Fin)
 open import Data.List.Kleene

src/Tactic/RingSolver/Core/Polynomial/Semantics.agda

@@ -16,7 +16,7 @@ module Tactic.RingSolver.Core.Polynomial.Semantics
 open import Data.Nat using (ℕ; suc; zero; _≤′_; ≤′-step; ≤′-refl)
 open import Data.Vec using (Vec; []; _∷_; uncons)
 open import Data.List.Base using ([]; _∷_)
-open import Data.Product  using (_,_; _×_)
+open import Data.Product.Base using (_,_; _×_)
 open import Data.List.Kleene using (_+; _*; ∹_; _&_; [])
 
 open Homomorphism homo hiding (_^_)

src/Test/Golden.agda

@@ -89,7 +89,7 @@ open import Data.List.Relation.Unary.Any using (any?)
 open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe)
 open import Data.Nat.Base using (ℕ; _≡ᵇ_; _<ᵇ_; _+_; _∸_)
 import Data.Nat.Show as ℕ using (show)
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.String as String using (String; lines; unlines; unwords; concat; _≟_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Unit.Base using (⊤)

src/Text/Regex/Properties/Core.agda

@@ -17,7 +17,7 @@ open import Data.List.Base as List using (List; []; _∷_; _++_)
 
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 
 open import Relation.Nullary using (¬_; Dec; yes; no)

src/Text/Tabular/List.agda

@@ -11,7 +11,7 @@ module Text.Tabular.List where
 open import Data.String using (String)
 open import Data.List.Base
 import Data.Nat.Properties as ℕₚ
-open import Data.Product using (-,_; proj₂)
+open import Data.Product.Base using (-,_; proj₂)
 open import Data.Vec.Base as Vec using (Vec)
 open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤)
 open import Function.Base

src/Text/Tabular/Vec.agda

@@ -9,7 +9,7 @@
 module Text.Tabular.Vec where
 
 open import Data.List.Base using (List)
-open import Data.Product as Prod using (uncurry)
+open import Data.Product.Base as Prod using (uncurry)
 open import Data.String using (String; rectangle; fromAlignment)
 open import Data.Vec.Base
 open import Function.Base