Simplify some Relation.Binary imports

README/Data/Trie/NonDependent.agda

@@ -62,7 +62,7 @@ open import Data.These       as These
 
 open import Function.Base using (case_of_; _$_; _∘′_; id; _on_)
 open import Relation.Nary
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary.Decidable using (¬?)
 
 open import Data.Trie Char.<-strictTotalOrder

README/Design/Hierarchies.agda

@@ -10,7 +10,7 @@ module README.Design.Hierarchies where
 
 open import Data.Sum using (_⊎_)
 open import Level using (Level; _⊔_; suc)
-open import Relation.Binary using (_Preserves₂_⟶_⟶_)
+open import Relation.Binary.Core using (_Preserves₂_⟶_⟶_)
 
 private
   variable

src/Algebra/Consequences/Propositional.agda

@@ -11,7 +11,9 @@ module Algebra.Consequences.Propositional
   {a} {A : Set a} where
 
 open import Data.Sum.Base using (inj₁; inj₂)
-open import Relation.Binary using (Rel; Setoid; Symmetric; Total)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions using (Symmetric; Total)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary using (Pred)
 

src/Algebra/Consequences/Setoid.agda

@@ -7,7 +7,10 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; Setoid; Substitutive; Symmetric; Total)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions
+  using (Substitutive; Symmetric; Total)
 
 module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where
 

src/Algebra/Construct/Initial.agda

@@ -22,7 +22,10 @@ open import Algebra.Core using (Op₂)
 open import Algebra.Definitions using (Congruent₂)
 open import Algebra.Structures using (IsMagma; IsSemigroup; IsBand)
 open import Data.Empty.Polymorphic
-open import Relation.Binary using (Rel; Reflexive; Symmetric; Transitive; IsEquivalence)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Binary.Definitions
+  using (Reflexive; Symmetric; Transitive)
 
 
 ------------------------------------------------------------------------

src/Algebra/FunctionProperties/Consequences.agda

@@ -6,7 +6,10 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; Setoid; Substitutive; Symmetric; Total)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions
+  using (Substitutive; Symmetric; Total)
 
 module Algebra.FunctionProperties.Consequences
   {a ℓ} (S : Setoid a ℓ) where

src/Algebra/Lattice/Bundles/Raw.agda

@@ -11,7 +11,7 @@ module Algebra.Lattice.Bundles.Raw where
 open import Algebra.Core
 open import Algebra.Bundles.Raw using (RawMagma)
 open import Level using (suc; _⊔_)
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 
 record RawLattice c ℓ : Set (suc (c ⊔ ℓ)) where
   infixr 7 _∧_

src/Algebra/Lattice/Structures.agda

@@ -16,7 +16,9 @@
 open import Algebra.Core
 open import Data.Product.Base using (proj₁; proj₂)
 open import Level using (_⊔_)
-open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
 
 module Algebra.Lattice.Structures
   {a ℓ} {A : Set a}  -- The underlying set

src/Algebra/Lattice/Structures/Biased.agda

@@ -16,7 +16,9 @@ open import Algebra.Core
 open import Algebra.Consequences.Setoid
 open import Data.Product.Base using (proj₁; proj₂)
 open import Level using (_⊔_)
-open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
 
 module Algebra.Lattice.Structures.Biased
   {a ℓ} {A : Set a}  -- The underlying set

src/Algebra/Module/Consequences.agda

@@ -14,7 +14,8 @@ open import Algebra.Module.Core using (Opₗ; Opᵣ)
 open import Algebra.Module.Definitions
 open import Function.Base using (flip)
 open import Level using (Level)
-open import Relation.Binary using (Rel; Setoid)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.Reasoning.Setoid as Rea
 
 private

src/Algebra/Module/Structures.agda

@@ -6,7 +6,9 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
 
 module Algebra.Module.Structures where
 

src/Algebra/Module/Structures/Biased.agda

@@ -7,7 +7,9 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
 
 module Algebra.Module.Structures.Biased where
 

src/Algebra/Ordered/Bundles.agda

@@ -16,7 +16,7 @@ open import Algebra.Core
 open import Algebra.Bundles
 open import Algebra.Ordered.Structures
 open import Level using (suc; _⊔_)
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Preorder; Poset)
 
 ------------------------------------------------------------------------

src/Algebra/Properties/CancellativeCommutativeSemiring.agda

