Simplify Data.Product imports

README/Data/Container/FreeMonad.agda

@@ -16,7 +16,7 @@ open import Data.Unit
 open import Data.Bool.Base using (Bool; true)
 open import Data.Nat
 open import Data.Sum using (inj₁; inj₂)
-open import Data.Product renaming (_×_ to _⟨×⟩_)
+open import Data.Product.Base renaming (_×_ to _⟨×⟩_)
 open import Data.Container using (Container; _▷_)
 open import Data.Container.Combinator
 open import Data.Container.FreeMonad as FreeMonad

src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda

@@ -11,7 +11,7 @@ open import Algebra.Apartness.Bundles using (HeytingCommutativeRing)
 module Algebra.Apartness.Properties.HeytingCommutativeRing
   {c ℓ₁ ℓ₂} (HCR : HeytingCommutativeRing c ℓ₁ ℓ₂) where
 
-open import Data.Product using (_,_; proj₂)
+open import Data.Product.Base using (_,_; proj₂)
 open import Algebra using (CommutativeRing; RightIdentity)
 
 open HeytingCommutativeRing HCR

src/Algebra/Construct/Add/Identity.agda

@@ -14,7 +14,7 @@ open import Algebra.Core using (Op₂)
 open import Algebra.Definitions
 open import Algebra.Structures
 open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions

src/Algebra/Construct/Flip/Op.agda

@@ -10,7 +10,7 @@
 module Algebra.Construct.Flip.Op where
 
 open import Algebra
-import Data.Product as Prod
+import Data.Product.Base as Prod
 import Data.Sum as Sum
 open import Function.Base using (flip)
 open import Level using (Level)

src/Algebra/Construct/LexProduct/Inner.agda

@@ -8,7 +8,7 @@
 
 open import Algebra
 open import Data.Bool.Base using (false; true)
-open import Data.Product using (_×_; _,_; swap; map; uncurry′)
+open import Data.Product.Base using (_×_; _,_; swap; map; uncurry′)
 open import Function.Base using (_∘_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Definitions using (Decidable)

src/Algebra/Construct/LiftedChoice.agda

@@ -14,7 +14,7 @@ open import Algebra.Consequences.Base
 open import Relation.Binary
 open import Relation.Nullary using (¬_; yes; no)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Unary using (Pred)

src/Algebra/Construct/NaturalChoice/Min.agda

@@ -10,7 +10,7 @@ open import Algebra.Core
 open import Algebra.Bundles
 open import Algebra.Construct.NaturalChoice.Base
 open import Data.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
 import Algebra.Construct.NaturalChoice.MinOp as MinOp

src/Algebra/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.Core
 
 module Algebra.Construct.Subst.Equality

src/Algebra/Lattice/Morphism/Construct/Identity.agda

@@ -11,7 +11,7 @@ module Algebra.Lattice.Morphism.Construct.Identity where
 open import Algebra.Lattice.Bundles
 open import Algebra.Lattice.Morphism.Structures
   using ( module LatticeMorphisms )
-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.Morphism.Construct.Identity using (isRelHomomorphism)

src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda

@@ -15,7 +15,7 @@ open import Algebra.Lattice.Morphism.Structures
 import Algebra.Consequences.Setoid as Consequences
 import Algebra.Morphism.MagmaMonomorphism as MagmaMonomorphisms
 import Algebra.Lattice.Properties.Lattice as LatticeProperties
-open import Data.Product using (_,_; map)
+open import Data.Product.Base using (_,_; map)
 open import Relation.Binary
 import Relation.Binary.Morphism.RelMonomorphism as RelMonomorphisms
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning

src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda

@@ -18,7 +18,7 @@ open import Effect.Applicative as Applicative
 open import Effect.Monad
 open import Data.Fin.Base using (Fin)
 open import Data.Nat.Base
-open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Data.Vec.Base as Vec using (Vec)
 import Data.Vec.Effectful as VecCat
 import Function.Identity.Effectful as IdCat

src/Algebra/Lattice/Structures/Biased.agda

@@ -14,7 +14,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)
 

src/Algebra/Module/Morphism/Construct/Identity.agda

@@ -21,7 +21,7 @@ open import Algebra.Module.Morphism.Structures
         ; module ModuleMorphisms
         )
 open import Algebra.Morphism.Construct.Identity
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
 open import Level using (Level)
 

src/Algebra/Module/Structures.agda

@@ -16,7 +16,7 @@ open import Algebra.Module.Core
 import Algebra.Definitions as Defs
 open import Algebra.Module.Definitions
 open import Algebra.Structures
-open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Level using (Level; _⊔_)
 
 private

src/Algebra/Morphism/Consequences.agda

