[ re #1993 ] Simplifying the dependency graph (#1995)

Author: gallais

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)