More simplifications for Relation.Binary imports (#2038)

README/Nary.agda

@@ -19,7 +19,7 @@ open import Data.Product.Base using (_×_; _,_)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (id; flip; _∘′_)
 open import Relation.Nullary
-open import Relation.Binary using (module Tri); open Tri
+open import Relation.Binary.Definitions using (module Tri); open Tri
 open import Relation.Binary.PropositionalEquality
 
 private

src/Data/AVL.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
  {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)

src/Data/AVL/Indexed.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.Indexed
  {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) where

src/Data/AVL/NonEmpty/Propositional.agda

@@ -6,7 +6,9 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; IsStrictTotalOrder; StrictTotalOrder)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Structures using (IsStrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
 
 module Data.AVL.NonEmpty.Propositional

src/Data/List/Extrema.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (TotalOrder; Setoid)
+open import Relation.Binary.Bundles using (TotalOrder; Setoid)
 
 module Data.List.Extrema
  {b ℓ₁ ℓ₂} (totalOrder : TotalOrder b ℓ₁ ℓ₂) where

src/Data/List/Fresh/Properties.agda

@@ -12,7 +12,8 @@ open import Level using (Level; _⊔_; Lift)
 open import Data.Product.Base using (_,_)
 open import Relation.Nullary
 open import Relation.Unary as U using (Pred)
-open import Relation.Binary as B using (Rel)
+import Relation.Binary.Definitions as B
+open import Relation.Binary.Core using (Rel)
 
 open import Data.List.Fresh
 

src/Data/List/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 using (_≡_)
 open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 

src/Data/List/Membership/DecSetoid.agda

@@ -6,7 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Decidable; DecSetoid)
+open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Binary.Bundles using (DecSetoid)
 open import Relation.Nullary.Decidable using (¬?)
 
 module Data.List.Membership.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where

src/Data/List/Properties.agda

@@ -34,10 +34,10 @@ open import Data.Fin.Properties using (toℕ-cast)
 open import Function.Base using (id; _∘_; _∘′_; _∋_; _-⟨_∣; ∣_⟩-_; _$_; const; flip)
 open import Function.Definitions using (Injective)
 open import Level using (Level)
-open import Relation.Binary as B using (DecidableEquality)
+open import Relation.Binary.Definitions as B using (DecidableEquality)
 import Relation.Binary.Reasoning.Setoid as EqR
 open import Relation.Binary.PropositionalEquality as P hiding ([_])
-open import Relation.Binary as B using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no; contradiction)
 open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋; ¬?; _×-dec_)

src/Data/List/Relation/Binary/Equality/DecSetoid.agda

@@ -14,7 +14,7 @@ module Data.List.Relation.Binary.Equality.DecSetoid
 import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
 import Data.List.Relation.Binary.Pointwise as PW
 open import Level
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 open DecSetoid DS
 
 ------------------------------------------------------------------------

src/Data/List/Relation/Binary/Equality/Setoid.agda

@@ -7,7 +7,9 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Core using (Op₂)
-open import Relation.Binary using (Setoid)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions using (Transitive; Symmetric; Reflexive; _Respects_)
+open import Relation.Binary.Structures using (IsEquivalence)
 
 module Data.List.Relation.Binary.Equality.Setoid {a ℓ} (S : Setoid a ℓ) where
 
@@ -17,7 +19,7 @@ open import Data.List.Relation.Binary.Pointwise as PW using (Pointwise)
 open import Data.List.Relation.Unary.Unique.Setoid S using (Unique)
 open import Function.Base using (_∘_)
 open import Level
-open import Relation.Binary renaming (Rel to Rel₂)
+open import Relation.Binary.Core renaming (Rel to Rel₂)
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Binary.Properties.Setoid S using (≉-resp₂)
 open import Relation.Unary as U using (Pred)

src/Data/List/Relation/Binary/Infix/Heterogeneous.agda

@@ -9,7 +9,7 @@
 module Data.List.Relation.Binary.Infix.Heterogeneous where
 
 open import Level
-open import Relation.Binary using (REL; _⇒_)
+open import Relation.Binary.Core using (REL; _⇒_)
 open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.List.Relation.Binary.Pointwise
  using (Pointwise)

src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda

@@ -20,7 +20,8 @@ open import Function.Base using (case_of_; _$′_)
 open import Relation.Nullary.Decidable using (yes; no; does; map′; _⊎-dec_)
 open import Relation.Nullary.Negation using (¬_; contradiction)
 open import Relation.Unary as U using (Pred)
