From ed2b0dedc2d929191fbeb4a24310a194b7e25d5d Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Sun, 20 Aug 2023 00:19:20 -0400 Subject: [PATCH] More `Relation.Binary` simplifications (#2053) --- README/Case.agda | 1 - README/Data/Record.agda | 2 +- README/Data/Wrap.agda | 1 - src/Algebra/Bundles.agda | 2 +- src/Algebra/Construct/LexProduct.agda | 3 ++- src/Algebra/Construct/LiftedChoice.agda | 3 ++- src/Algebra/Construct/NaturalChoice/Base.agda | 2 +- src/Algebra/Construct/NaturalChoice/Max.agda | 2 +- src/Algebra/Construct/NaturalChoice/MaxOp.agda | 3 ++- src/Algebra/Construct/NaturalChoice/Min.agda | 2 +- src/Algebra/Construct/NaturalChoice/MinMaxOp.agda | 3 ++- src/Algebra/Construct/NaturalChoice/MinOp.agda | 4 +++- src/Algebra/Lattice/Bundles.agda | 3 ++- src/Algebra/Lattice/Construct/LiftedChoice.agda | 3 ++- .../Lattice/Construct/NaturalChoice/MaxOp.agda | 2 +- .../Lattice/Construct/NaturalChoice/MinMaxOp.agda | 2 +- .../Lattice/Construct/NaturalChoice/MinOp.agda | 2 +- .../Lattice/Morphism/LatticeMonomorphism.agda | 2 +- src/Algebra/Lattice/Properties/BooleanAlgebra.agda | 1 - src/Algebra/Lattice/Properties/Lattice.agda | 2 +- src/Algebra/Module/Bundles.agda | 2 +- src/Algebra/Module/Definitions.agda | 2 -- src/Algebra/Module/Definitions/Bi.agda | 2 +- src/Algebra/Module/Definitions/Left.agda | 3 ++- src/Algebra/Module/Definitions/Right.agda | 3 ++- src/Algebra/Morphism.agda | 2 +- .../CommutativeSemiring/Exp/TCOptimised.agda | 1 - src/Algebra/Properties/Lattice.agda | 2 +- src/Algebra/Properties/Monoid/Divisibility.agda | 5 ++++- src/Algebra/Properties/Monoid/Mult.agda | 2 +- src/Algebra/Properties/Semiring/Exp.agda | 2 +- src/Algebra/Properties/Semiring/Exp/TCOptimised.agda | 2 +- .../Semiring/Exp/TailRecursiveOptimised.agda | 2 +- src/Algebra/Solver/Ring.agda | 1 - src/Algebra/Solver/Ring/AlmostCommutativeRing.agda | 2 +- src/Algebra/Solver/Ring/Simple.agda | 2 +- .../Guarded/Stream/Relation/Binary/Pointwise.agda | 6 +++++- src/Codata/Musical/Colist.agda | 4 +++- src/Codata/Musical/Colist/Bisimilarity.agda | 5 ++++- .../Colist/Relation/Unary/Any/Properties.agda | 2 +- src/Codata/Musical/Conat.agda | 4 +++- src/Codata/Musical/Covec.agda | 5 ++++- src/Codata/Musical/Stream.agda | 4 +++- src/Codata/Sized/Colist/Bisimilarity.agda | 6 +++++- src/Codata/Sized/Conat/Bisimilarity.agda | 3 ++- src/Codata/Sized/Covec/Bisimilarity.agda | 3 ++- src/Codata/Sized/Cowriter/Bisimilarity.agda | 6 +++++- src/Codata/Sized/Delay/Bisimilarity.agda | 3 ++- src/Codata/Sized/M/Bisimilarity.agda | 6 +++++- src/Codata/Sized/Stream/Bisimilarity.agda | 6 +++++- src/Data/Bool/Properties.agda | 8 +++++++- src/Data/Container/Indexed.agda | 10 +++++----- src/Data/Fin/Properties.agda | 7 ++++++- src/Data/Fin/Subset/Properties.agda | 7 ++++++- src/Data/List/Fresh.agda | 7 ++++--- .../List/Fresh/Membership/Setoid/Properties.agda | 2 +- src/Data/List/Membership/Setoid/Properties.agda | 4 +++- src/Data/List/Relation/Binary/Lex.agda | 5 ++++- .../Binary/Sublist/Heterogeneous/Properties.agda | 7 ++++++- .../Relation/Binary/Subset/Setoid/Properties.agda | 6 +++++- .../Binary/Suffix/Heterogeneous/Properties.agda | 5 +++-- src/Data/List/Relation/Unary/All.agda | 3 ++- src/Data/List/Relation/Unary/All/Properties.agda | 6 ++++-- src/Data/List/Relation/Unary/AllPairs.agda | 4 ++-- src/Data/List/Relation/Unary/Any/Properties.agda | 3 ++- src/Data/List/Relation/Unary/Grouped.agda | 3 ++- src/Data/List/Relation/Unary/Linked/Properties.agda | 4 +++- src/Data/List/Relation/Unary/Sorted/TotalOrder.agda | 4 ++-- .../Relation/Unary/Sorted/TotalOrder/Properties.agda | 3 ++- .../List/Relation/Unary/Unique/DecPropositional.agda | 3 ++- .../Unary/Unique/DecPropositional/Properties.agda | 2 +- src/Data/List/Relation/Unary/Unique/DecSetoid.agda | 2 +- .../Relation/Unary/Unique/DecSetoid/Properties.agda | 2 +- .../Unary/Unique/Propositional/Properties.agda | 3 ++- src/Data/List/Relation/Unary/Unique/Setoid.agda | 3 ++- .../Relation/Unary/Unique/Setoid/Properties.agda | 3 ++- src/Data/Maybe/Relation/Binary/Connected.agda | 3 ++- src/Data/Maybe/Relation/Binary/Pointwise.agda | 5 ++++- .../Product/Function/Dependent/Propositional.agda | 1 - src/Data/Product/Function/Dependent/Setoid.agda | 4 ++-- .../Product/Function/Dependent/Setoid/WithK.agda | 1 - .../Product/Function/NonDependent/Propositional.agda | 1 - .../Product/Relation/Binary/Pointwise/Dependent.agda | 12 +++++++----- src/Data/Unit/Properties.agda | 6 +++++- src/Data/Vec/Functional/Properties.agda | 6 +++--- src/Data/Vec/Properties.agda | 2 +- src/Data/Vec/Relation/Binary/Lex/Core.agda | 5 ++++- .../Vec/Relation/Binary/Pointwise/Extensional.agda | 5 ++++- src/Function/Bijection.agda | 2 +- src/Function/Bundles.agda | 3 ++- src/Function/Consequences.agda | 7 ++++--- src/Function/Construct/Composition.agda | 4 +++- src/Function/Construct/Identity.agda | 5 ++++- src/Function/Endomorphism/Setoid.agda | 3 ++- src/Function/Equality.agda | 2 +- src/Function/Equivalence.agda | 3 ++- src/Function/Injection.agda | 2 +- src/Function/Inverse.agda | 3 ++- src/Function/LeftInverse.agda | 2 +- src/Function/Metric/Nat/Structures.agda | 2 +- src/Function/Metric/Rational/Structures.agda | 2 +- src/Function/Metric/Structures.agda | 3 ++- src/Function/Properties/Bijection.agda | 4 +++- src/Function/Related.agda | 5 ++++- src/Function/Related/TypeIsomorphisms.agda | 1 - src/Function/Structures.agda | 4 +++- src/Function/Surjection.agda | 2 +- src/Induction/WellFounded.agda | 4 +++- .../Construct/Closure/Reflexive/Properties.agda | 6 +++++- .../RingSolver/Core/AlmostCommutativeRing.agda | 2 +- 110 files changed, 251 insertions(+), 130 deletions(-) diff --git a/README/Case.agda b/README/Case.agda index 9de25c6e82..30ce0221aa 100644 --- 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 index da0ae70dc4..63fea328ae 100644 --- 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 index b92a8a3c81..7273e787d1 100644 --- 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 index 2598fde953..f20cf1ad03 100644 --- 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 index 984cdd57f2..e4d51ff9ed 100644 --- 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 index 91d3f1d546..2433c87b9d 100644 --- 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 index 3ebd9b924f..6b4d4d13b7 100644 --- 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 index 212a52602f..3e4c8f7db8 100644 --- 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 index d6c7de61ba..8e4b032950 100644 --- 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 index 41f895afe6..6d2482a4a9 100644 --- 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 index a0b7a945f2..04866f0ad0 100644 --- 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 index 563e1662f1..744d32e1fe 100644 --- 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 index e278d0ffb4..28fd07d5b3 100644 --- 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 index bcedcf2074..01cef531c6 100644 --- 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 index 445e685da0..4d00c28524 100644 --- 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 index 058bd694cf..b574147807 100644 --- 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 index 19468c0851..ac4328ded3 100644 --- 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 index c2c8301409..fe3ceec5be 100644 --- 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 index cf90b022b9..85f22c39be 100644 --- 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 index b5908f57b1..b83dcdea10 100644 --- 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 index e6b33ed065..f36e5bccd0 100644 --- 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 index cb02f94469..19c1abdb46 100644 --- 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 index a6aa511af2..b85589b6fb 100644 --- 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 index 3c04e82cd0..e8aa153507 100644 --- 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 index 92b90a477c..d1a7a878ea 100644 --- 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 index 59a6f22e23..1bba00bab2 100644 --- 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 index 6c06319032..67b37378bc 100644 --- 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 index ed5bfd00dc..57037296f6 100644 --- 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 index f2c8c1f20f..588f6ef375 100644 --- 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 index 1a9e346585..7abdb583ca 100644 --- 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 index 1d50298ca5..5da80a99f1 100644 --- 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 index 23a11524cb..5642bde51c 100644 --- 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 index 836c794e10..d661dde6b1 100644 --- 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 index 5bc696da38..50c191903b 100644 --- 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 index 2bcfe92901..4c33c7b337 100644 --- 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 index 86a7d1ca04..93bcc1a7fa 100644 --- 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 index 3f610599a5..acc7153f52 100644 --- 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 index 3ef672abc7..fdfbfc00b1 100644 --- 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 index 64a0c37d9c..304e20db4b 100644 --- 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 index 8ea859f4a7..874a338a85 100644 --- 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 index d8e76d90be..f4dab55a6f 100644 --- 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 index 8993fd5aa8..2658fd0311 100644 --- 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 diff --git a/src/Codata/Musical/Stream.agda b/src/Codata/Musical/Stream.agda index a51f8f41b5..d0d655af65 100644 --- a/src/Codata/Musical/Stream.agda +++ b/src/Codata/Musical/Stream.agda @@ -13,7 +13,9 @@ open import Codata.Musical.Notation open import Codata.Musical.Colist using (Colist; []; _∷_) open import Data.Vec.Base using (Vec; []; _∷_) open import Data.Nat.Base using (ℕ; zero; suc) -open import Relation.Binary +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive) +open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) private diff --git a/src/Codata/Sized/Colist/Bisimilarity.agda b/src/Codata/Sized/Colist/Bisimilarity.agda index d66ade8b89..4ea3a18047 100644 --- a/src/Codata/Sized/Colist/Bisimilarity.agda +++ b/src/Codata/Sized/Colist/Bisimilarity.agda @@ -15,7 +15,11 @@ open import Codata.Sized.Colist open import Data.List.Base using (List; []; _∷_) open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_) open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_) -open import Relation.Binary +open import Relation.Binary.Core using (REL; Rel) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive; Sym; Trans) open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_) import Relation.Binary.PropositionalEquality.Properties as Eq diff --git a/src/Codata/Sized/Conat/Bisimilarity.agda b/src/Codata/Sized/Conat/Bisimilarity.agda index ae3e306aca..1b5aaea922 100644 --- a/src/Codata/Sized/Conat/Bisimilarity.agda +++ b/src/Codata/Sized/Conat/Bisimilarity.agda @@ -12,7 +12,8 @@ open import Level using (0ℓ) open import Size open import Codata.Sized.Thunk open import Codata.Sized.Conat -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Structures using (IsEquivalence) infix 1 _⊢_≈_ data _⊢_≈_ i : (m n : Conat ∞) → Set where diff --git a/src/Codata/Sized/Covec/Bisimilarity.agda b/src/Codata/Sized/Covec/Bisimilarity.agda index 7610c41946..685b7f180f 100644 --- a/src/Codata/Sized/Covec/Bisimilarity.agda +++ b/src/Codata/Sized/Covec/Bisimilarity.agda @@ -13,7 +13,8 @@ open import Size open import Codata.Sized.Thunk open import Codata.Sized.Conat hiding (_⊔_) open import Codata.Sized.Covec -open import Relation.Binary +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive; Sym; Trans) open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_) data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) (i : Size) : diff --git a/src/Codata/Sized/Cowriter/Bisimilarity.agda b/src/Codata/Sized/Cowriter/Bisimilarity.agda index 84ab0375c4..d9ce3e2d6f 100644 --- a/src/Codata/Sized/Cowriter/Bisimilarity.agda +++ b/src/Codata/Sized/Cowriter/Bisimilarity.agda @@ -12,7 +12,11 @@ open import Level using (Level; _⊔_) open import Size open import Codata.Sized.Thunk open import Codata.Sized.Cowriter -open import Relation.Binary +open import Relation.Binary.Core using (REL; Rel) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive; Sym; Trans) open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_) import Relation.Binary.PropositionalEquality.Properties as Eq diff --git a/src/Codata/Sized/Delay/Bisimilarity.agda b/src/Codata/Sized/Delay/Bisimilarity.agda index 4d9f702acc..f4845669ba 100644 --- a/src/Codata/Sized/Delay/Bisimilarity.agda +++ b/src/Codata/Sized/Delay/Bisimilarity.agda @@ -12,7 +12,8 @@ open import Size open import Codata.Sized.Thunk open import Codata.Sized.Delay open import Level -open import Relation.Binary +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive; Sym; Trans) open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_) data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) i : diff --git a/src/Codata/Sized/M/Bisimilarity.agda b/src/Codata/Sized/M/Bisimilarity.agda index 8205ae92e3..9c641ec834 100644 --- a/src/Codata/Sized/M/Bisimilarity.agda +++ b/src/Codata/Sized/M/Bisimilarity.agda @@ -16,7 +16,11 @@ open import Data.Container.Core open import Data.Container.Relation.Binary.Pointwise using (Pointwise; _,_) open import Data.Product.Base using (_,_) open import Function.Base using (_∋_) -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive) import Relation.Binary.PropositionalEquality.Core as P data Bisim {s p} (C : Container s p) (i : Size) : Rel (M C ∞) (s ⊔ p) where diff --git a/src/Codata/Sized/Stream/Bisimilarity.agda b/src/Codata/Sized/Stream/Bisimilarity.agda index c036d030b7..f08d0daeb8 100644 --- a/src/Codata/Sized/Stream/Bisimilarity.agda +++ b/src/Codata/Sized/Stream/Bisimilarity.agda @@ -14,7 +14,11 @@ open import Codata.Sized.Stream open import Level open import Data.List.NonEmpty as List⁺ using (_∷_) open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; REL) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive; Sym; Trans) +open import Relation.Binary.Structures using (IsEquivalence) open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_) import Relation.Binary.PropositionalEquality.Properties as Eq diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda index 713ad3da34..3c073cd23a 100644 --- a/src/Data/Bool/Properties.agda +++ b/src/Data/Bool/Properties.agda @@ -21,7 +21,13 @@ open import Function.Equivalence using (_⇔_; equivalence; module Equivalence) open import Induction.WellFounded using (WellFounded; Acc; acc) open import Level using (Level; 0ℓ) -open import Relation.Binary hiding (_⇔_) +open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Structures + using (IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder) +open import Relation.Binary.Bundles + using (Setoid; DecSetoid; Poset; Preorder; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder) +open import Relation.Binary.Definitions + using (Decidable; Reflexive; Transitive; Antisymmetric; Minimum; Maximum; Total; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri<; tri>; _Respects₂_) open import Relation.Binary.PropositionalEquality.Core open import Relation.Binary.PropositionalEquality.Properties open import Relation.Nullary.Reflects using (ofʸ; ofⁿ) diff --git a/src/Data/Container/Indexed.agda b/src/Data/Container/Indexed.agda index 26aeaa25b0..fa2e7fc33a 100644 --- a/src/Data/Container/Indexed.agda +++ b/src/Data/Container/Indexed.agda @@ -18,7 +18,7 @@ open import Function.Base renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_) open import Function.Equality using (_⟨$⟩_) open import Function.Inverse using (_↔_; module Inverse) open import Relation.Unary using (Pred; _⊆_) -import Relation.Binary as B +open import Relation.Binary.Core using (Rel; REL) open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_; refl) ------------------------------------------------------------------------ @@ -66,7 +66,7 @@ module _ {i₁ i₂ o₁ o₂} record ContainerMorphism {c₁ c₂ r₁ r₂ ℓ₁ ℓ₂} (C₁ : Container I₁ O₁ c₁ r₁) (C₂ : Container I₂ O₂ c₂ r₂) (f : I₁ → I₂) (g : O₁ → O₂) - (_∼_ : B.Rel I₂ ℓ₁) (_≈_ : B.REL (Set r₂) (Set r₁) ℓ₂) + (_∼_ : Rel I₂ ℓ₁) (_≈_ : REL (Set r₂) (Set r₁) ℓ₂) (_·_ : ∀ {A B} → A ≈ B → A → B) : Set (i₁ ⊔ i₂ ⊔ o₁ ⊔ o₂ ⊔ c₁ ⊔ c₂ ⊔ r₁ ⊔ r₂ ⊔ ℓ₁ ⊔ ℓ₂) where field @@ -107,13 +107,13 @@ module _ {i o c r} {I : Set i} {O : Set o} where infixr 8 _⇒_ _⊸_ _⇒C_ - _⇒_ : B.Rel (Container I O c r) _ + _⇒_ : Rel (Container I O c r) _ C₁ ⇒ C₂ = C₁ ⇒[ ⟨id⟩ / ⟨id⟩ ] C₂ - _⊸_ : B.Rel (Container I O c r) _ + _⊸_ : Rel (Container I O c r) _ C₁ ⊸ C₂ = C₁ ⊸[ ⟨id⟩ / ⟨id⟩ ] C₂ - _⇒C_ : B.Rel (Container I O c r) _ + _⇒C_ : Rel (Container I O c r) _ C₁ ⇒C C₂ = C₁ ⇒C[ ⟨id⟩ / ⟨id⟩ ] C₂ ------------------------------------------------------------------------ diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 2bacfe58ca..e8a1cef5dc 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -35,7 +35,12 @@ open import Function.Definitions using (Injective; Surjective) open import Function.Consequences.Propositional using (contraInjective) open import Function.Construct.Composition as Comp hiding (injective) open import Level using (Level) -open import Relation.Binary as B hiding (Decidable; _⇔_) +open import Relation.Binary.Definitions as B hiding (Decidable) +open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_) +open import Relation.Binary.Bundles + using (Preorder; Setoid; DecSetoid; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder) +open import Relation.Binary.Structures + using (IsDecEquivalence; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder) open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_; module ≡-Reasoning) open import Relation.Nullary diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda index 1cc8bd19f9..2f7246da6a 100644 --- a/src/Data/Fin/Subset/Properties.agda +++ b/src/Data/Fin/Subset/Properties.agda @@ -30,7 +30,12 @@ open import Data.Vec.Properties open import Function.Base using (_∘_; const; id; case_of_) open import Function.Bundles using (_⇔_; mk⇔) open import Level using (Level) -open import Relation.Binary as B hiding (Decidable; _⇔_) +open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Structures + using (IsPreorder; IsPartialOrder; IsStrictPartialOrder; IsDecStrictPartialOrder) +open import Relation.Binary.Bundles + using (Preorder; Poset; StrictPartialOrder; DecStrictPartialOrder) +open import Relation.Binary.Definitions as B hiding (Decidable) open import Relation.Binary.PropositionalEquality open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_) open import Relation.Nullary.Negation using (contradiction) diff --git a/src/Data/List/Fresh.agda b/src/Data/List/Fresh.agda index b5a5718765..3375b0d54a 100644 --- a/src/Data/List/Fresh.agda +++ b/src/Data/List/Fresh.agda @@ -22,9 +22,10 @@ open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_) open import Data.Maybe.Base as Maybe using (Maybe; just; nothing) open import Data.Nat.Base using (ℕ; zero; suc) open import Function.Base using (_∘′_; flip; id; _on_) -open import Relation.Nullary using (does) -open import Relation.Unary as U using (Pred) -open import Relation.Binary as B using (Rel) +open import Relation.Nullary using (does) +open import Relation.Unary as U using (Pred) +open import Relation.Binary.Core using (Rel) +import Relation.Binary.Definitions as B open import Relation.Nary private diff --git a/src/Data/List/Fresh/Membership/Setoid/Properties.agda b/src/Data/List/Fresh/Membership/Setoid/Properties.agda index d2f2634bf8..ce3f7df88b 100644 --- a/src/Data/List/Fresh/Membership/Setoid/Properties.agda +++ b/src/Data/List/Fresh/Membership/Setoid/Properties.agda @@ -21,7 +21,7 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; fromInj₂) open import Function.Base using (id; _∘′_; _$_) open import Relation.Nullary open import Relation.Unary as U using (Pred) -import Relation.Binary as B +import Relation.Binary.Definitions as B import Relation.Binary.PropositionalEquality.Core as P open import Relation.Nary diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda index 5488f9a037..4072da5ed8 100644 --- a/src/Data/List/Membership/Setoid/Properties.agda +++ b/src/Data/List/Membership/Setoid/Properties.agda @@ -27,7 +27,9 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) open import Function.Base using (_$_; flip; _∘_; _∘′_; id) open import Function.Inverse using (_↔_) open import Level using (Level) -open import Relation.Binary as B hiding (Decidable) +open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_; _Preserves_⟶_) +open import Relation.Binary.Definitions as B hiding (Decidable) +open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) open import Relation.Unary as U using (Decidable; Pred) open import Relation.Nullary using (¬_; does; _because_; yes; no) diff --git a/src/Data/List/Relation/Binary/Lex.agda b/src/Data/List/Relation/Binary/Lex.agda index c1a07e8b53..6c8fb4b323 100644 --- a/src/Data/List/Relation/Binary/Lex.agda +++ b/src/Data/List/Relation/Binary/Lex.agda @@ -19,7 +19,10 @@ open import Level using (_⊔_) open import Relation.Nullary.Negation using (¬_) open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_; _⊎-dec_) -open import Relation.Binary hiding (_⇔_) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Binary.Definitions + using (Symmetric; Transitive; Irreflexive; Asymmetric; Antisymmetric; Decidable; _Respects₂_; _Respects_) open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_; head; tail) diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda index 46d5d7d2cc..b11e011d76 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda @@ -33,7 +33,12 @@ open import Relation.Nullary.Reflects using (invert) open import Relation.Nullary using (Dec; does; _because_; yes; no; ¬_) open import Relation.Nullary.Decidable as Dec using (¬?) open import Relation.Unary as U using (Pred) -open import Relation.Binary hiding (_⇔_) +open import Relation.Binary.Core using (Rel; REL; _⇒_) +open import Relation.Binary.Bundles using (Preorder; Poset; DecPoset) +open import Relation.Binary.Definitions + using (Reflexive; Trans; Antisym; Decidable; Irrelevant; Irreflexive) +open import Relation.Binary.Structures + using (IsPreorder; IsPartialOrder; IsDecPartialOrder) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) ------------------------------------------------------------------------ diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda index 5229813a50..551b721d8d 100644 --- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda @@ -26,7 +26,11 @@ open import Level using (Level) open import Relation.Nullary using (¬_; does; yes; no) open import Relation.Nullary.Negation using (contradiction) open import Relation.Unary using (Pred; Decidable) renaming (_⊆_ to _⋐_) -open import Relation.Binary hiding (Decidable) +open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Definitions + using (Reflexive; Transitive; _Respectsʳ_; _Respectsˡ_; _Respects_) +open import Relation.Binary.Bundles using (Setoid; Preorder) +open import Relation.Binary.Structures using (IsPreorder) import Relation.Binary.Reasoning.Preorder as PreorderReasoning open Setoid using (Carrier) diff --git a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda index 05b7725d31..3ea10495e6 100644 --- a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda @@ -24,8 +24,9 @@ open import Relation.Nullary using (Dec; does; ¬_) import Relation.Nullary.Decidable as Dec open import Relation.Unary as U using (Pred) open import Relation.Nullary.Negation using (contradiction) -open import Relation.Binary as B - using (REL; Rel; Trans; Antisym; Irrelevant; _⇒_) +open import Relation.Binary.Core using (REL; Rel; _⇒_) +open import Relation.Binary.Definitions as B + using (Trans; Antisym; Irrelevant) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; _≢_; refl; sym; subst; subst₂) diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda index 00d8e6f7b7..97da349699 100644 --- a/src/Data/List/Relation/Unary/All.agda +++ b/src/Data/List/Relation/Unary/All.agda @@ -23,7 +23,8 @@ open import Level using (Level; _⊔_) open import Relation.Nullary hiding (Irrelevant) import Relation.Nullary.Decidable as Dec open import Relation.Unary hiding (_∈_) -open import Relation.Binary using (Setoid; _Respects_) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Definitions using (_Respects_) open import Relation.Binary.PropositionalEquality.Core as P import Relation.Binary.PropositionalEquality.Properties as P diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda index af41a14041..1a75b5eb35 100644 --- a/src/Data/List/Relation/Unary/All/Properties.agda +++ b/src/Data/List/Relation/Unary/All/Properties.agda @@ -38,7 +38,9 @@ open import Function.Equality using (_⟨$⟩_) open import Function.Equivalence using (_⇔_; equivalence; Equivalence) open import Function.Surjection using (_↠_; surjection) open import Level using (Level) -open import Relation.Binary as B using (REL; Setoid; _Respects_) +open import Relation.Binary.Core using (REL) +open import Relation.Binary.Bundles using (Setoid) +import Relation.Binary.Definitions as B open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂; _≗_) open import Relation.Nullary @@ -731,7 +733,7 @@ module _ (S : Setoid c ℓ) where open Setoid S open ListEq S - respects : P Respects _≈_ → (All P) Respects _≋_ + respects : P B.Respects _≈_ → (All P) B.Respects _≋_ respects p≈ [] [] = [] respects p≈ (x≈y ∷ xs≈ys) (px ∷ pxs) = p≈ x≈y px ∷ respects p≈ xs≈ys pxs diff --git a/src/Data/List/Relation/Unary/AllPairs.agda b/src/Data/List/Relation/Unary/AllPairs.agda index 49bfac6ae0..bed4a5972d 100644 --- a/src/Data/List/Relation/Unary/AllPairs.agda +++ b/src/Data/List/Relation/Unary/AllPairs.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary using (Rel) +open import Relation.Binary.Core using (Rel; _⇒_) module Data.List.Relation.Unary.AllPairs {a ℓ} {A : Set a} {R : Rel A ℓ} where @@ -16,7 +16,7 @@ open import Data.List.Relation.Unary.All as All using (All; []; _∷_) open import Data.Product.Base as Prod using (_,_; _×_; uncurry; <_,_>) open import Function.Base using (id; _∘_) open import Level using (_⊔_) -open import Relation.Binary as B using (Rel; _⇒_) +open import Relation.Binary.Definitions as B open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_) open import Relation.Binary.PropositionalEquality open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_) diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda index 8f3bcd640c..b50b962e26 100644 --- a/src/Data/List/Relation/Unary/Any/Properties.agda +++ b/src/Data/List/Relation/Unary/Any/Properties.agda @@ -40,7 +40,8 @@ open import Function.Equivalence using (_⇔_; equivalence; Equivalence) open import Function.Inverse as Inv using (_↔_; inverse; Inverse) open import Function.Related as Related using (Kind; Related; SK-sym) open import Level using (Level) -open import Relation.Binary as B hiding (_⇔_) +open import Relation.Binary.Core using (Rel; REL) +open import Relation.Binary.Definitions as B open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl) open import Relation.Unary as U diff --git a/src/Data/List/Relation/Unary/Grouped.agda b/src/Data/List/Relation/Unary/Grouped.agda index 87b11cabc3..f10bc1fd32 100644 --- a/src/Data/List/Relation/Unary/Grouped.agda +++ b/src/Data/List/Relation/Unary/Grouped.agda @@ -12,7 +12,8 @@ open import Data.List.Base using (List; []; _∷_; map) open import Data.List.Relation.Unary.All as All using (All; []; _∷_; all?) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Data.Product.Base using (_×_; _,_) -open import Relation.Binary as B using (REL; Rel) +open import Relation.Binary.Core using (REL; Rel) +open import Relation.Binary.Definitions as B open import Relation.Unary as U using (Pred) open import Relation.Nullary.Negation using (¬_) open import Relation.Nullary.Decidable as Dec using (yes; ¬?; _⊎-dec_; _×-dec_) diff --git a/src/Data/List/Relation/Unary/Linked/Properties.agda b/src/Data/List/Relation/Unary/Linked/Properties.agda index d969986a55..10ece2fdb3 100644 --- a/src/Data/List/Relation/Unary/Linked/Properties.agda +++ b/src/Data/List/Relation/Unary/Linked/Properties.agda @@ -22,7 +22,9 @@ open import Data.Maybe.Relation.Binary.Connected using (Connected; just; nothing; just-nothing; nothing-just) open import Level using (Level) open import Function.Base using (_∘_; flip; _on_) -open import Relation.Binary using (Rel; Transitive; DecSetoid) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (DecSetoid) +open import Relation.Binary.Definitions using (Transitive) open import Relation.Binary.PropositionalEquality.Core using (_≢_) open import Relation.Unary using (Pred; Decidable) open import Relation.Nullary.Decidable using (yes; no; does) diff --git a/src/Data/List/Relation/Unary/Sorted/TotalOrder.agda b/src/Data/List/Relation/Unary/Sorted/TotalOrder.agda index 0b6060bae9..cfdf8bf275 100644 --- a/src/Data/List/Relation/Unary/Sorted/TotalOrder.agda +++ b/src/Data/List/Relation/Unary/Sorted/TotalOrder.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary using (TotalOrder) +open import Relation.Binary.Bundles using (TotalOrder) module Data.List.Relation.Unary.Sorted.TotalOrder {a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂) where @@ -17,7 +17,7 @@ open import Data.List.Base using (List; []; _∷_) open import Data.List.Relation.Unary.Linked as Linked using (Linked) open import Level using (_⊔_) open import Relation.Unary as U using (Pred; _⊆_) -open import Relation.Binary as B +open import Relation.Binary.Definitions as B ------------------------------------------------------------------------ -- Definition diff --git a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda index 89582d2f88..c8c4210ed6 100644 --- a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda +++ b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda @@ -23,7 +23,8 @@ open import Data.Maybe.Relation.Binary.Connected using (Connected; just) open import Data.Nat.Base using (ℕ; zero; suc; _<_) open import Level using (Level) -open import Relation.Binary hiding (Decidable) +open import Relation.Binary.Core using (_Preserves_⟶_) +open import Relation.Binary.Bundles using (TotalOrder; DecTotalOrder; Preorder) import Relation.Binary.Properties.TotalOrder as TotalOrderProperties open import Relation.Unary using (Pred; Decidable) open import Relation.Nullary.Decidable using (yes; no) diff --git a/src/Data/List/Relation/Unary/Unique/DecPropositional.agda b/src/Data/List/Relation/Unary/Unique/DecPropositional.agda index 3f552b6fa9..f2e3692103 100644 --- a/src/Data/List/Relation/Unary/Unique/DecPropositional.agda +++ b/src/Data/List/Relation/Unary/Unique/DecPropositional.agda @@ -6,7 +6,8 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary using (DecSetoid; DecidableEquality) +open import Relation.Binary.Bundles using (DecSetoid) +open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Properties using (decSetoid) module Data.List.Relation.Unary.Unique.DecPropositional diff --git a/src/Data/List/Relation/Unary/Unique/DecPropositional/Properties.agda b/src/Data/List/Relation/Unary/Unique/DecPropositional/Properties.agda index 6d28ed56d6..4184647ae2 100644 --- a/src/Data/List/Relation/Unary/Unique/DecPropositional/Properties.agda +++ b/src/Data/List/Relation/Unary/Unique/DecPropositional/Properties.agda @@ -10,7 +10,7 @@ open import Data.List import Data.List.Relation.Unary.Unique.DecSetoid.Properties as Setoid open import Data.List.Relation.Unary.All.Properties using (all-filter) open import Level -open import Relation.Binary using (DecidableEquality) +open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Properties using (decSetoid) module Data.List.Relation.Unary.Unique.DecPropositional.Properties diff --git a/src/Data/List/Relation/Unary/Unique/DecSetoid.agda b/src/Data/List/Relation/Unary/Unique/DecSetoid.agda index 4b7133c8f1..bddc7b2727 100644 --- a/src/Data/List/Relation/Unary/Unique/DecSetoid.agda +++ b/src/Data/List/Relation/Unary/Unique/DecSetoid.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary using (DecSetoid) +open import Relation.Binary.Bundles using (DecSetoid) import Data.List.Relation.Unary.AllPairs as AllPairs open import Relation.Unary using (Decidable) open import Relation.Nullary.Decidable using (¬?) diff --git a/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda b/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda index 2eda2ded13..9e97527ff8 100644 --- a/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda +++ b/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda @@ -11,7 +11,7 @@ import Data.List.Relation.Unary.Unique.DecSetoid as Unique open import Data.List.Relation.Unary.All.Properties using (all-filter) open import Data.List.Relation.Unary.Unique.Setoid.Properties open import Level -open import Relation.Binary using (DecSetoid) +open import Relation.Binary.Bundles using (DecSetoid) open import Relation.Nullary.Decidable using (¬?) module Data.List.Relation.Unary.Unique.DecSetoid.Properties where diff --git a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda index 7740dc83e3..e12b5cf47b 100644 --- a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda +++ b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda @@ -21,7 +21,8 @@ open import Data.Product.Base using (_×_; _,_) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (≡⇒≡×≡) open import Function.Base using (id; _∘_) open import Level using (Level) -open import Relation.Binary using (Rel; Setoid) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.PropositionalEquality using (refl; _≡_; _≢_; sym; setoid) open import Relation.Unary using (Pred; Decidable) diff --git a/src/Data/List/Relation/Unary/Unique/Setoid.agda b/src/Data/List/Relation/Unary/Unique/Setoid.agda index aad10762ac..041b68ec9b 100644 --- a/src/Data/List/Relation/Unary/Unique/Setoid.agda +++ b/src/Data/List/Relation/Unary/Unique/Setoid.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) open import Relation.Nullary.Negation using (¬_) module Data.List.Relation.Unary.Unique.Setoid {a ℓ} (S : Setoid a ℓ) where diff --git a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda index 6ba7f803a1..ffb587018a 100644 --- a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda +++ b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda @@ -23,7 +23,8 @@ open import Data.Fin.Base using (Fin) open import Data.Nat.Base using (_<_) open import Function.Base using (_∘_; id) open import Level using (Level) -open import Relation.Binary using (Rel; Setoid) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.PropositionalEquality.Core using (_≡_) open import Relation.Unary using (Pred; Decidable) open import Relation.Nullary.Negation using (¬_) diff --git a/src/Data/Maybe/Relation/Binary/Connected.agda b/src/Data/Maybe/Relation/Binary/Connected.agda index 5c509e50fd..8c174c9ea1 100644 --- a/src/Data/Maybe/Relation/Binary/Connected.agda +++ b/src/Data/Maybe/Relation/Binary/Connected.agda @@ -11,7 +11,8 @@ module Data.Maybe.Relation.Binary.Connected where open import Level open import Data.Maybe.Base using (Maybe; just; nothing) open import Function.Bundles using (_⇔_; mk⇔) -open import Relation.Binary hiding (_⇔_) +open import Relation.Binary.Core using (REL; _⇒_) +open import Relation.Binary.Definitions using (Reflexive; Sym; Decidable) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) open import Relation.Nullary import Relation.Nullary.Decidable as Dec diff --git a/src/Data/Maybe/Relation/Binary/Pointwise.agda b/src/Data/Maybe/Relation/Binary/Pointwise.agda index a9946a6ef3..48fa144a2e 100644 --- a/src/Data/Maybe/Relation/Binary/Pointwise.agda +++ b/src/Data/Maybe/Relation/Binary/Pointwise.agda @@ -12,7 +12,10 @@ open import Level open import Data.Product.Base using (∃; _×_; -,_; _,_) open import Data.Maybe.Base using (Maybe; just; nothing) open import Function.Bundles using (_⇔_; mk⇔) -open import Relation.Binary hiding (_⇔_) +open import Relation.Binary.Core using (REL; Rel; _⇒_) +open import Relation.Binary.Bundles using (Setoid; DecSetoid) +open import Relation.Binary.Definitions using (Reflexive; Sym; Trans; Decidable) +open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) open import Relation.Nullary import Relation.Nullary.Decidable as Dec diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda index abae430992..b7333283ff 100644 --- a/src/Data/Product/Function/Dependent/Propositional.agda +++ b/src/Data/Product/Function/Dependent/Propositional.agda @@ -12,7 +12,6 @@ module Data.Product.Function.Dependent.Propositional where open import Data.Product.Base using (Σ; map; _,_) open import Data.Product.Function.NonDependent.Setoid open import Data.Product.Relation.Binary.Pointwise.NonDependent -open import Relation.Binary hiding (_⇔_) open import Function.Base open import Function.Equality using (_⟶_; _⟨$⟩_) open import Function.Equivalence as Equiv using (_⇔_; module Equivalence) diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda index 22f3f7937a..71cd995b18 100644 --- a/src/Data/Product/Function/Dependent/Setoid.agda +++ b/src/Data/Product/Function/Dependent/Setoid.agda @@ -23,7 +23,8 @@ open import Function.LeftInverse as LeftInv using (LeftInverse; _↞_; _LeftInverseOf_; _RightInverseOf_; module LeftInverse) open import Function.Surjection as Surj using (Surjection; _↠_; module Surjection) -open import Relation.Binary as B hiding (_⇔_) +open import Relation.Binary.Core using (_=[_]⇒_) +open import Relation.Binary.Bundles as B open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid) open import Relation.Binary.Indexed.Heterogeneous.Construct.At @@ -57,7 +58,6 @@ private using () renaming (_≈_ to _≈₁_) open B.Setoid (setoid (P.setoid A₂) B₂) using () renaming (_≈_ to _≈₂_) - open B using (_=[_]⇒_) fg = map f (_⟨$⟩_ g) diff --git a/src/Data/Product/Function/Dependent/Setoid/WithK.agda b/src/Data/Product/Function/Dependent/Setoid/WithK.agda index 7362b3ade0..3336ecb5e5 100644 --- a/src/Data/Product/Function/Dependent/Setoid/WithK.agda +++ b/src/Data/Product/Function/Dependent/Setoid/WithK.agda @@ -25,7 +25,6 @@ open import Function.LeftInverse as LeftInv using (LeftInverse; _↞_; _LeftInverseOf_; _RightInverseOf_; module LeftInverse) open import Function.Surjection as Surj using (Surjection; _↠_; module Surjection) -open import Relation.Binary as B open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid) open import Relation.Binary.Indexed.Heterogeneous.Construct.At diff --git a/src/Data/Product/Function/NonDependent/Propositional.agda b/src/Data/Product/Function/NonDependent/Propositional.agda index b4c9501304..7dfb28207d 100644 --- a/src/Data/Product/Function/NonDependent/Propositional.agda +++ b/src/Data/Product/Function/NonDependent/Propositional.agda @@ -12,7 +12,6 @@ module Data.Product.Function.NonDependent.Propositional where open import Data.Product.Base using (_×_; map) open import Data.Product.Function.NonDependent.Setoid open import Data.Product.Relation.Binary.Pointwise.NonDependent -open import Relation.Binary hiding (_⇔_) open import Function.Equality using (_⟶_) open import Function.Equivalence as Eq using (_⇔_; module Equivalence) open import Function.Injection as Inj using (_↣_; module Injection) diff --git a/src/Data/Product/Relation/Binary/Pointwise/Dependent.agda b/src/Data/Product/Relation/Binary/Pointwise/Dependent.agda index 8a7dc43e83..fd22ff6cce 100644 --- a/src/Data/Product/Relation/Binary/Pointwise/Dependent.agda +++ b/src/Data/Product/Relation/Binary/Pointwise/Dependent.agda @@ -11,8 +11,10 @@ module Data.Product.Relation.Binary.Pointwise.Dependent where open import Data.Product.Base as Prod open import Level open import Function.Base -open import Relation.Binary as B - using (_⇒_; Setoid; IsEquivalence) +open import Relation.Binary.Core using (Rel; REL; _⇒_) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Binary.Definitions as B open import Relation.Binary.Indexed.Heterogeneous as I using (IREL; IRel; IndexedSetoid; IsIndexedEquivalence) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) @@ -25,7 +27,7 @@ infixr 4 _,_ record POINTWISE {a₁ a₂ b₁ b₂ ℓ₁ ℓ₂} {A₁ : Set a₁} (B₁ : A₁ → Set b₁) {A₂ : Set a₂} (B₂ : A₂ → Set b₂) - (_R₁_ : B.REL A₁ A₂ ℓ₁) (_R₂_ : IREL B₁ B₂ ℓ₂) + (_R₁_ : REL A₁ A₂ ℓ₁) (_R₂_ : IREL B₁ B₂ ℓ₂) (xy₁ : Σ A₁ B₁) (xy₂ : Σ A₂ B₂) : Set (a₁ ⊔ a₂ ⊔ b₁ ⊔ b₂ ⊔ ℓ₁ ⊔ ℓ₂) where constructor _,_ @@ -36,14 +38,14 @@ record POINTWISE {a₁ a₂ b₁ b₂ ℓ₁ ℓ₂} open POINTWISE public Pointwise : ∀ {a b ℓ₁ ℓ₂} {A : Set a} (B : A → Set b) - (_R₁_ : B.Rel A ℓ₁) (_R₂_ : IRel B ℓ₂) → B.Rel (Σ A B) _ + (_R₁_ : Rel A ℓ₁) (_R₂_ : IRel B ℓ₂) → Rel (Σ A B) _ Pointwise B = POINTWISE B B ------------------------------------------------------------------------ -- Pointwise preserves many relational properties module _ {a b ℓ₁ ℓ₂} {A : Set a} {B : A → Set b} - {R : B.Rel A ℓ₁} {S : IRel B ℓ₂} where + {R : Rel A ℓ₁} {S : IRel B ℓ₂} where private R×S = Pointwise B R S diff --git a/src/Data/Unit/Properties.agda b/src/Data/Unit/Properties.agda index b31d8feb3d..5b4c0bee51 100644 --- a/src/Data/Unit/Properties.agda +++ b/src/Data/Unit/Properties.agda @@ -12,7 +12,11 @@ open import Data.Sum.Base open import Data.Unit.Base open import Level using (0ℓ) open import Relation.Nullary -open import Relation.Binary hiding (Irrelevant) +open import Relation.Binary.Bundles + using (Setoid; DecSetoid; Poset; DecTotalOrder) +open import Relation.Binary.Structures + using (IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder) +open import Relation.Binary.Definitions using (Decidable; Total; Antisymmetric) open import Relation.Binary.PropositionalEquality ------------------------------------------------------------------------ diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda index d0dbc16cda..f3314754e0 100644 --- a/src/Data/Vec/Functional/Properties.agda +++ b/src/Data/Vec/Functional/Properties.agda @@ -21,7 +21,7 @@ import Data.Vec.Properties as Vₚ open import Data.Vec.Functional open import Function.Base open import Level using (Level) -open import Relation.Binary as B +open import Relation.Binary.Definitions using (DecidableEquality; Decidable) open import Relation.Binary.PropositionalEquality open import Relation.Nullary.Decidable using (Dec; does; yes; no; map′; _×-dec_) @@ -46,8 +46,8 @@ module _ {n} {xs ys : Vector A (suc n)} where ∷-injective : xs ≗ ys → head xs ≡ head ys × tail xs ≗ tail ys ∷-injective eq = eq zero , eq ∘ suc -≗-dec : B.DecidableEquality A → - ∀ {n} → B.Decidable {A = Vector A n} _≗_ +≗-dec : DecidableEquality A → + ∀ {n} → Decidable {A = Vector A n} _≗_ ≗-dec _≟_ {zero} xs ys = yes λ () ≗-dec _≟_ {suc n} xs ys = map′ (Product.uncurry ∷-cong) ∷-injective diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 57ffb79317..b370b155d4 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -24,7 +24,7 @@ open import Function.Base -- open import Function.Inverse using (_↔_; inverse) open import Function.Bundles using (_↔_; mk↔′) open import Level using (Level) -open import Relation.Binary hiding (Decidable) +open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; _≗_; refl; sym; trans; cong; cong₂; subst; module ≡-Reasoning) open import Relation.Unary using (Pred; Decidable) diff --git a/src/Data/Vec/Relation/Binary/Lex/Core.agda b/src/Data/Vec/Relation/Binary/Lex/Core.agda index c091d0f98c..7b35081911 100644 --- a/src/Data/Vec/Relation/Binary/Lex/Core.agda +++ b/src/Data/Vec/Relation/Binary/Lex/Core.agda @@ -18,7 +18,10 @@ open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _ open import Function.Base using (flip) open import Function.Bundles using (_⇔_; mk⇔) open import Level using (Level; _⊔_) -open import Relation.Binary hiding (_⇔_) +open import Relation.Binary.Core using (Rel; REL) +open import Relation.Binary.Definitions + using (Transitive; Symmetric; Asymmetric; Antisymmetric; Irreflexive; Trans; _Respects₂_; _Respectsˡ_; _Respectsʳ_; Decidable; Irrelevant) +open import Relation.Binary.Structures using (IsPartialEquivalence) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl; cong) import Relation.Nullary as Nullary diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda b/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda index c7b2b3d7ea..5dcaa6b900 100644 --- a/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda +++ b/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda @@ -18,7 +18,10 @@ open import Function.Base using (_∘_) open import Function.Bundles using (module Equivalence; _⇔_; mk⇔) open import Function.Properties.Equivalence using (⇔-setoid) open import Level using (Level; _⊔_; 0ℓ) -open import Relation.Binary hiding (_⇔_) +open import Relation.Binary.Core using (Rel; REL; _⇒_; _=[_]⇒_) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence) +open import Relation.Binary.Definitions using (Reflexive; Sym; Trans; Decidable) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) open import Relation.Binary.Construct.Closure.Transitive as Plus hiding (equivalent; map) diff --git a/src/Function/Bijection.agda b/src/Function/Bijection.agda index 8c7ce78ef3..405d326b51 100644 --- a/src/Function/Bijection.agda +++ b/src/Function/Bijection.agda @@ -14,7 +14,7 @@ module Function.Bijection where open import Level -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.PropositionalEquality as P open import Function.Equality as F using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_) diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index 1b92bee909..d100fc5343 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -24,7 +24,8 @@ open import Function.Definitions import Function.Structures as FunctionStructures open import Level using (Level; _⊔_; suc) open import Data.Product.Base using (_,_; proj₁; proj₂) -open import Relation.Binary hiding (_⇔_) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Core using (_Preserves_⟶_) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) import Relation.Binary.PropositionalEquality.Properties as ≡ diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index 242aa3d289..60606cc673 100644 --- a/src/Function/Consequences.agda +++ b/src/Function/Consequences.agda @@ -12,9 +12,10 @@ module Function.Consequences where open import Data.Product.Base as Prod open import Function.Definitions -open import Level -open import Relation.Binary.Core -open import Relation.Binary.Definitions +open import Level using (Level) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive) open import Relation.Nullary.Negation.Core using (¬_; contraposition) private diff --git a/src/Function/Construct/Composition.agda b/src/Function/Construct/Composition.agda index b745daa8e6..75baef6256 100644 --- a/src/Function/Construct/Composition.agda +++ b/src/Function/Construct/Composition.agda @@ -14,7 +14,9 @@ open import Function.Bundles open import Function.Definitions open import Function.Structures open import Level using (Level) -open import Relation.Binary hiding (_⇔_; IsEquivalence) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Definitions using (Transitive) private variable diff --git a/src/Function/Construct/Identity.agda b/src/Function/Construct/Identity.agda index e4ec7e3d3e..0088445ba5 100644 --- a/src/Function/Construct/Identity.agda +++ b/src/Function/Construct/Identity.agda @@ -14,7 +14,10 @@ open import Function.Bundles import Function.Definitions as Definitions import Function.Structures as Structures open import Level using (Level) -open import Relation.Binary as B hiding (_⇔_; IsEquivalence) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Structures as B hiding (IsEquivalence) +open import Relation.Binary.Definitions using (Reflexive) open import Relation.Binary.PropositionalEquality.Core using (_≡_) open import Relation.Binary.PropositionalEquality.Properties using (setoid) diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda index 9d7974294c..d9890c3a35 100644 --- a/src/Function/Endomorphism/Setoid.agda +++ b/src/Function/Endomorphism/Setoid.agda @@ -9,7 +9,8 @@ -- Disabled to prevent warnings from deprecated names {-# OPTIONS --warn=noUserWarning #-} -open import Relation.Binary +open import Relation.Binary.Core using (_Preserves_⟶_) +open import Relation.Binary.Bundles using (Setoid) module Function.Endomorphism.Setoid {c e} (S : Setoid c e) where diff --git a/src/Function/Equality.agda b/src/Function/Equality.agda index bb32bca8cd..91eeb7ef73 100644 --- a/src/Function/Equality.agda +++ b/src/Function/Equality.agda @@ -15,7 +15,7 @@ module Function.Equality where import Function.Base as Fun open import Level using (Level; _⊔_) -open import Relation.Binary using (Setoid) +open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid; _=[_]⇒_) import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial diff --git a/src/Function/Equivalence.agda b/src/Function/Equivalence.agda index 7bbbade93c..34ab390682 100644 --- a/src/Function/Equivalence.agda +++ b/src/Function/Equivalence.agda @@ -17,7 +17,8 @@ open import Function.Base using (flip) open import Function.Equality as F using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_) open import Level -open import Relation.Binary hiding (_⇔_) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Definitions using (Reflexive; TransFlip; Sym) import Relation.Binary.PropositionalEquality as P ------------------------------------------------------------------------ diff --git a/src/Function/Injection.agda b/src/Function/Injection.agda index 4f746c2beb..9bd6277fd2 100644 --- a/src/Function/Injection.agda +++ b/src/Function/Injection.agda @@ -15,7 +15,7 @@ module Function.Injection where open import Function.Base as Fun using () renaming (_∘_ to _⟨∘⟩_) open import Level -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) open import Function.Equality as F using (_⟶_; _⟨$⟩_ ; Π) renaming (_∘_ to _⟪∘⟫_) open import Relation.Binary.PropositionalEquality as P using (_≡_) diff --git a/src/Function/Inverse.agda b/src/Function/Inverse.agda index 4d0185d4b6..87632836db 100644 --- a/src/Function/Inverse.agda +++ b/src/Function/Inverse.agda @@ -19,7 +19,8 @@ open import Function.Bijection hiding (id; _∘_; bijection) open import Function.Equality as F using (_⟶_) renaming (_∘_ to _⟪∘⟫_) open import Function.LeftInverse as Left hiding (id; _∘_) -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Definitions using (Reflexive; TransFlip; Sym) open import Relation.Binary.PropositionalEquality as P using (_≗_; _≡_) open import Relation.Unary using (Pred) diff --git a/src/Function/LeftInverse.agda b/src/Function/LeftInverse.agda index 23f9b4a900..6f2c8d0db5 100644 --- a/src/Function/LeftInverse.agda +++ b/src/Function/LeftInverse.agda @@ -15,7 +15,7 @@ module Function.LeftInverse where open import Level import Relation.Binary.Reasoning.Setoid as EqReasoning -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) open import Function.Equality as Eq using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_) open import Function.Equivalence using (Equivalence) diff --git a/src/Function/Metric/Nat/Structures.agda b/src/Function/Metric/Nat/Structures.agda index 839dc7b974..8eaa533faa 100644 --- a/src/Function/Metric/Nat/Structures.agda +++ b/src/Function/Metric/Nat/Structures.agda @@ -11,7 +11,7 @@ module Function.Metric.Nat.Structures where open import Data.Nat.Base hiding (suc) open import Function.Base using (const) open import Level using (Level; suc) -open import Relation.Binary hiding (Symmetric) +open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core using (_≡_) open import Function.Metric.Nat.Core diff --git a/src/Function/Metric/Rational/Structures.agda b/src/Function/Metric/Rational/Structures.agda index daa2b71a60..3a8acdaae6 100644 --- a/src/Function/Metric/Rational/Structures.agda +++ b/src/Function/Metric/Rational/Structures.agda @@ -9,7 +9,7 @@ open import Data.Rational.Base open import Function.Base using (const) open import Level using (Level; suc) -open import Relation.Binary hiding (Symmetric) +open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core using (_≡_) open import Function.Metric.Rational.Core diff --git a/src/Function/Metric/Structures.agda b/src/Function/Metric/Structures.agda index 1523673557..68c85e48b4 100644 --- a/src/Function/Metric/Structures.agda +++ b/src/Function/Metric/Structures.agda @@ -9,7 +9,8 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary hiding (Symmetric) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Structures using (IsPartialOrder; IsEquivalence) module Function.Metric.Structures {a i ℓ₁ ℓ₂ ℓ₃} {A : Set a} {I : Set i} diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda index 38d269195b..1028e694e8 100644 --- a/src/Function/Properties/Bijection.agda +++ b/src/Function/Properties/Bijection.agda @@ -10,7 +10,9 @@ module Function.Properties.Bijection where open import Function.Bundles open import Level using (Level) -open import Relation.Binary hiding (_⇔_) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Binary.Definitions using (Reflexive; Trans) open import Relation.Binary.PropositionalEquality as P using (setoid) open import Data.Product.Base using (_,_; proj₁; proj₂) open import Function.Base using (_∘_) diff --git a/src/Function/Related.agda b/src/Function/Related.agda index cc80adff63..aa661c9cb8 100644 --- a/src/Function/Related.agda +++ b/src/Function/Related.agda @@ -18,7 +18,10 @@ open import Function.Inverse as Inv using (Inverse; _↔_) open import Function.LeftInverse as LeftInv using (LeftInverse) open import Function.Surjection as Surj using (Surjection) open import Function.Consequences.Propositional -open import Relation.Binary +open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Bundles using (Setoid; Preorder) +open import Relation.Binary.Structures using (IsEquivalence; IsPreorder) +open import Relation.Binary.Definitions using (Reflexive; Trans; Sym) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) import Relation.Binary.PropositionalEquality.Properties as P open import Data.Product.Base using (_,_; proj₁; proj₂; <_,_>) diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda index 9922c69fcf..c2ba98dce4 100644 --- a/src/Function/Related/TypeIsomorphisms.agda +++ b/src/Function/Related/TypeIsomorphisms.agda @@ -28,7 +28,6 @@ open import Function.Equality using (_⟨$⟩_) open import Function.Equivalence as Eq using (_⇔_; Equivalence) open import Function.Inverse as Inv using (_↔_; Inverse; inverse) open import Function.Related -open import Relation.Binary hiding (_⇔_) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) open import Relation.Nullary.Reflects using (invert) open import Relation.Nullary using (Dec; ¬_; _because_; ofⁿ) diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index 5566e92c8b..a1cc0d6ceb 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -8,7 +8,9 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Structures using (IsEquivalence) module Function.Structures {a b ℓ₁ ℓ₂} {A : Set a} (_≈₁_ : Rel A ℓ₁) -- Equality over the domain diff --git a/src/Function/Surjection.agda b/src/Function/Surjection.agda index 6861979551..729b46a538 100644 --- a/src/Function/Surjection.agda +++ b/src/Function/Surjection.agda @@ -19,7 +19,7 @@ open import Function.Equality as F open import Function.Equivalence using (Equivalence) open import Function.Injection hiding (id; _∘_; injection) open import Function.LeftInverse as Left hiding (id; _∘_) -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.PropositionalEquality as P using (_≡_) ------------------------------------------------------------------------ diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda index c1e206a0af..12b1719118 100644 --- a/src/Induction/WellFounded.agda +++ b/src/Induction/WellFounded.agda @@ -12,7 +12,9 @@ open import Data.Product.Base using (Σ; _,_; proj₁) open import Function.Base using (_on_) open import Induction open import Level using (Level; _⊔_) -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Definitions + using (Symmetric; _Respectsʳ_; _Respects_) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) open import Relation.Unary diff --git a/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda b/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda index d9bf470f5c..29defea059 100644 --- a/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda +++ b/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda @@ -13,7 +13,11 @@ open import Data.Sum.Base as Sum open import Function.Bundles using (_⇔_; mk⇔) open import Function.Base using (id) open import Level -open import Relation.Binary hiding (_⇔_) +open import Relation.Binary.Core using (Rel; REL; _=[_]⇒_) +open import Relation.Binary.Structures + using (IsPreorder; IsStrictPartialOrder; IsPartialOrder; IsDecStrictPartialOrder; IsDecPartialOrder; IsStrictTotalOrder; IsTotalOrder; IsDecTotalOrder) +open import Relation.Binary.Definitions + using (Symmetric; Transitive; Reflexive; Asymmetric; Antisymmetric; Trichotomous; Total; Decidable; tri<; tri≈; tri>; _Respectsˡ_; _Respectsʳ_; _Respects_; _Respects₂_) open import Relation.Binary.Construct.Closure.Reflexive open import Relation.Binary.PropositionalEquality.Core as PropEq using (_≡_; refl) import Relation.Binary.PropositionalEquality.Properties as PropEq diff --git a/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda b/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda index 2817b21cf4..5ed5b8f4ff 100644 --- a/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda +++ b/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda @@ -9,7 +9,7 @@ module Tactic.RingSolver.Core.AlmostCommutativeRing where open import Level -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _Preserves_⟶_) open import Algebra.Core using (Op₁; Op₂) open import Algebra.Structures using (IsCommutativeSemiring) open import Algebra.Definitions