Final Data.Product import simplifications

README/Case.agda

@@ -12,7 +12,6 @@ module README.Case where
 open import Data.Fin   hiding (pred)
 open import Data.Maybe hiding (from-just)
 open import Data.Nat   hiding (pred)
-open import Data.Product
 open import Function.Base using (case_of_; case_return_of_)
 open import Relation.Nullary
 open import Relation.Binary

README/Data/Container/Indexed.agda

@@ -11,7 +11,7 @@ module README.Data.Container.Indexed where
 open import Data.Unit
 open import Data.Empty
 open import Data.Nat.Base
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Function.Base using (_∋_)
 open import Data.W.Indexed
 open import Data.Container.Indexed

README/Data/Integer.agda

@@ -51,7 +51,6 @@ ex₅ i j = ℤₚ.*-comm i j
 -- provides some combinators for equational reasoning.
 
 open P.≡-Reasoning
-open import Data.Product
 
 ex₆ : ∀ i j → i * (j + + 0) ≡ j * i
 ex₆ i j = begin

README/Data/List/Fresh.agda

@@ -12,7 +12,7 @@ open import Data.Nat
 open import Data.List.Base
 open import Data.List.Fresh
 open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
-open import Data.Product
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Relation.Nary using (⌊_⌋; fromWitness)
 
 -- A sorted list of natural numbers can be seen as a fresh list

README/Data/Record.agda

@@ -11,7 +11,7 @@
 
 module README.Data.Record where
 
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Data.String
 open import Function.Base using (flip)
 open import Level

README/Data/Trie/NonDependent.agda

@@ -56,7 +56,7 @@ import Data.Char.Properties  as Char
 open import Data.List.Base   as List using (List; []; _∷_)
 open import Data.List.Fresh  as List# using (List#; []; _∷#_)
 open import Data.Maybe       as Maybe
-open import Data.Product     as Prod
+open import Data.Product.Base as Prod using (_×_; ∃; proj₁; _,_)
 open import Data.String.Base as String using (String)
 open import Data.String.Properties as String using (_≟_)
 open import Data.These       as These

README/Data/Wrap.agda

@@ -13,7 +13,7 @@ open import Data.Wrap
 open import Algebra
 open import Data.Nat
 open import Data.Nat.Properties
-open import Data.Product
+open import Data.Product.Base using (_,_; ∃; ∃₂; _×_)
 open import Level using (Level)
 open import Relation.Binary
 

README/Design/Decidability.agda

@@ -13,7 +13,7 @@ open import Data.List.Base using (List; []; _∷_)
 open import Data.List.Properties using (∷-injective)
 open import Data.Nat
 open import Data.Nat.Properties using (suc-injective)
-open import Data.Product
+open import Data.Product.Base using (uncurry)
 open import Data.Unit
 open import Function.Base using (id;  _∘_)
 open import Relation.Binary.PropositionalEquality

README/Foreign/Haskell.agda

@@ -22,7 +22,7 @@ open import Data.Bool.Base using (Bool; if_then_else_)
 open import Data.Char as Char
 open import Data.List.Base as List using (List; _∷_; []; takeWhile; dropWhile)
 open import Data.Maybe.Base using (Maybe; just; nothing)
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_)
 open import Function
 open import Relation.Nullary.Decidable
 

README/Inspect.agda

@@ -14,7 +14,7 @@ module README.Inspect where
 
 open import Data.Nat.Base
 open import Data.Nat.Properties
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Binary.PropositionalEquality using (inspect)
 

README/Relation/Binary/TypeClasses.agda

@@ -19,7 +19,7 @@ open import Data.List.Instances
 open import Data.List.Relation.Binary.Lex.NonStrict using (Lex-≤)
 open import Data.Nat.Base renaming (_≤_ to _≤ℕ_)
 open import Data.Nat.Instances
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_; Σ)
 open import Data.Product.Instances
 open import Data.Unit.Base renaming (_≤_ to _≤⊤_)
 open import Data.Unit.Instances

README/Text/Pretty.agda

@@ -14,7 +14,7 @@ open import Data.Bool.Base
 open import Data.List.Base as List
 open import Data.List.NonEmpty as List⁺
 open import Data.Nat.Base
-open import Data.Product
+open import Data.Product.Base using (_×_; uncurry; _,_)
 open import Data.String.Base hiding (parens; _<+>_)
 open import Data.Vec.Base as Vec
 open import Function.Base

src/Algebra/Apartness/Structures.agda

@@ -17,7 +17,7 @@ module Algebra.Apartness.Structures
   where
 
 open import Level using (_⊔_; suc)
