agda · MatthewDaggitt · Aug 20, 2023 · Jul 3, 2023 · Aug 11, 2023 · Jun 26, 2023
diff --git a/README/Case.agda b/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

diff --git a/README/Data/Record.agda b/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
 

diff --git a/README/Data/Wrap.agda b/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

diff --git a/src/Algebra/Bundles.agda b/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

diff --git a/src/Algebra/Construct/LexProduct.agda b/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

diff --git a/src/Algebra/Construct/LiftedChoice.agda b/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 (_×_; _,_)

diff --git a/src/Algebra/Construct/NaturalChoice/Base.agda b/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

diff --git a/src/Algebra/Construct/NaturalChoice/Max.agda b/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

diff --git a/src/Algebra/Construct/NaturalChoice/MaxOp.agda b/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)
 

diff --git a/src/Algebra/Construct/NaturalChoice/Min.agda b/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

diff --git a/src/Algebra/Construct/NaturalChoice/MinMaxOp.agda b/src/Algebra/Construct/NaturalChoice/MinMaxOp.agda
@@ -13,7 +13,8 @@ open import Algebra.Construct.NaturalChoice.Base
 open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id; _∘_; flip)
-open import Relation.Binary
+open import Relation.Binary.Core using (_Preserves_⟶_)
+open import Relation.Binary.Bundles using (TotalPreorder)
 open import Relation.Binary.Consequences
 
 module Algebra.Construct.NaturalChoice.MinMaxOp

diff --git a/src/Algebra/Construct/NaturalChoice/MinOp.agda b/src/Algebra/Construct/NaturalChoice/MinOp.agda
@@ -13,7 +13,9 @@ open import Algebra.Construct.NaturalChoice.Base
 open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id; _∘_)
-open import Relation.Binary
+open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
+open import Relation.Binary.Bundles using (TotalPreorder)
+open import Relation.Binary.Definitions using (Maximum; Minimum)
 open import Relation.Binary.Consequences
 
 module Algebra.Construct.NaturalChoice.MinOp

diff --git a/src/Algebra/Lattice/Bundles.agda b/src/Algebra/Lattice/Bundles.agda
@@ -21,7 +21,8 @@ open import Algebra.Structures
 import Algebra.Lattice.Bundles.Raw as Raw
 open import Algebra.Lattice.Structures
 open import Level using (suc; _⊔_)
-open import Relation.Binary
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Core using (Rel)
 
 ------------------------------------------------------------------------
 -- Re-export definitions of 'raw' bundles

diff --git a/src/Algebra/Lattice/Construct/LiftedChoice.agda b/src/Algebra/Lattice/Construct/LiftedChoice.agda
@@ -9,7 +9,8 @@
 open import Algebra
 open import Algebra.Lattice
 open import Algebra.Construct.LiftedChoice
-open import Relation.Binary
+open import Relation.Binary.Core using (Rel; _Preserves_⟶_)
+open import Relation.Binary.Structures using (IsEquivalence)
 open import Level using (Level)
 
 module Algebra.Lattice.Construct.LiftedChoice where

diff --git a/src/Algebra/Lattice/Construct/NaturalChoice/MaxOp.agda b/src/Algebra/Lattice/Construct/NaturalChoice/MaxOp.agda
@@ -9,7 +9,7 @@
 
 open import Algebra.Construct.NaturalChoice.Base
 import Algebra.Lattice.Construct.NaturalChoice.MinOp as MinOp
