Simplify more Relation.Binary imports (#2034)

Saransh-cpp · MatthewDaggitt · commit ed293b51d42d · 2023-10-13T11:34:27.000+09:00
diff --git a/src/Algebra/Properties/Monoid/Sum.agda b/src/Algebra/Properties/Monoid/Sum.agda
@@ -12,7 +12,7 @@ open import Data.Vec.Functional as Vector
 open import Data.Fin.Base using (zero; suc)
 open import Data.Unit using (tt)
 open import Function.Base using (_∘_)
-open import Relation.Binary as B using (_Preserves_⟶_)
+open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.PropositionalEquality as P using (_≗_; _≡_)
 
 module Algebra.Properties.Monoid.Sum {a ℓ} (M : Monoid a ℓ) where
diff --git a/src/Data/AVL/Map.agda b/src/Data/AVL/Map.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.AVL.Map
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
diff --git a/src/Data/AVL/NonEmpty.agda b/src/Data/AVL/NonEmpty.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.AVL.NonEmpty
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) where
diff --git a/src/Data/AVL/Sets.agda b/src/Data/AVL/Sets.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.AVL.Sets
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
diff --git a/src/Data/AVL/Value.agda b/src/Data/AVL/Value.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Setoid)
+open import Relation.Binary.Bundles using (Setoid)
 
 module Data.AVL.Value {a ℓ} (S : Setoid a ℓ) where
 
diff --git a/src/Data/Container/Morphism/Properties.agda b/src/Data/Container/Morphism/Properties.agda
@@ -11,7 +11,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 Relation.Binary using (Setoid)
+open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)
 
 open import Data.Container.Core
diff --git a/src/Data/Container/Relation/Binary/Equality/Setoid.agda b/src/Data/Container/Relation/Binary/Equality/Setoid.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Setoid)
+open import Relation.Binary.Bundles using (Setoid)
 
 module Data.Container.Relation.Binary.Equality.Setoid {c e} (S : Setoid c e) where
 
diff --git a/src/Data/Container/Relation/Binary/Pointwise.agda b/src/Data/Container/Relation/Binary/Pointwise.agda
@@ -11,7 +11,7 @@ module Data.Container.Relation.Binary.Pointwise where
 open import Data.Product using (_,_; Σ-syntax; -,_; proj₁; proj₂)
 open import Function.Base using (_∘_)
 open import Level using (_⊔_)
-open import Relation.Binary using (REL; _⇒_)
+open import Relation.Binary.Core using (REL; _⇒_)
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; subst; cong)
 
diff --git a/src/Data/Container/Relation/Unary/Any/Properties.agda b/src/Data/Container/Relation/Unary/Any/Properties.agda
@@ -22,7 +22,7 @@ open import Function.Inverse as Inv using (_↔_; inverse; module Inverse)
 open import Function.Related as Related using (Related; SK-sym)
 open import Function.Related.TypeIsomorphisms
 open import Relation.Unary using (Pred ; _∪_ ; _∩_)
-open import Relation.Binary using (REL)
+open import Relation.Binary.Core using (REL)
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≗_; refl)
 
diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
@@ -25,7 +25,7 @@ open import Function.Equality using (_⟨$⟩_)
 open import Function.Properties.Inverse using (↔⇒↣)
 open import Function.Base using (_∘_)
 open import Level using (0ℓ)
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary using (does; ¬_; yes; no)
 open import Relation.Nullary.Decidable using (dec-yes; dec-no)
 open import Relation.Nullary.Negation using (contradiction)
diff --git a/src/Data/Integer/Coprimality.agda b/src/Data/Integer/Coprimality.agda
@@ -15,7 +15,8 @@ import Data.Nat.Coprimality as ℕ
 import Data.Nat.Divisibility as ℕ
 open import Function.Base using (_on_)
 open import Level using (0ℓ)
-open import Relation.Binary using (Rel; Decidable; Symmetric)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Decidable; Symmetric)
 open import Relation.Binary.PropositionalEquality.Core using (subst)
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Extrema/Core.agda b/src/Data/List/Extrema/Core.agda
@@ -6,7 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Trans; TotalOrder; Setoid)
+open import Relation.Binary.Definitions using (Trans)
+open import Relation.Binary.Bundles using (TotalOrder; Setoid)
 
 module Data.List.Extrema.Core
   {b ℓ₁ ℓ₂} (totalOrder : TotalOrder b ℓ₁ ℓ₂) where
diff --git a/src/Data/List/Fresh/Membership/Setoid/Properties.agda b/src/Data/List/Fresh/Membership/Setoid/Properties.agda
@@ -6,7 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; Setoid)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
 
 module Data.List.Fresh.Membership.Setoid.Properties {c ℓ} (S : Setoid c ℓ) where
 
diff --git a/src/Data/List/Fresh/Relation/Unary/All.agda b/src/Data/List/Fresh/Relation/Unary/All.agda
@@ -13,7 +13,7 @@ open import Data.Product.Base using (_×_; _,_; proj₁; uncurry)
 open import Data.Sum.Base as Sum using (inj₁; inj₂)
 open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_)
 open import Relation.Unary  as U