@@ -10,7 +10,7 @@ module Algebra.Morphism.Consequences where
 
 open import Algebra using (Magma)
 open import Algebra.Morphism.Definitions
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Function.Base using (id; _∘_)
 open import Function.Definitions
 import Relation.Binary.Reasoning.Setoid as EqR

src/Algebra/Morphism/Construct/Identity.agda

@@ -20,7 +20,7 @@ open import Algebra.Morphism.Structures
         ; module QuasigroupMorphisms
         ; module LoopMorphisms
         )
-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.Morphism.Construct.Identity using (isRelHomomorphism)

src/Algebra/Morphism/MonoidMonomorphism.agda

@@ -24,7 +24,7 @@ open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; 
 
 open import Algebra.Definitions
 open import Algebra.Structures
-open import Data.Product using (map)
+open import Data.Product.Base using (map)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 
 ------------------------------------------------------------------------

src/Algebra/Ordered/Structures.agda

@@ -21,7 +21,7 @@ module Algebra.Ordered.Structures
 open import Algebra.Core
 open import Algebra.Definitions _≈_
 open import Algebra.Structures _≈_
-open import Data.Product using (proj₁; proj₂)
+open import Data.Product.Base using (proj₁; proj₂)
 open import Function.Base using (flip)
 open import Level using (_⊔_)
 open import Relation.Binary.Definitions using (Transitive; Monotonic₁; Monotonic₂)

src/Algebra/Properties/BooleanAlgebra.agda

@@ -30,7 +30,7 @@ open import Algebra.Structures _≈_
 open import Relation.Binary
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence using (_⇔_; module Equivalence)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES

src/Algebra/Properties/CommutativeMagma/Divisibility.agda

@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra using (CommutativeMagma)
-open import Data.Product using (_×_; _,_; map)
+open import Data.Product.Base using (_×_; _,_; map)
 
 module Algebra.Properties.CommutativeMagma.Divisibility
   {a ℓ} (CM : CommutativeMagma a ℓ)

src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda

@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra using (CommutativeSemigroup)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 
 module Algebra.Properties.CommutativeSemigroup.Divisibility

src/Algebra/Properties/Lattice.agda

@@ -11,7 +11,7 @@ open import Algebra.Lattice.Bundles
 open import Relation.Binary
 open import Function.Base
 open import Function.Bundles using (module Equivalence; _⇔_)
-open import Data.Product using (_,_; swap)
+open import Data.Product.Base using (_,_; swap)
 
 module Algebra.Properties.Lattice {l₁ l₂} (L : Lattice l₁ l₂) where
 

src/Algebra/Properties/Monoid/Divisibility.agda

@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra using (Monoid)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Relation.Binary
 
 module Algebra.Properties.Monoid.Divisibility

src/Algebra/Properties/Semigroup/Divisibility.agda

@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra using (Semigroup)
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Relation.Binary.Definitions using (Transitive)
 
 module Algebra.Properties.Semigroup.Divisibility

src/Algebra/Properties/Semiring/Divisibility.agda

@@ -8,7 +8,7 @@
 
 open import Algebra using (Semiring)
 import Algebra.Properties.Monoid.Divisibility as MonoidDivisibility
-open import Data.Product using (_,_)
+open import Data.Product.Base using (_,_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 
 module Algebra.Properties.Semiring.Divisibility

src/Algebra/Solver/CommutativeMonoid.agda

@@ -17,7 +17,7 @@ open import Data.Maybe.Base as Maybe
   using (Maybe; decToMaybe; From-just; from-just)
 open import Data.Nat as ℕ using (ℕ; zero; suc; _+_)
 open import Data.Nat.GeneralisedArithmetic using (fold)
-open import Data.Product using (_×_; uncurry)
+open import Data.Product.Base using (_×_; uncurry)
 open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate)
 
 open import Function.Base using (_∘_)

src/Algebra/Solver/IdempotentCommutativeMonoid.agda

@@ -15,7 +15,7 @@ open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Maybe.Base as Maybe
   using (Maybe; decToMaybe; From-just; from-just)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_)
-open import Data.Product using (_×_; uncurry)
+open import Data.Product.Base using (_×_; uncurry)
 open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate)
 
 open import Function.Base using (_∘_)

src/Algebra/Solver/Ring/NaturalCoefficients.agda

@@ -12,7 +12,7 @@ import Algebra.Properties.Semiring.Mult as SemiringMultiplication
 open import Data.Maybe.Base using (Maybe; just; nothing; map)
 open import Algebra.Solver.Ring.AlmostCommutativeRing
 open import Data.Nat.Base as ℕ
-open import Data.Product using (module Σ)
+open import Data.Product.Base using (module Σ)
 open import Function.Base using (id)
 open import Relation.Binary.PropositionalEquality using (_≡_)