@@ -9,7 +9,7 @@
 open import Algebra using (CancellativeCommutativeSemiring)
 open import Algebra.Definitions using (AlmostRightCancellative)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Negation using (contradiction)
 

src/Algebra/Properties/Semiring/Primality.agda

@@ -9,7 +9,7 @@
 open import Algebra using (Semiring)
 open import Data.Sum.Base using (reduce)
 open import Function.Base using (flip)
-open import Relation.Binary using (Symmetric)
+open import Relation.Binary.Definitions using (Symmetric)
 
 module Algebra.Properties.Semiring.Primality
   {a ℓ} (R : Semiring a ℓ)

src/Algebra/Solver/Monoid.agda

@@ -20,7 +20,7 @@ open import Data.Nat.Base using (ℕ)
 open import Data.Product
 open import Data.Vec.Base using (Vec; lookup)
 open import Function.Base using (_∘_; _$_)
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 import Relation.Binary.Reflection

src/Algebra/Structures.agda

@@ -9,7 +9,9 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
 
 module Algebra.Structures
   {a ℓ} {A : Set a}  -- The underlying set

src/Algebra/Structures/Biased.agda

@@ -11,7 +11,9 @@ open import Algebra.Core
 open import Algebra.Consequences.Setoid
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Level using (_⊔_)
-open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
 
 module Algebra.Structures.Biased
   {a ℓ} {A : Set a}  -- The underlying set

src/Data/String.agda

@@ -22,7 +22,7 @@ open import Data.Vec.Base as Vec using (Vec)
 open import Data.Char.Base as Char using (Char)
 import Data.Char.Properties as Char using (_≟_)
 open import Function
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 open import Relation.Nullary.Decidable using (does)
 open import Relation.Unary using (Pred; Decidable)

src/Effect/Monad/Partiality.agda

@@ -19,7 +19,13 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (Level; _⊔_)
-open import Relation.Binary as B hiding (Rel; _⇔_)
+open import Relation.Binary.Core as B hiding (Rel; _⇔_)
+open import Relation.Binary.Definitions
+  using (Decidable; Reflexive; Symmetric; Transitive)
+open import Relation.Binary.Structures
+  using (IsPreorder; IsEquivalence)
+open import Relation.Binary.Bundles
+  using (Preorder; Setoid; Poset)
 import Relation.Binary.Properties.Setoid as SetoidProperties
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Nullary

src/Function/Construct/Symmetry.agda

@@ -11,7 +11,9 @@ module Function.Construct.Symmetry where
 open import Data.Product.Base using (_,_; swap; proj₁; proj₂)
 open import Function
 open import Level using (Level)
-open import Relation.Binary hiding (_⇔_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Symmetric; Transitive)
+open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.PropositionalEquality
 
 private

src/Function/Indexed/Bundles.agda

@@ -10,7 +10,7 @@ module Function.Indexed.Bundles where
 
 open import Relation.Unary using (Pred)
 open import Function.Bundles using (_⟶_; _↣_; _↠_; _⤖_; _⇔_; _↩_; _↪_; _↩↪_; _↔_)
-open import Relation.Binary hiding (_⇔_)
+open import Relation.Binary.Core hiding (_⇔_)
 open import Level using (Level)
 
 private

src/Relation/Binary/Construct/Closure/Transitive.agda

@@ -12,7 +12,9 @@ open import Function.Base
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Induction.WellFounded
 open import Level
-open import Relation.Binary hiding (_⇔_)
+open import Relation.Binary.Core using (Rel; _=[_]⇒_; _⇒_)
+open import Relation.Binary.Definitions
+  using (Reflexive; Symmetric; Transitive)
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
 private

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

@@ -13,7 +13,7 @@ module Relation.Binary.Indexed.Heterogeneous.Bundles where
 
 open import Function.Base
 open import Level using (suc; _⊔_)
-open import Relation.Binary using (_⇒_)
+open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Binary.Indexed.Heterogeneous.Core
 open import Relation.Binary.Indexed.Heterogeneous.Structures

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

@@ -17,7 +17,7 @@ module Relation.Binary.Indexed.Heterogeneous.Structures
 
 open import Function.Base
 open import Level using (suc; _⊔_)
-open import Relation.Binary using (_⇒_)
+open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Binary.Indexed.Heterogeneous.Definitions
 

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

@@ -14,7 +14,8 @@ module Relation.Binary.Indexed.Homogeneous.Bundles where
 open import Data.Product using (_,_)
 open import Function.Base using (_⟨_⟩_)
 open import Level using (Level; _⊔_; suc)