-open import Relation.Binary
+open import Relation.Binary.Bundles using (TotalPreorder)
 
 module Algebra.Lattice.Construct.NaturalChoice.MaxOp
   {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (maxOp : MaxOperator O)

diff --git a/src/Algebra/Lattice/Construct/NaturalChoice/MinMaxOp.agda b/src/Algebra/Lattice/Construct/NaturalChoice/MinMaxOp.agda
@@ -8,7 +8,7 @@
 
 open import Algebra.Lattice.Bundles
 open import Algebra.Construct.NaturalChoice.Base
-open import Relation.Binary
+open import Relation.Binary.Bundles using (TotalPreorder)
 
 module Algebra.Lattice.Construct.NaturalChoice.MinMaxOp
   {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂}

diff --git a/src/Algebra/Lattice/Construct/NaturalChoice/MinOp.agda b/src/Algebra/Lattice/Construct/NaturalChoice/MinOp.agda
@@ -10,7 +10,7 @@
 open import Algebra.Bundles
 open import Algebra.Lattice.Bundles
 open import Algebra.Construct.NaturalChoice.Base
-open import Relation.Binary
+open import Relation.Binary.Bundles using (TotalPreorder)
 
 module Algebra.Lattice.Construct.NaturalChoice.MinOp
   {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (minOp : MinOperator O) where

diff --git a/src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda b/src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda
@@ -16,7 +16,7 @@ import Algebra.Consequences.Setoid as Consequences
 import Algebra.Morphism.MagmaMonomorphism as MagmaMonomorphisms
 import Algebra.Lattice.Properties.Lattice as LatticeProperties
 open import Data.Product.Base using (_,_; map)
-open import Relation.Binary
+open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.Morphism.RelMonomorphism as RelMonomorphisms
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 

diff --git a/src/Algebra/Lattice/Properties/BooleanAlgebra.agda b/src/Algebra/Lattice/Properties/BooleanAlgebra.agda
@@ -22,7 +22,6 @@ open import Algebra.Consequences.Setoid setoid
 open import Algebra.Bundles
 open import Algebra.Lattice.Structures _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
-open import Relation.Binary
 open import Function.Base using (id; _$_; _⟨_⟩_)
 open import Function.Bundles using (_⇔_; module Equivalence)
 open import Data.Product.Base using (_,_)

diff --git a/src/Algebra/Lattice/Properties/Lattice.agda b/src/Algebra/Lattice/Properties/Lattice.agda
@@ -8,7 +8,7 @@
 
 open import Algebra.Lattice.Bundles
 import Algebra.Lattice.Properties.Semilattice as SemilatticeProperties
-open import Relation.Binary
+open import Relation.Binary.Bundles using (Poset)
 import Relation.Binary.Lattice as R
 open import Function.Base
 open import Data.Product.Base using (_,_; swap)

diff --git a/src/Algebra/Module/Bundles.agda b/src/Algebra/Module/Bundles.agda
@@ -34,7 +34,7 @@ open import Algebra.Module.Definitions
 open import Algebra.Properties.Group
 open import Function.Base
 open import Level
-open import Relation.Binary
+open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary    using (¬_)
 import Relation.Binary.Reasoning.Setoid as SetR
 

diff --git a/src/Algebra/Module/Definitions.agda b/src/Algebra/Module/Definitions.agda
@@ -7,8 +7,6 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary
-
 module Algebra.Module.Definitions where
 
   import Algebra.Module.Definitions.Left as L

diff --git a/src/Algebra/Module/Definitions/Bi.agda b/src/Algebra/Module/Definitions/Bi.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary
+open import Relation.Binary.Core using (Rel)
 
 -- The properties are parameterised by the three carriers and
 -- the result equality.

diff --git a/src/Algebra/Module/Definitions/Left.agda b/src/Algebra/Module/Definitions/Left.agda
@@ -6,7 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary
+open import Relation.Binary.Core
+  using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
 
 -- The properties are parameterised by the two carriers and
 -- the result equality.

diff --git a/src/Algebra/Module/Definitions/Right.agda b/src/Algebra/Module/Definitions/Right.agda
@@ -6,7 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary
+open import Relation.Binary.Core
+  using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
 
 -- The properties are parameterised by the two carriers and
 -- the result equality.

diff --git a/src/Algebra/Morphism.agda b/src/Algebra/Morphism.agda
@@ -13,7 +13,7 @@ open import Algebra
 import Algebra.Properties.Group as GroupP
 open import Function.Base
 open import Level
-open import Relation.Binary
+open import Relation.Binary.Core using (Rel; _Preserves_⟶_)
 import Relation.Binary.Reasoning.Setoid as EqR
 
 private

diff --git a/src/Algebra/Properties/CommutativeSemiring/Exp/TCOptimised.agda b/src/Algebra/Properties/CommutativeSemiring/Exp/TCOptimised.agda
@@ -9,7 +9,6 @@
 open import Algebra
 open import Data.Nat.Base as ℕ using (zero; suc)
 import Data.Nat.Properties as ℕ
-open import Relation.Binary
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 module Algebra.Properties.CommutativeSemiring.Exp.TCOptimised

diff --git a/src/Algebra/Properties/Lattice.agda b/src/Algebra/Properties/Lattice.agda
@@ -8,7 +8,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Lattice.Bundles
-open import Relation.Binary
+open import Relation.Binary.Core using (Rel)
 open import Function.Base
 open import Function.Bundles using (module Equivalence; _⇔_)
 open import Data.Product.Base using (_,_; swap)

diff --git a/src/Algebra/Properties/Monoid/Divisibility.agda b/src/Algebra/Properties/Monoid/Divisibility.agda
@@ -8,7 +8,10 @@
 
 open import Algebra using (Monoid)
 open import Data.Product.Base using (_,_)
-open import Relation.Binary
+open import Relation.Binary.Core using (_⇒_)
+open import Relation.Binary.Bundles using (Preorder)
+open import Relation.Binary.Structures using (IsPreorder; IsEquivalence)
+open import Relation.Binary.Definitions using (Reflexive)
 
 module Algebra.Properties.Monoid.Divisibility
   {a ℓ} (M : Monoid a ℓ) where

diff --git a/src/Algebra/Properties/Monoid/Mult.agda b/src/Algebra/Properties/Monoid/Mult.agda
@@ -8,7 +8,7 @@
 
 open import Algebra.Bundles using (Monoid)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero)
-open import Relation.Binary
+open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 module Algebra.Properties.Monoid.Mult {a ℓ} (M : Monoid a ℓ) where

diff --git a/src/Algebra/Properties/Semiring/Exp.agda b/src/Algebra/Properties/Semiring/Exp.agda
@@ -8,7 +8,7 @@
 
 open import Algebra
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
-open import Relation.Binary
+open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Data.Nat.Properties as ℕ
 

diff --git a/src/Algebra/Properties/Semiring/Exp/TCOptimised.agda b/src/Algebra/Properties/Semiring/Exp/TCOptimised.agda
@@ -9,7 +9,7 @@
 open import Algebra
 open import Data.Nat.Base as ℕ using (zero; suc)
 import Data.Nat.Properties as ℕ
-open import Relation.Binary
+open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 module Algebra.Properties.Semiring.Exp.TCOptimised

diff --git a/src/Algebra/Properties/Semiring/Exp/TailRecursiveOptimised.agda b/src/Algebra/Properties/Semiring/Exp/TailRecursiveOptimised.agda
@@ -9,7 +9,7 @@
 open import Algebra
 open import Data.Nat.Base as ℕ using (zero; suc)
 import Data.Nat.Properties as ℕ
-open import Relation.Binary
+open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
 
 module Algebra.Properties.Semiring.Exp.TailRecursiveOptimised
   {a ℓ} (S : Semiring a ℓ) where

diff --git a/src/Algebra/Solver/Ring.agda b/src/Algebra/Solver/Ring.agda
@@ -39,7 +39,6 @@ open import Algebra.Morphism
 open _-Raw-AlmostCommutative⟶_ morphism renaming (⟦_⟧ to ⟦_⟧′)
 open import Algebra.Properties.Semiring.Exp semiring
 
-open import Relation.Binary
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Binary.Reasoning.Setoid setoid
 import Relation.Binary.PropositionalEquality.Core as PropEq

diff --git a/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda b/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda
@@ -16,7 +16,7 @@ import Algebra.Morphism as Morphism
 import Algebra.Morphism.Definitions as MorphismDefinitions
 open import Function.Base using (id)
 open import Level
-open import Relation.Binary
+open import Relation.Binary.Core using (Rel)
 
 
 record IsAlmostCommutativeRing {a ℓ} {A : Set a} (_≈_ : Rel A ℓ)

diff --git a/src/Algebra/Solver/Ring/Simple.agda b/src/Algebra/Solver/Ring/Simple.agda
@@ -8,7 +8,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Solver.Ring.AlmostCommutativeRing
-open import Relation.Binary
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.Consequences using (dec⇒weaklyDec)
 
 module Algebra.Solver.Ring.Simple

diff --git a/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda b/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda
@@ -12,7 +12,11 @@ open import Codata.Guarded.Stream as Stream using (Stream; head; tail)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Function.Base using (_∘_; _on_)
 open import Level using (Level; _⊔_)
-open import Relation.Binary
+open import Relation.Binary.Core using (REL; _⇒_)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions
+  using (Reflexive; Sym; Trans; Antisym; Symmetric; Transitive)
+open import Relation.Binary.Structures using (IsEquivalence)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as P
 

diff --git a/src/Codata/Musical/Colist.agda b/src/Codata/Musical/Colist.agda
@@ -28,7 +28,9 @@ open import Function.Base
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Inverse as Inv using (_↔_; _↔̇_; Inverse; inverse)
 open import Level using (_⊔_)
-open import Relation.Binary
+open import Relation.Binary.Core using (Rel; _⇒_)
+open import Relation.Binary.Bundles using (Poset; Setoid; Preorder)
+open import Relation.Binary.Definitions using (Transitive; Antisymmetric)
 import Relation.Binary.Construct.FromRel as Ind
 import Relation.Binary.Reasoning.Preorder as PreR
 import Relation.Binary.Reasoning.PartialOrder as POR

diff --git a/src/Codata/Musical/Colist/Bisimilarity.agda b/src/Codata/Musical/Colist/Bisimilarity.agda
@@ -11,7 +11,10 @@ module Codata.Musical.Colist.Bisimilarity where
 open import Codata.Musical.Colist.Base
 open import Codata.Musical.Notation
 open import Level using (Level)
-open import Relation.Binary
+open import Relation.Binary.Core using (Rel; _=[_]⇒_)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions
+  using (Reflexive; Symmetric; Transitive)
 
 private
   variable

diff --git a/src/Codata/Musical/Colist/Relation/Unary/Any/Properties.agda b/src/Codata/Musical/Colist/Relation/Unary/Any/Properties.agda
@@ -21,7 +21,7 @@ open import Function.Base using (_∋_; _∘_)
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Inverse as Inv using (_↔_; _↔̇_; Inverse; inverse)
 open import Level using (Level; _⊔_)
-open import Relation.Binary
+open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; refl; cong)
 open import Relation.Unary using (Pred)

diff --git a/src/Codata/Musical/Conat.agda b/src/Codata/Musical/Conat.agda
@@ -11,7 +11,9 @@ module Codata.Musical.Conat where
 open import Codata.Musical.Notation
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Function.Base using (_∋_)
-open import Relation.Binary
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions
+  using (Reflexive; Symmetric; Transitive)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 ------------------------------------------------------------------------

diff --git a/src/Codata/Musical/Covec.agda b/src/Codata/Musical/Covec.agda
@@ -17,7 +17,10 @@ open import Data.Vec.Base using (Vec; []; _∷_)
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_∋_)
 open import Level using (Level)
-open import Relation.Binary
+open import Relation.Binary.Core using (_⇒_; _=[_]⇒_)
+open import Relation.Binary.Bundles using (Setoid; Poset)
+open import Relation.Binary.Definitions
+  using (Reflexive; Symmetric; Transitive; Antisymmetric)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 private