-open import Relation.Binary as B using (Rel)
+open import Relation.Binary.Core using (Rel)
 
 open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
 open import Data.List.Fresh.Relation.Unary.Any as Any using (Any; here; there)
diff --git a/src/Data/List/Fresh/Relation/Unary/All/Properties.agda b/src/Data/List/Fresh/Relation/Unary/All/Properties.agda
@@ -15,7 +15,7 @@ open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘′_)
 open import Relation.Nullary
 open import Relation.Unary  as U
-open import Relation.Binary as B using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
 open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
diff --git a/src/Data/List/Fresh/Relation/Unary/Any.agda b/src/Data/List/Fresh/Relation/Unary/Any.agda
@@ -16,7 +16,7 @@ open import Function.Bundles using (_⇔_; mk⇔)
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_)
 open import Relation.Unary  as U
-open import Relation.Binary as B using (Rel)
+open import Relation.Binary.Core using (Rel)
 
 open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
 
diff --git a/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda b/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda
@@ -18,7 +18,7 @@ open import Function.Base using (_∘′_)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary
 open import Relation.Unary  as U using (Pred)
-open import Relation.Binary as B using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Nary
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
@@ -34,7 +34,8 @@ open import Function.Inverse as Inv using (_↔_; module Inverse)
 import Function.Related as Related
 open import Function.Related.TypeIsomorphisms
 open import Level using (Level)
-open import Relation.Binary as B hiding (Decidable)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions as B hiding (Decidable)
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; refl; sym; trans; cong; subst; →-to-⟶; _≗_)
 import Relation.Binary.Properties.DecTotalOrder as DTOProperties
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -6,7 +6,10 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary as B hiding (Decidable)
+open import Relation.Binary.Core
+  using (Rel; _⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions as B hiding (Decidable)
 
 module Data.List.Relation.Binary.Permutation.Setoid.Properties
   {a ℓ} (S : Setoid a ℓ)
diff --git a/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda b/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda
@@ -13,7 +13,7 @@ open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Binary.Pointwise
   using (Pointwise; []; _∷_)
 open import Data.Product using (∃; _×_; _,_; uncurry)
-open import Relation.Binary using (REL; _⇒_)
+open import Relation.Binary.Core using (REL; _⇒_)
 
 module _ {a b r} {A : Set a} {B : Set b} (R : REL A B r) where
 
diff --git a/src/Data/List/Relation/Binary/Sublist/DecPropositional/Solver.agda b/src/Data/List/Relation/Binary/Sublist/DecPropositional/Solver.agda
@@ -7,7 +7,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 module Data.List.Relation.Binary.Sublist.DecPropositional.Solver
diff --git a/src/Data/List/Relation/Binary/Sublist/DecSetoid/Solver.agda b/src/Data/List/Relation/Binary/Sublist/DecSetoid/Solver.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (DecSetoid)
+open import Relation.Binary.Bundles using (DecSetoid)
 
 module Data.List.Relation.Binary.Sublist.DecSetoid.Solver {c ℓ} (S : DecSetoid c ℓ) where
 
diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Core.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Core.agda
@@ -13,7 +13,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (REL)
+open import Relation.Binary.Core using (REL)
 
 module Data.List.Relation.Binary.Sublist.Heterogeneous.Core
        {a b r} {A : Set a} {B : Set b} (R : REL A B r)
diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda
@@ -6,7 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; Reflexive; Decidable)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Reflexive; Decidable)
 
 module Data.List.Relation.Binary.Sublist.Heterogeneous.Solver
   {a r} {A : Set a} (R : Rel A r)
diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid.agda b/src/Data/List/Relation/Binary/Sublist/Setoid.agda
@@ -9,7 +9,8 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 {-# OPTIONS --postfix-projections #-}
 
-open import Relation.Binary using (Setoid; Rel)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
 
 module Data.List.Relation.Binary.Sublist.Setoid
   {c ℓ} (S : Setoid c ℓ) where
diff --git a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
@@ -6,7 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary hiding (Decidable)
+open import Relation.Binary.Definitions hiding (Decidable)
+open import Relation.Binary.Structures using (IsPreorder)
 
 module Data.List.Relation.Binary.Subset.Propositional.Properties
   where
@@ -35,7 +36,8 @@ open import Function.Equivalence using (module Equivalence)
 open import Level using (Level)
 open import Relation.Nullary using (¬_; yes; no)
 open import Relation.Unary using (Decidable; Pred) renaming (_⊆_ to _⋐_)
-open import Relation.Binary using (_⇒_; _Respects_)
+open import Relation.Binary.Core using (_⇒_)
+open import Relation.Binary.Bundles using (Preorder)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; _≗_; isEquivalence; subst; resp; refl; setoid; module ≡-Reasoning)
 import Relation.Binary.Reasoning.Preorder as PreorderReasoning
diff --git a/src/Data/List/Relation/Ternary/Appending.agda b/src/Data/List/Relation/Ternary/Appending.agda
@@ -12,7 +12,7 @@ open import Level using (Level; _⊔_)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
 open import Data.Product as Prod using (∃₂; _×_; _,_; -,_)
