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 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 Bundles
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Binary.Indexed.Homogeneous.Core
@@ -39,13 +40,13 @@ record IndexedSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
   Carrier : Set _
   Carrier = ∀ i → Carrierᵢ i
 
-  _≈_ : B.Rel Carrier _
+  _≈_ : Rel Carrier _
   _≈_ = Lift Carrierᵢ _≈ᵢ_
 
-  _≉_ : B.Rel Carrier _
+  _≉_ : Rel Carrier _
   x ≉ y = ¬ (x ≈ y)
 
-  setoid : B.Setoid _ _
+  setoid : Bundles.Setoid _ _
   setoid = record
     { isEquivalence = isEquivalence
     }
@@ -87,13 +88,13 @@ 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 _ _ _
+  preorder : Bundles.Preorder _ _ _
   preorder = record
     { isPreorder = isPreorder
     }
@@ -119,7 +120,7 @@ record IndexedPoset {i} (I : Set i) c ℓ₁ ℓ₂ :
   open IndexedPreorder preorderᵢ public
     using (Carrier; _≈_; preorder) renaming (_∼_ to _≤_)
 
-  poset : B.Poset _ _ _
+  poset : Bundles.Poset _ _ _
   poset = record
     { isPartialOrder = isPartialOrder
     }

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,10 @@ 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 Definitions
+import Relation.Binary.Bundles as Bundles
+import Relation.Binary.Structures as Structures
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Binary.Indexed.Homogeneous.Definitions
 
@@ -45,16 +48,16 @@ record IsIndexedEquivalence : Set (i ⊔ a ⊔ ℓ) where
   reflexive : _≡_ ⇒ (Lift A _≈ᵢ_)
   reflexive P.refl i = reflᵢ
 
-  refl : B.Reflexive (Lift A _≈ᵢ_)
+  refl : Definitions.Reflexive (Lift A _≈ᵢ_)
   refl i = reflᵢ
 
-  sym : B.Symmetric (Lift A _≈ᵢ_)
+  sym : Definitions.Symmetric (Lift A _≈ᵢ_)
   sym x≈y i = symᵢ (x≈y i)
 
-  trans : B.Transitive (Lift A _≈ᵢ_)
+  trans : Definitions.Transitive (Lift A _≈ᵢ_)
   trans x≈y y≈z i = transᵢ (x≈y i) (y≈z i)
 
-  isEquivalence : B.IsEquivalence (Lift A _≈ᵢ_)
+  isEquivalence : Structures.IsEquivalence (Lift A _≈ᵢ_)
   isEquivalence = record
     { refl  = refl
     ; sym   = sym
@@ -97,25 +100,25 @@ 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 _∼ᵢ_)
+  refl : Definitions.Reflexive (Lift A _∼ᵢ_)
   refl i = reflᵢ
 
-  trans : B.Transitive (Lift A _∼ᵢ_)
+  trans : Definitions.Transitive (Lift A _∼ᵢ_)
   trans x≈y y≈z i = transᵢ (x≈y i) (y≈z i)
 
-  ∼-respˡ-≈ : (Lift A _∼ᵢ_) B.Respectsˡ (Lift A _≈ᵢ_)
+  ∼-respˡ-≈ : (Lift A _∼ᵢ_) Definitions.Respectsˡ (Lift A _≈ᵢ_)
   ∼-respˡ-≈ x≈y x∼z i = ∼ᵢ-respˡ-≈ᵢ (x≈y i) (x∼z i)
 
-  ∼-respʳ-≈ : (Lift A _∼ᵢ_) B.Respectsʳ (Lift A _≈ᵢ_)
+  ∼-respʳ-≈ : (Lift A _∼ᵢ_) Definitions.Respectsʳ (Lift A _≈ᵢ_)
   ∼-respʳ-≈ x≈y z∼x i = ∼ᵢ-respʳ-≈ᵢ (x≈y i) (z∼x i)
 
-  ∼-resp-≈ : (Lift A _∼ᵢ_) B.Respects₂ (Lift A _≈ᵢ_)
+  ∼-resp-≈ : (Lift A _∼ᵢ_) Definitions.Respects₂ (Lift A _≈ᵢ_)
   ∼-resp-≈ = ∼-respʳ-≈ , ∼-respˡ-≈
 
-  isPreorder : B.IsPreorder (Lift A _≈ᵢ_) (Lift A _∼ᵢ_)
+  isPreorder : Structures.IsPreorder (Lift A _≈ᵢ_) (Lift A _∼ᵢ_)
   isPreorder = record
     { isEquivalence = Eq.isEquivalence
     ; reflexive     = reflexive
@@ -142,10 +145,10 @@ record IsIndexedPartialOrder {ℓ₂} (_≤ᵢ_ : IRel A ℓ₂)
     ; ∼-resp-≈    to ≤-resp-≈
     )
 
-  antisym : B.Antisymmetric (Lift A _≈ᵢ_) (Lift A _≤ᵢ_)
+  antisym : Definitions.Antisymmetric (Lift A _≈ᵢ_) (Lift A _≤ᵢ_)
   antisym x≤y y≤x i = antisymᵢ (x≤y i) (y≤x i)
 
-  isPartialOrder : B.IsPartialOrder (Lift A _≈ᵢ_) (Lift A _≤ᵢ_)
+  isPartialOrder : Structures.IsPartialOrder (Lift A _≈ᵢ_) (Lift A _≤ᵢ_)
   isPartialOrder = record
     { isPreorder = isPreorder
     ; antisym    = antisym