More simplifications for Relation.Binary imports (#2038)

Author: Saransh-cpp

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
 
 ------------------------------------------------------------------------