-open import Relation.Binary using (REL; _⇒_; Decidable; Trans; Antisym)
+open import Relation.Binary.Core using (REL; _⇒_)
+open import Relation.Binary.Definitions using (Decidable; Trans; Antisym)
 open import Relation.Binary.PropositionalEquality.Core using (_≢_; refl; cong)
 open import Data.List.Relation.Binary.Pointwise.Base as Pointwise using (Pointwise)
 open import Data.List.Relation.Binary.Infix.Heterogeneous

src/Data/List/Relation/Binary/Pointwise.agda

@@ -25,7 +25,10 @@ open import Level
 open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec using (map′)
 open import Relation.Unary as U using (Pred)
-open import Relation.Binary renaming (Rel to Rel₂)
+open import Relation.Binary.Core renaming (Rel to Rel₂)
+open import Relation.Binary.Definitions using (_Respects_; _Respects₂_)
+open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder; Poset)
+open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence; IsPartialOrder; IsPreorder)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as P
 

src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda

@@ -22,7 +22,7 @@ import Data.List.Relation.Binary.Sublist.Setoid.Properties
 open import Data.Product using (∃; _,_; proj₂)
 open import Function.Base
 open import Level using (Level)
-open import Relation.Binary using (_Respects_)
+open import Relation.Binary.Definitions using (_Respects_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary using (Pred)
 

src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda

@@ -6,7 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; Setoid; _⇒_; _Preserves_⟶_)
+open import Relation.Binary.Core using (Rel; _⇒_; _Preserves_⟶_)
+open import Relation.Binary.Bundles using (Setoid)
 
 module Data.List.Relation.Binary.Sublist.Setoid.Properties
  {c ℓ} (S : Setoid c ℓ) where
@@ -20,7 +21,7 @@ open import Data.Product using (∃; _,_; proj₂)
 open import Function.Base
 open import Function.Bundles using (_⇔_; _⤖_)
 open import Level
-open import Relation.Binary using () renaming (Decidable to Decidable₂)
+open import Relation.Binary.Definitions using () renaming (Decidable to Decidable₂)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 open import Relation.Binary.Structures using (IsDecTotalOrder)
 open import Relation.Unary using (Pred; Decidable; Irrelevant)

src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda

@@ -9,7 +9,7 @@
 module Data.List.Relation.Binary.Suffix.Heterogeneous where
 
 open import Level
-open import Relation.Binary using (REL; _⇒_)
+open import Relation.Binary.Core using (REL; _⇒_)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Binary.Pointwise.Base as Pointwise
  using (Pointwise; []; _∷_)

src/Data/List/Relation/Unary/AllPairs/Core.agda

@@ -12,7 +12,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 
 module Data.List.Relation.Unary.AllPairs.Core
  {a ℓ} {A : Set a} (R : Rel A ℓ) where

src/Data/List/Relation/Unary/AllPairs/Properties.agda

@@ -19,7 +19,8 @@ open import Data.Nat.Base using (zero; suc; _<_; z≤n; s≤s)
 open import Data.Nat.Properties using (≤-refl; m<n⇒m<1+n)
 open import Function.Base using (_∘_; flip)
 open import Level using (Level)
-open import Relation.Binary using (Rel; DecSetoid)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (DecSetoid)
 open import Relation.Binary.PropositionalEquality.Core using (_≢_)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Nullary.Decidable using (does)

src/Data/List/Relation/Unary/Grouped/Properties.agda

@@ -16,7 +16,8 @@ open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _
 open import Data.List.Relation.Unary.Grouped
 open import Function.Base using (_∘_)
 open import Function.Bundles using (module Equivalence; _⇔_)
-open import Relation.Binary as B using (REL; Rel)
+open import Relation.Binary.Definitions as B
+open import Relation.Binary.Core using (REL; Rel)
 open import Relation.Unary as U using (Pred)
 open import Relation.Nullary using (¬_; does; yes; no)
 open import Relation.Nullary.Negation using (contradiction)

src/Data/List/Relation/Unary/Linked.agda

@@ -16,7 +16,8 @@ open import Data.Maybe.Relation.Binary.Connected
  using (Connected; just; just-nothing)
 open import Function.Base using (id; _∘_)
 open import Level using (Level; _⊔_)
-open import Relation.Binary as B using (Rel; _⇒_)
+open import Relation.Binary.Definitions as B
+open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)

src/Data/List/Sort.agda

@@ -10,7 +10,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Data.List.Base using (List)
-open import Relation.Binary using (DecTotalOrder)
+open import Relation.Binary.Bundles using (DecTotalOrder)
 
 module Data.List.Sort
  {a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂)