-open import Data.Product using (∃-syntax; _×_; _,_; proj₂)
+open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₂)
 open import Algebra.Definitions _≈_ using (Invertible)
 open import Algebra.Structures _≈_ using (IsCommutativeRing)
 open import Relation.Binary.Structures using (IsEquivalence; IsApartnessRelation)

src/Algebra/Construct/DirectProduct.agda

@@ -16,7 +16,7 @@
 module Algebra.Construct.DirectProduct where
 
 open import Algebra
-open import Data.Product
+open import Data.Product.Base using (_×_; zip; _,_; map; _<*>_; uncurry)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Level using (Level; _⊔_)
 

src/Algebra/Construct/LexProduct.agda

@@ -8,7 +8,7 @@
 
 open import Algebra
 open import Data.Bool using (true; false)
-open import Data.Product
+open import Data.Product.Base using (_×_; _,_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (Pointwise)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_∘_)

src/Algebra/Lattice/Construct/DirectProduct.agda

@@ -16,7 +16,7 @@
 open import Algebra
 open import Algebra.Lattice
 import Algebra.Construct.DirectProduct as DirectProduct
-open import Data.Product
+open import Data.Product.Base using (_,_; _<*>_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Level using (Level; _⊔_)
 

src/Algebra/Module/Construct/DirectProduct.agda

@@ -14,7 +14,7 @@ module Algebra.Module.Construct.DirectProduct where
 open import Algebra.Bundles
 open import Algebra.Construct.DirectProduct
 open import Algebra.Module.Bundles
-open import Data.Product
+open import Data.Product.Base using (map; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Level
 

src/Algebra/Module/Definitions/Left.agda

@@ -15,8 +15,6 @@ module Algebra.Module.Definitions.Left
   {a b ℓb} (A : Set a) {B : Set b} (_≈_ : Rel B ℓb)
   where
 
-open import Data.Product
-
 ------------------------------------------------------------------------
 -- Binary operations
 

src/Algebra/Module/Definitions/Right.agda

@@ -15,8 +15,6 @@ module Algebra.Module.Definitions.Right
   {a b ℓb} (A : Set a) {B : Set b} (_≈_ : Rel B ℓb)
   where
 
-open import Data.Product
-
 ------------------------------------------------------------------------
 -- Binary operations
 

src/Algebra/Module/Morphism/ModuleHomomorphism.agda

@@ -25,7 +25,7 @@ module Algebra.Module.Morphism.ModuleHomomorphism
   where
 
 open import Axiom.DoubleNegationElimination
-open import Data.Product
+open import Data.Product.Base using (∃₂; _×_; _,_)
 open import Relation.Binary.Reasoning.MultiSetoid
 open import Relation.Nullary          using (¬_)
 open import Relation.Nullary.Negation using (contraposition)

src/Algebra/Morphism/Construct/Composition.agda

@@ -10,7 +10,6 @@ module Algebra.Morphism.Construct.Composition where
 
 open import Algebra.Bundles
 open import Algebra.Morphism.Structures
-open import Data.Product
 open import Function.Base using (_∘_)
 import Function.Construct.Composition as Func
 open import Level using (Level)

src/Algebra/Morphism/GroupMonomorphism.agda

@@ -26,7 +26,7 @@ open RawGroup G₂ renaming
 
 open import Algebra.Definitions
 open import Algebra.Structures
-open import Data.Product
+open import Data.Product.Base using (_,_)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 
 ------------------------------------------------------------------------

src/Algebra/Morphism/MagmaMonomorphism.agda

@@ -25,7 +25,7 @@ open RawMagma M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_)
 
 open import Algebra.Structures
 open import Algebra.Definitions
-open import Data.Product
+open import Data.Product.Base using (map)
 open import Data.Sum.Base using (inj₁; inj₂)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 import Relation.Binary.Morphism.RelMonomorphism isRelMonomorphism as RelMorphism

src/Algebra/Morphism/RingMonomorphism.agda

@@ -28,7 +28,7 @@ open RawRing R₂ renaming
 
 open import Algebra.Definitions
 open import Algebra.Structures
-open import Data.Product
+open import Data.Product.Base using (proj₁; proj₂; _,_)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 
 ------------------------------------------------------------------------

src/Algebra/Properties/Loop.agda

@@ -13,7 +13,6 @@ module Algebra.Properties.Loop {l₁ l₂} (L : Loop l₁ l₂) where
 open Loop L
 open import Algebra.Definitions _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
-open import Data.Product
 open import Algebra.Properties.Quasigroup
 
 x//x≈ε : ∀ x → x // x ≈ ε

src/Algebra/Properties/Magma/Divisibility.agda

@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra using (Magma)
-open import Data.Product using (_×_; _,_; ∃; map; swap)
+open import Data.Product.Base using (_×_; _,_; ∃; map; swap)
 open import Relation.Binary.Definitions
 
 module Algebra.Properties.Magma.Divisibility {a ℓ} (M : Magma a ℓ) where

src/Algebra/Properties/MiddleBolLoop.agda

@@ -13,7 +13,6 @@ module Algebra.Properties.MiddleBolLoop {m₁ m₂} (M : MiddleBolLoop m₁ m₂
 open MiddleBolLoop M
 open import Algebra.Definitions _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
-open import Data.Product
 import Algebra.Properties.Loop as LoopProperties
 open LoopProperties loop public
 

src/Algebra/Properties/MoufangLoop.agda

@@ -13,7 +13,7 @@ module Algebra.Properties.MoufangLoop {a ℓ} (M : MoufangLoop a ℓ) where
 open MoufangLoop M
 open import Algebra.Definitions _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
-open import Data.Product
+open import Data.Product.Base using (_,_)
 
 alternativeˡ : LeftAlternative _∙_
 alternativeˡ x y = begin

src/Algebra/Properties/Quasigroup.agda

@@ -13,7 +13,7 @@ module Algebra.Properties.Quasigroup {q₁ q₂} (Q : Quasigroup q₁ q₂) wher
 open Quasigroup Q
 open import Algebra.Definitions _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
-open import Data.Product
+open import Data.Product.Base using (_,_)
 
 cancelˡ : LeftCancellative _∙_
 cancelˡ x y z eq = begin

src/Algebra/Solver/Monoid.agda

@@ -17,7 +17,7 @@ import Data.List.Relation.Binary.Equality.DecPropositional as ListEq
 open import Data.Maybe.Base as Maybe
   using (Maybe; decToMaybe; From-just; from-just)
 open import Data.Nat.Base using (ℕ)
-open import Data.Product
+open import Data.Product.Base using (_×_; uncurry)
 open import Data.Vec.Base using (Vec; lookup)
 open import Function.Base using (_∘_; _$_)
 open import Relation.Binary.Definitions using (Decidable)

src/Codata/Musical/Colist.agda

@@ -21,7 +21,7 @@ open import Data.Maybe.Relation.Unary.Any using (just)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.NonEmpty using (List⁺; _∷_)
-open import Data.Product as Prod using (∃; _×_; _,_)
+open import Data.Product.Base as Prod using (∃; _×_; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Vec.Bounded as Vec≤ using (Vec≤)
 open import Function.Base

src/Codata/Musical/Colist/Infinite-merge.agda

@@ -13,7 +13,7 @@ open import Codata.Musical.Colist as Colist hiding (_⋎_)
 open import Data.Nat.Base
 open import Data.Nat.Induction using (<′-wellFounded)
 open import Data.Nat.Properties
-open import Data.Product as Prod
+open import Data.Product.Base as Prod using (_×_; _,_; ∃; ∃₂; proj₁; proj₂)
 open import Data.Sum.Base
 open import Data.Sum.Properties
 open import Data.Sum.Function.Propositional using (_⊎-cong_)

src/Codata/Musical/Conversion.agda

@@ -27,7 +27,7 @@ open import Codata.Musical.Covec hiding (module Covec)
 open import Codata.Musical.M hiding (module M)
 open import Codata.Musical.Notation
 open import Codata.Musical.Stream hiding (module Stream)
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Data.Container.Core as C using (Container)
 import Size
 

src/Codata/Musical/M/Indexed.agda

@@ -11,7 +11,7 @@ module Codata.Musical.M.Indexed where
 
 open import Level
 open import Codata.Musical.Notation
-open import Data.Product
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Data.Container.Indexed.Core
 open import Function.Base using (_∘_)
 open import Relation.Unary

src/Data/Container/Combinator.agda

@@ -10,7 +10,7 @@ module Data.Container.Combinator where
 
 open import Level using (Level; _⊔_; lower)
 open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
-open import Data.Product as P using (_,_; <_,_>; proj₁; proj₂; ∃)
+open import Data.Product.Base as P using (_,_; <_,_>; proj₁; proj₂; ∃)
 open import Data.Sum.Base as S using ([_,_]′)
 open import Data.Unit.Polymorphic.Base using (⊤)
 import Function.Base as F

src/Data/Container/Combinator/Properties.agda

@@ -13,7 +13,7 @@ open import Data.Container.Core
 open import Data.Container.Combinator
 open import Data.Container.Relation.Unary.Any
 open import Data.Empty using (⊥-elim)
-open import Data.Product as Prod using (∃; _,_; proj₁; proj₂; <_,_>; uncurry; curry)
+open import Data.Product.Base as Prod using (∃; _,_; proj₁; proj₂; <_,_>; uncurry; curry)
 open import Data.Sum.Base as S using (inj₁; inj₂; [_,_]′; [_,_])
 open import Function.Base as F using (_∘′_)
 open import Function.Inverse as Inv using (_↔_; inverse; module Inverse)

src/Data/Container/Indexed/Combinator.agda

@@ -12,7 +12,7 @@ open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Data.Container.Indexed
 open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
 open import Data.Unit.Polymorphic.Base using (⊤)
-open import Data.Product as Prod hiding (Σ) renaming (_×_ to _⟨×⟩_)
+open import Data.Product.Base as Prod hiding (Σ) renaming (_×_ to _⟨×⟩_)
 open import Data.Sum.Base renaming (_⊎_ to _⟨⊎⟩_)
 open import Data.Sum.Relation.Unary.All as All using (All)
 open import Function.Base as F hiding (id; const) renaming (_∘_ to _⟨∘⟩_)

src/Data/Container/Indexed/Core.agda

@@ -9,7 +9,7 @@
 module Data.Container.Indexed.Core where
 
 open import Level
-open import Data.Product
+open import Data.Product.Base using (Σ; Σ-syntax; _,_; ∃)
 open import Relation.Unary
 
 infix 5 _◃_/_

src/Data/Container/Indexed/FreeMonad.agda

@@ -15,7 +15,7 @@ open import Data.Container.Indexed
 open import Data.Container.Indexed.Combinator hiding (id; _∘_)
 open import Data.Empty
 open import Data.Sum.Base using (inj₁; inj₂)
-open import Data.Product
+open import Data.Product.Base using (_,_)
 open import Data.W.Indexed
 open import Relation.Unary
 open import Relation.Unary.PredicateTransformer

src/Data/Container/Indexed/WithK.agda

@@ -15,7 +15,8 @@ module Data.Container.Indexed.WithK where
 
 open import Axiom.Extensionality.Heterogeneous using (Extensionality)
 open import Data.Container.Indexed hiding (module PlainMorphism)
-open import Data.Product as Prod hiding (map)
+open import Data.Product.Base
+  using (_,_; -,_; _×_; ∃; proj₁; proj₂; Σ-syntax)
 open import Function.Base renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
 open import Level
 open import Relation.Unary using (Pred; _⊆_)

src/Data/Container/Morphism/Properties.agda

@@ -10,7 +10,7 @@ module Data.Container.Morphism.Properties where
 
 open import Level using (_⊔_; suc)
 open import Function.Base as F using (_$_)
-open import Data.Product using (∃; proj₁; proj₂; _,_)
+open import Data.Product.Base using (∃; proj₁; proj₂; _,_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)
 

src/Data/Container/Relation/Unary/All.agda

@@ -10,7 +10,7 @@ module Data.Container.Relation.Unary.All where
 
 open import Level using (_⊔_)
 open import Relation.Unary using (Pred; _⊆_)
-open import Data.Product as Prod using (_,_; proj₁; proj₂; ∃)
+open import Data.Product.Base using (_,_; proj₁; proj₂; ∃)
 open import Function.Base using (_∘′_; id)
 
 open import Data.Container.Core hiding (map)

src/Data/Container/Relation/Unary/Any.agda

@@ -10,7 +10,7 @@ module Data.Container.Relation.Unary.Any where
 
 open import Level using (_⊔_)
 open import Relation.Unary using (Pred; _⊆_)
-open import Data.Product as Prod using (_,_; proj₂; ∃)
+open import Data.Product.Base using (_,_; proj₂; ∃)
 open import Function.Base using (_∘′_; id)
 
 open import Data.Container.Core hiding (map)

src/Data/Container/Relation/Unary/Any/Properties.agda

@@ -10,7 +10,7 @@ module Data.Container.Relation.Unary.Any.Properties where
 
 open import Level
 open import Algebra
-open import Data.Product as Prod using (∃; _×_; ∃₂; _,_; proj₂)
+open import Data.Product.Base using (∃; _×_; ∃₂; _,_; proj₂)
 open import Data.Product.Function.NonDependent.Propositional using (_×-cong_)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])