-open import Relation.Binary using (REL)
+open import Relation.Binary.Core using (REL)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
 private
diff --git a/src/Data/List/Relation/Ternary/Appending/Properties.agda b/src/Data/List/Relation/Ternary/Appending/Properties.agda
@@ -13,7 +13,8 @@ open import Data.List.Relation.Ternary.Appending
 open import Data.List.Relation.Binary.Pointwise.Base as Pw using (Pointwise; []; _∷_)
 open import Data.List.Relation.Binary.Pointwise.Properties as Pw using (transitive)
 open import Level using (Level)
-open import Relation.Binary using (REL; Rel; Trans)
+open import Relation.Binary.Core using (REL; Rel)
+open import Relation.Binary.Definitions using (Trans)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 private
diff --git a/src/Data/List/Relation/Ternary/Appending/Setoid.agda b/src/Data/List/Relation/Ternary/Appending/Setoid.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Setoid)
+open import Relation.Binary.Bundles using (Setoid)
 
 module Data.List.Relation.Ternary.Appending.Setoid
   {c ℓ} (S : Setoid c ℓ)
diff --git a/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda b/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Setoid)
+open import Relation.Binary.Bundles using (Setoid)
 
 module Data.List.Relation.Ternary.Appending.Setoid.Properties {c l} (S : Setoid c l) where
 
diff --git a/src/Data/List/Relation/Ternary/Interleaving/Setoid.agda b/src/Data/List/Relation/Ternary/Interleaving/Setoid.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Setoid)
+open import Relation.Binary.Bundles using (Setoid)
 
 module Data.List.Relation.Ternary.Interleaving.Setoid {c ℓ} (S : Setoid c ℓ) where
 
diff --git a/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda b/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Setoid)
+open import Relation.Binary.Bundles using (Setoid)
 
 module Data.List.Relation.Ternary.Interleaving.Setoid.Properties
   {c ℓ} (S : Setoid c ℓ) where
diff --git a/src/Data/Tree/AVL.agda b/src/Data/Tree/AVL.agda
@@ -13,7 +13,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
diff --git a/src/Data/Trie/NonEmpty.agda b/src/Data/Trie/NonEmpty.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --sized-types #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Trie.NonEmpty {k e r} (S : StrictTotalOrder k e r) where
 
diff --git a/src/Data/Vec/Membership/DecPropositional.agda b/src/Data/Vec/Membership/DecPropositional.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
diff --git a/src/Data/Vec/Relation/Binary/Equality/DecSetoid.agda b/src/Data/Vec/Relation/Binary/Equality/DecSetoid.agda
@@ -15,7 +15,7 @@ open import Data.Nat.Base using (ℕ)
 import Data.Vec.Relation.Binary.Equality.Setoid as Equality
 import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
 open import Level using (_⊔_)
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 
 open DecSetoid DS
 
diff --git a/src/Data/Vec/Relation/Unary/All/Properties.agda b/src/Data/Vec/Relation/Unary/All/Properties.agda
@@ -20,7 +20,7 @@ open import Level using (Level)
 open import Function.Base using (_∘_; id)
 open import Function.Inverse using (_↔_; inverse)
 open import Relation.Unary using (Pred) renaming (_⊆_ to _⋐_)
-open import Relation.Binary as B using (REL)
+open import Relation.Binary.Core using (REL)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; cong; cong₂; →-to-⟶)
 
diff --git a/src/Relation/Binary/Indexed/Homogeneous/Definitions.agda b/src/Relation/Binary/Indexed/Homogeneous/Definitions.agda
@@ -13,7 +13,8 @@ module Relation.Binary.Indexed.Homogeneous.Definitions where
 
 open import Data.Product.Base using (_×_)
 open import Level using (Level)
-import Relation.Binary as B
+open import Relation.Binary.Core using (_⇒_)
+import Relation.Binary.Definitions as B
 open import Relation.Unary.Indexed using (IPred)
 
 open import Relation.Binary.Indexed.Homogeneous.Core
@@ -31,7 +32,7 @@ module _ (A : I → Set a) where
   syntax Implies A _∼₁_ _∼₂_ = _∼₁_ ⇒[ A ] _∼₂_
 
   Implies : IRel A ℓ₁ → IRel A ℓ₂ → Set _
-  Implies _∼₁_ _∼₂_ = ∀ {i} → _∼₁_ B.⇒ (_∼₂_ {i})
+  Implies _∼₁_ _∼₂_ = ∀ {i} → _∼₁_ ⇒ (_∼₂_ {i})
 
   Reflexive : IRel A ℓ → Set _
   Reflexive _∼_ = ∀ {i} → B.Reflexive (_∼_ {i})
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
@@ -16,7 +16,8 @@ open import Data.Sum.Base as Sum hiding (map)
 open import Function.Base
 open import Function.Bundles using
   (Injection; module Injection; module Equivalence; _⇔_; _↔_; mk↔′)
-open import Relation.Binary using (Setoid; module Setoid; Decidable)
+open import Relation.Binary.Bundles using (Setoid; module Setoid)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary
 open import Relation.Nullary.Negation
 open import Relation.Nullary.Reflects using (invert)