-open import Relation.Binary as B using (_⇒_)
+open import Relation.Binary.Core using (_⇒_; Rel)
+open import Relation.Binary.Bundles as B
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Binary.Indexed.Homogeneous.Core
@@ -41,10 +42,10 @@ record IndexedSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
 
   infix 4 _≉_
 
-  _≈_ : B.Rel Carrier _
+  _≈_ : Rel Carrier _
   _≈_ = Lift Carrierᵢ _≈ᵢ_
 
-  _≉_ : B.Rel Carrier _
+  _≉_ : Rel Carrier _
   x ≉ y = ¬ (x ≈ y)
 
   setoid : B.Setoid _ _
@@ -89,10 +90,10 @@ record IndexedPreorder {i} (I : Set i) c ℓ₁ ℓ₂ :
   Carrier : Set _
   Carrier = ∀ i → Carrierᵢ i
 
-  _≈_ : B.Rel Carrier _
+  _≈_ : Rel Carrier _
   x ≈ y = ∀ i → x i ≈ᵢ y i
 
-  _∼_ : B.Rel Carrier _
+  _∼_ : Rel Carrier _
   x ∼ y = ∀ i → x i ∼ᵢ y i
 
   preorder : B.Preorder _ _ _

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

@@ -13,7 +13,7 @@ module Relation.Binary.Indexed.Homogeneous.Core where
 
 open import Level using (Level; _⊔_)
 open import Data.Product using (_×_)
-open import Relation.Binary as B using (REL; Rel)
+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
 open import Relation.Unary.Indexed using (IPred)

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

@@ -20,7 +20,9 @@ module Relation.Binary.Indexed.Homogeneous.Structures
 open import Data.Product using (_,_)
 open import Function.Base using (_⟨_⟩_)
 open import Level using (Level; _⊔_; suc)
-open import Relation.Binary as B using (_⇒_)
+open import Relation.Binary.Core using (_⇒_)
+import Relation.Binary.Definitions as B
+import Relation.Binary.Structures as B
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Binary.Indexed.Homogeneous.Definitions
 
@@ -97,7 +99,7 @@ record IsIndexedPreorder {ℓ₂} (_∼ᵢ_ : IRel A ℓ₂)
 
   -- Lifted properties
 
-  reflexive : Lift A _≈ᵢ_ B.⇒ Lift A _∼ᵢ_
+  reflexive : Lift A _≈ᵢ_ ⇒ Lift A _∼ᵢ_
   reflexive x≈y i = reflexiveᵢ (x≈y i)
 
   refl : B.Reflexive (Lift A _∼ᵢ_)

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

@@ -15,7 +15,7 @@ open BoundedLattice L
 
 open import Algebra.Definitions _≈_
 open import Data.Product using (_,_)
-open import Relation.Binary using (Setoid)
+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/Nullary/Universe.agda

@@ -10,7 +10,8 @@ module Relation.Nullary.Universe where
 
 open import Relation.Nullary
 open import Relation.Nullary.Negation
-open import Relation.Binary hiding (_⇒_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.Construct.Always as Always
 open import Relation.Binary.PropositionalEquality as PropEq
   using (_≡_; refl)

src/Relation/Unary/PredicateTransformer.agda

@@ -13,7 +13,7 @@ open import Function
 open import Level hiding (_⊔_)
 open import Relation.Nullary
 open import Relation.Unary
-open import Relation.Binary using (REL)
+open import Relation.Binary.Core using (REL)
 
 private
   variable

src/Text/Regex.agda

@@ -10,7 +10,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (DecPoset)
+open import Relation.Binary.Bundles using (DecPoset)
 
 module Text.Regex {a e r} (decPoset : DecPoset a e r) where
 

src/Text/Regex/Base.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Preorder)
+open import Relation.Binary.Bundles using (Preorder)
 
 module Text.Regex.Base {a e r} (P : Preorder a e r) where
 

src/Text/Regex/Derivative/Brzozowski.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (DecPoset)
+open import Relation.Binary.Bundles using (DecPoset)
 
 module Text.Regex.Derivative.Brzozowski {a e r} (P? : DecPoset a e r) where
 
@@ -18,7 +18,7 @@ open import Function.Base using (_$_; _∘′_; case_of_)
 open import Relation.Nullary.Decidable using (Dec; yes; no)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Nullary.Decidable using (map′; ¬?)
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
 
 open DecPoset P? using (preorder) renaming (Carrier to A)