[ re #1993 ] Simplifying the dependency graph

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

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}

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

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

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

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 (¬_)

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

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

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
 

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)
 

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

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

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

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)

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 (_⊔_)
 
 ------------------------------------------------------------------------

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)
 

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≤; _,_)

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

src/Data/Bool/Properties.agda

@@ -13,18 +13,18 @@ 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)
 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} _≡_

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

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ℓ)

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."
 #-}
-

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)

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)

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

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

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 (¬_)
 

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; []; _∷_)

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)

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; _⊔_)

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