More Relation.Binary simplifications (#2053)

Author: Saransh-cpp

README/Case.agda

@@ -14,7 +14,6 @@ open import Data.Maybe hiding (from-just)
 open import Data.Nat   hiding (pred)
 open import Function.Base using (case_of_; case_return_of_)
 open import Relation.Nullary
-open import Relation.Binary
 
 ------------------------------------------------------------------------
 -- Different types of pattern-matching lambdas

README/Data/Record.agda

@@ -15,7 +15,7 @@ open import Data.Product.Base using (_,_)
 open import Data.String
 open import Function.Base using (flip)
 open import Level
-open import Relation.Binary
+open import Relation.Binary.Definitions using (Symmetric; Transitive)
 
 import Data.Record as Record
 

README/Data/Wrap.agda

@@ -15,7 +15,6 @@ open import Data.Nat
 open import Data.Nat.Properties
 open import Data.Product.Base using (_,_; ∃; ∃₂; _×_)
 open import Level using (Level)
-open import Relation.Binary
 
 private
   variable

src/Algebra/Bundles.agda

@@ -14,7 +14,7 @@ module Algebra.Bundles where
 import Algebra.Bundles.Raw as Raw
 open import Algebra.Core
 open import Algebra.Structures
-open import Relation.Binary
+open import Relation.Binary.Core using (Rel)
 open import Function.Base
 import Relation.Nullary as N
 open import Level

src/Algebra/Construct/LexProduct.agda

@@ -12,7 +12,8 @@ open import Data.Product.Base using (_×_; _,_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (Pointwise)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_∘_)
-open import Relation.Binary
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary using (¬_; does; yes; no)
 open import Relation.Nullary.Negation using (contradiction; contradiction₂)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning

src/Algebra/Construct/LiftedChoice.agda

@@ -11,7 +11,8 @@ open import Algebra
 module Algebra.Construct.LiftedChoice where
 
 open import Algebra.Consequences.Base
-open import Relation.Binary
+open import Relation.Binary.Core using (Rel; _⇒_; _Preserves_⟶_)
+open import Relation.Binary.Structures using (IsEquivalence)
 open import Relation.Nullary using (¬_; yes; no)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Product.Base using (_×_; _,_)

src/Algebra/Construct/NaturalChoice/Base.agda

@@ -10,7 +10,7 @@
 open import Algebra.Core
 open import Level as L hiding (_⊔_)
 open import Function.Base using (flip)
-open import Relation.Binary
+open import Relation.Binary.Bundles using (TotalPreorder)
 open import Relation.Binary.Construct.Flip.EqAndOrd using ()
   renaming (totalPreorder to flipOrder)
 import Relation.Binary.Properties.TotalOrder as TotalOrderProperties

src/Algebra/Construct/NaturalChoice/Max.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary
+open import Relation.Binary.Bundles using (TotalOrder)
 
 module Algebra.Construct.NaturalChoice.Max
   {a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂) where

src/Algebra/Construct/NaturalChoice/MaxOp.agda

@@ -11,7 +11,8 @@ open import Algebra.Core
 open import Algebra.Construct.NaturalChoice.Base
 import Algebra.Construct.NaturalChoice.MinOp as MinOp
 open import Function.Base using (flip)
-open import Relation.Binary
+open import Relation.Binary.Core using (_Preserves_⟶_)
+open import Relation.Binary.Bundles using (TotalPreorder)
 open import Relation.Binary.Construct.Flip.EqAndOrd using ()
   renaming (totalPreorder to flipOrder)
 

src/Algebra/Construct/NaturalChoice/Min.agda

@@ -12,7 +12,7 @@ open import Algebra.Construct.NaturalChoice.Base
 open import Data.Sum.Base using (inj₁; inj₂; [_,_])
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
-open import Relation.Binary
+open import Relation.Binary.Bundles using (TotalOrder)
 import Algebra.Construct.NaturalChoice.MinOp as MinOp
 
 module Algebra.Construct.NaturalChoice.Min