src/Data/List/Sort/Base.agda

@@ -9,7 +9,7 @@
 open import Data.List.Base using (List)
 open import Data.List.Relation.Binary.Permutation.Propositional
 open import Level using (_⊔_)
-open import Relation.Binary using (TotalOrder)
+open import Relation.Binary.Bundles using (TotalOrder)
 
 module Data.List.Sort.Base
  {a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂)

src/Data/List/Sort/MergeSort.agda

@@ -26,7 +26,7 @@ open import Data.Nat.Induction
 open import Data.Nat.Properties using (m<n⇒m<1+n)
 open import Data.Product.Base as Prod using (_,_)
 open import Function.Base using (_∘_)
-open import Relation.Binary using (DecTotalOrder)
+open import Relation.Binary.Bundles using (DecTotalOrder)
 open import Relation.Nullary.Negation using (¬_)
 
 module Data.List.Sort.MergeSort

src/Data/Maybe/Properties.agda

@@ -17,7 +17,7 @@ open import Data.Product.Base using (_,_)
 open import Function.Base using (_∋_; id; _∘_; _∘′_)
 open import Function.Definitions using (Injective)
 open import Level using (Level)
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Decidable using (map′)

src/Data/Nat/Divisibility/Core.agda

@@ -16,7 +16,7 @@ open import Data.Nat.Base using (ℕ; _*_)
 open import Data.Nat.Properties
 open import Level using (0ℓ)
 open import Relation.Nullary.Negation using (¬_)
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; cong₂; module ≡-Reasoning)
 

src/Data/Product/Effectful/Examples.agda

@@ -18,7 +18,7 @@ open import Data.Product
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Function.Base using (id)
 import Function.Identity.Effectful as Id
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 ------------------------------------------------------------------------

src/Data/Product/Properties.agda

@@ -13,7 +13,7 @@ open import Data.Product.Base
 open import Function.Base using (_∋_; _∘_; id)
 open import Function.Bundles using (_↔_; mk↔′)
 open import Level using (Level)
-open import Relation.Binary using (DecidableEquality)
+open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable as Dec using (Dec; yes; no)
 

src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda

@@ -13,7 +13,7 @@ open import Data.Product
 open import Data.Product.Relation.Binary.Pointwise.Dependent
 open import Function.Base
 open import Function.Inverse using (Inverse)
-open import Relation.Binary using (_⇒_)
+open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.HeterogeneousEquality as H using (_≅_)
 open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)

src/Data/Sum/Properties.agda

@@ -12,7 +12,7 @@ open import Level
 open import Data.Sum.Base
 open import Function.Base using (_∋_; _∘_; id)
 open import Function.Bundles using (mk↔′; _↔_)
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Decidable using (map′)

src/Data/These/Properties.agda

@@ -11,7 +11,7 @@ module Data.These.Properties where
 open import Data.Product
 open import Data.These.Base
 open import Function.Base using (_∘_)
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_)
 

src/Data/Tree/AVL/Indexed.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Indexed
  {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) where
@@ -19,7 +19,7 @@ open import Data.List.Base as List using (List)
 open import Data.DifferenceList using (DiffList; []; _∷_; _++_)
 open import Function.Base as F hiding (const)
 open import Relation.Unary
-open import Relation.Binary using (_Respects_; Tri; tri<; tri≈; tri>)
+open import Relation.Binary.Definitions using (_Respects_; Tri; tri<; tri≈; tri>)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 private

src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Indexed.Relation.Unary.All
  {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)

src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Indexed.Relation.Unary.Any
  {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)

src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties
  {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
@@ -21,7 +21,7 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function.Base as F
 open import Level using (Level)
 
-open import Relation.Binary using (_Respects_; tri<; tri≈; tri>)
+open import Relation.Binary.Definitions using (_Respects_; tri<; tri≈; tri>)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_) renaming (refl to ≡-refl)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Nullary.Negation using (contradiction)

src/Data/Tree/AVL/Map.agda

@@ -8,7 +8,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Map
  {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)

src/Data/Tree/AVL/Map/Membership/Propositional.agda

@@ -7,7 +7,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Map.Membership.Propositional
  {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
@@ -21,7 +21,7 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; _∘′_)
 open import Level using (Level)
 
-open import Relation.Binary using (Transitive; Symmetric; _Respectsˡ_)
+open import Relation.Binary.Definitions using (Transitive; Symmetric; _Respectsˡ_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Construct.Intersection using (_∩_)
 open import Relation.Binary.PropositionalEquality