diff --git a/src/Codata/Sized/Conat/Properties.agda b/src/Codata/Sized/Conat/Properties.agda index 43d5662a9a..54e211dc1f 100644 --- a/src/Codata/Sized/Conat/Properties.agda +++ b/src/Codata/Sized/Conat/Properties.agda @@ -16,7 +16,7 @@ open import Codata.Sized.Conat.Bisimilarity open import Function.Base using (_∋_) open import Relation.Nullary open import Relation.Nullary.Decidable using (map′) -open import Relation.Binary +open import Relation.Binary.Definitions using (Decidable) private variable diff --git a/src/Data/AVL/Indexed/WithK.agda b/src/Data/AVL/Indexed/WithK.agda index 15da148fa2..609fb7b45d 100644 --- a/src/Data/AVL/Indexed/WithK.agda +++ b/src/Data/AVL/Indexed/WithK.agda @@ -6,7 +6,8 @@ {-# OPTIONS --with-K --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Structures using (IsStrictTotalOrder) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; subst) module Data.AVL.Indexed.WithK diff --git a/src/Data/AVL/IndexedMap.agda b/src/Data/AVL/IndexedMap.agda index 84dbcceba4..fad21c14c2 100644 --- a/src/Data/AVL/IndexedMap.agda +++ b/src/Data/AVL/IndexedMap.agda @@ -7,7 +7,8 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Data.Product.Base using (∃) -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Structures using (IsStrictTotalOrder) open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst) import Data.Tree.AVL.Value diff --git a/src/Data/AVL/Key.agda b/src/Data/AVL/Key.agda index 96023d342d..f1ca15bacd 100644 --- a/src/Data/AVL/Key.agda +++ b/src/Data/AVL/Key.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (StrictTotalOrder) module Data.AVL.Key {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) diff --git a/src/Data/Bool.agda b/src/Data/Bool.agda index 5fdbcc45e0..1270125254 100644 --- a/src/Data/Bool.agda +++ b/src/Data/Bool.agda @@ -9,7 +9,6 @@ module Data.Bool where open import Relation.Nullary -open import Relation.Binary open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) ------------------------------------------------------------------------ diff --git a/src/Data/Char/Properties.agda b/src/Data/Char/Properties.agda index 52a997fd81..970eb6249a 100644 --- a/src/Data/Char/Properties.agda +++ b/src/Data/Char/Properties.agda @@ -17,7 +17,13 @@ open import Data.Product.Base using (_,_) open import Function.Base open import Relation.Nullary using (¬_; yes; no) open import Relation.Nullary.Decidable using (map′; isYes) -open import Relation.Binary +open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Bundles + using (Setoid; DecSetoid; StrictPartialOrder; StrictTotalOrder; Preorder; Poset; DecPoset) +open import Relation.Binary.Structures + using (IsDecEquivalence; IsStrictPartialOrder; IsStrictTotalOrder; IsPreorder; IsPartialOrder; IsDecPartialOrder; IsEquivalence) +open import Relation.Binary.Definitions + using (Decidable; Trichotomous; Irreflexive; Transitive; Asymmetric; Antisymmetric; Symmetric; Substitutive; Reflexive; tri<; tri≈; tri>) import Relation.Binary.Construct.On as On import Relation.Binary.Construct.Subst.Equality as Subst import Relation.Binary.Construct.Closure.Reflexive as Refl diff --git a/src/Data/Container/Properties.agda b/src/Data/Container/Properties.agda index 9ee24ad878..720455fefa 100644 --- a/src/Data/Container/Properties.agda +++ b/src/Data/Container/Properties.agda @@ -9,7 +9,7 @@ module Data.Container.Properties where import Function.Base as F -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) open import Data.Container.Core open import Data.Container.Relation.Binary.Equality.Setoid diff --git a/src/Data/Container/Related.agda b/src/Data/Container/Related.agda index a62603ac49..5f1715c765 100644 --- a/src/Data/Container/Related.agda +++ b/src/Data/Container/Related.agda @@ -12,7 +12,7 @@ module Data.Container.Related where open import Level using (_⊔_) open import Data.Container.Core import Function.Related as Related -open import Relation.Binary +open import Relation.Binary.Bundles using (Preorder; Setoid) open import Data.Container.Membership open Related public diff --git a/src/Data/Container/Relation/Binary/Equality/Setoid.agda b/src/Data/Container/Relation/Binary/Equality/Setoid.agda index 993aaef60b..c530413939 100644 --- a/src/Data/Container/Relation/Binary/Equality/Setoid.agda +++ b/src/Data/Container/Relation/Binary/Equality/Setoid.agda @@ -11,7 +11,10 @@ open import Relation.Binary.Bundles using (Setoid) module Data.Container.Relation.Binary.Equality.Setoid {c e} (S : Setoid c e) where open import Level using (_⊔_; suc) -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive) open import Data.Container.Core open import Data.Container.Relation.Binary.Pointwise diff --git a/src/Data/Container/Relation/Binary/Pointwise/Properties.agda b/src/Data/Container/Relation/Binary/Pointwise/Properties.agda index 7ddc209860..45b824cc56 100644 --- a/src/Data/Container/Relation/Binary/Pointwise/Properties.agda +++ b/src/Data/Container/Relation/Binary/Pointwise/Properties.agda @@ -13,7 +13,10 @@ open import Data.Container.Core open import Data.Container.Relation.Binary.Pointwise open import Data.Product.Base using (_,_; Σ-syntax; -,_) open import Level using (_⊔_) -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive) +open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; subst; cong) diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda index b0cf553d0d..a15287a48f 100644 --- a/src/Data/Fin/Induction.agda +++ b/src/Data/Fin/Induction.agda @@ -21,8 +21,10 @@ open import Function.Base using (flip; _$_) open import Induction open import Induction.WellFounded as WF open import Level using (Level) -open import Relation.Binary - using (Rel; Decidable; IsPartialOrder; IsStrictPartialOrder; StrictPartialOrder) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (StrictPartialOrder) +open import Relation.Binary.Structures using (IsPartialOrder; IsStrictPartialOrder) +open import Relation.Binary.Definitions using (Decidable) import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd import Relation.Binary.Construct.Flip.Ord as Ord import Relation.Binary.Construct.NonStrictToStrict as ToStrict diff --git a/src/Data/Float/Properties.agda b/src/Data/Float/Properties.agda index b2caebb616..a397dd53ec 100644 --- a/src/Data/Float/Properties.agda +++ b/src/Data/Float/Properties.agda @@ -17,7 +17,12 @@ import Data.Word.Base as Word import Data.Word.Properties as Wₚ open import Function.Base using (_∘_) open import Relation.Nullary.Decidable as RN using (map′) -open import Relation.Binary +open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Bundles using (Setoid; DecSetoid) +open import Relation.Binary.Structures + using (IsEquivalence; IsDecEquivalence) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive; Substitutive; Decidable; DecidableEquality) import Relation.Binary.Construct.On as On open import Relation.Binary.PropositionalEquality diff --git a/src/Data/Integer/Divisibility.agda b/src/Data/Integer/Divisibility.agda index 0f089b30fc..a8c55a1e2a 100644 --- a/src/Data/Integer/Divisibility.agda +++ b/src/Data/Integer/Divisibility.agda @@ -18,7 +18,7 @@ import Data.Nat.Properties as ℕᵖ import Data.Nat.Divisibility as ℕᵈ import Data.Nat.Coprimality as ℕᶜ open import Level -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _Preserves_⟶_) open import Relation.Binary.PropositionalEquality ------------------------------------------------------------------------ diff --git a/src/Data/Integer/Divisibility/Signed.agda b/src/Data/Integer/Divisibility/Signed.agda index db80bcb3a0..af06d57486 100644 --- a/src/Data/Integer/Divisibility/Signed.agda +++ b/src/Data/Integer/Divisibility/Signed.agda @@ -21,7 +21,11 @@ import Data.Nat.Properties as ℕ import Data.Sign as S import Data.Sign.Properties as SProp open import Level -open import Relation.Binary +open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_) +open import Relation.Binary.Bundles using (Preorder) +open import Relation.Binary.Structures using (IsPreorder) +open import Relation.Binary.Definitions + using (Reflexive; Transitive; Decidable) open import Relation.Binary.PropositionalEquality import Relation.Binary.Reasoning.Preorder as PreorderReasoning open import Relation.Nullary.Decidable using (yes; no) diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 78011e54b1..ef7528495e 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -27,7 +27,13 @@ open import Data.Sign as Sign using (Sign) renaming (_*_ to _𝕊*_) import Data.Sign.Properties as 𝕊ₚ open import Function.Base using (_∘_; _$_; id) open import Level using (0ℓ) -open import Relation.Binary +open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_) +open import Relation.Binary.Bundles using + (Setoid; DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder) +open import Relation.Binary.Structures + using (IsPreorder; IsTotalPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder) +open import Relation.Binary.Definitions + using (DecidableEquality; Reflexive; Transitive; Antisymmetric; Total; Decidable; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri<; tri>) open import Relation.Binary.PropositionalEquality open import Relation.Nullary using (yes; no; ¬_) import Relation.Nullary.Reflects as Reflects diff --git a/src/Data/List/Countdown.agda b/src/Data/List/Countdown.agda index db8dc806ad..8d6761de27 100644 --- a/src/Data/List/Countdown.agda +++ b/src/Data/List/Countdown.agda @@ -8,7 +8,7 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Level using (0ℓ) -open import Relation.Binary +open import Relation.Binary.Bundles using (DecSetoid) module Data.List.Countdown (D : DecSetoid 0ℓ 0ℓ) where diff --git a/src/Data/List/Fresh/Membership/Setoid.agda b/src/Data/List/Fresh/Membership/Setoid.agda index 6ef9ef4836..5e0b3fdc15 100644 --- a/src/Data/List/Fresh/Membership/Setoid.agda +++ b/src/Data/List/Fresh/Membership/Setoid.agda @@ -6,7 +6,8 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid) module Data.List.Fresh.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda index 047620041d..1b8a67fb7d 100644 --- a/src/Data/List/Membership/Setoid.agda +++ b/src/Data/List/Membership/Setoid.agda @@ -6,7 +6,8 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Definitions using (_Respects_) module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda index d48b3dae45..451ce28c10 100644 --- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda +++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda @@ -36,7 +36,8 @@ open import Function.Inverse as Inv using (_↔_; Inverse; inverse) open import Function.Related as Related using (↔⇒; ⌊_⌋; ⌊_⌋→; ⇒→; K-refl; SK-sym) open import Function.Related.TypeIsomorphisms -open import Relation.Binary +open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Bundles using (Preorder; Setoid) import Relation.Binary.Reasoning.Setoid as EqR import Relation.Binary.Reasoning.Preorder as PreorderReasoning open import Relation.Binary.PropositionalEquality as P diff --git a/src/Data/List/Relation/Binary/Disjoint/Propositional.agda b/src/Data/List/Relation/Binary/Disjoint/Propositional.agda index 6b78c64c85..f60f275b89 100644 --- a/src/Data/List/Relation/Binary/Disjoint/Propositional.agda +++ b/src/Data/List/Relation/Binary/Disjoint/Propositional.agda @@ -6,8 +6,6 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary - module Data.List.Relation.Binary.Disjoint.Propositional {a} {A : Set a} where diff --git a/src/Data/List/Relation/Binary/Disjoint/Setoid.agda b/src/Data/List/Relation/Binary/Disjoint/Setoid.agda index 6ea7e15cf7..d912c28825 100644 --- a/src/Data/List/Relation/Binary/Disjoint/Setoid.agda +++ b/src/Data/List/Relation/Binary/Disjoint/Setoid.agda @@ -6,7 +6,8 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid) module Data.List.Relation.Binary.Disjoint.Setoid {c ℓ} (S : Setoid c ℓ) where diff --git a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda index 43a67d4d7d..bc5a95fc77 100644 --- a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda @@ -16,7 +16,8 @@ open import Data.List.Relation.Unary.All.Properties using (¬Any⇒All¬) open import Data.List.Relation.Unary.Any.Properties using (++⁻) open import Data.Product.Base using (_,_) open import Data.Sum.Base using (inj₁; inj₂) -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Definitions using (Symmetric) open import Relation.Nullary.Negation using (¬_) ------------------------------------------------------------------------ diff --git a/src/Data/List/Relation/Binary/Equality/DecPropositional.agda b/src/Data/List/Relation/Binary/Equality/DecPropositional.agda index 1697020ed3..0be92107c7 100644 --- a/src/Data/List/Relation/Binary/Equality/DecPropositional.agda +++ b/src/Data/List/Relation/Binary/Equality/DecPropositional.agda @@ -10,7 +10,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.PropositionalEquality module Data.List.Relation.Binary.Equality.DecPropositional diff --git a/src/Data/List/Relation/Binary/Equality/DecSetoid.agda b/src/Data/List/Relation/Binary/Equality/DecSetoid.agda index ec82d91dcf..670e3c981b 100644 --- a/src/Data/List/Relation/Binary/Equality/DecSetoid.agda +++ b/src/Data/List/Relation/Binary/Equality/DecSetoid.agda @@ -6,7 +6,9 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (DecSetoid) +open import Relation.Binary.Structures using (IsDecEquivalence) +open import Relation.Binary.Definitions using (Decidable) module Data.List.Relation.Binary.Equality.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where diff --git a/src/Data/List/Relation/Binary/Equality/Propositional.agda b/src/Data/List/Relation/Binary/Equality/Propositional.agda index 9ecb2cfd6b..8b45be7d27 100644 --- a/src/Data/List/Relation/Binary/Equality/Propositional.agda +++ b/src/Data/List/Relation/Binary/Equality/Propositional.agda @@ -10,7 +10,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (_⇒_) module Data.List.Relation.Binary.Equality.Propositional {a} {A : Set a} where diff --git a/src/Data/List/Relation/Binary/Infix/Homogeneous/Properties.agda b/src/Data/List/Relation/Binary/Infix/Homogeneous/Properties.agda index cf7c2b7b27..0abb36a149 100644 --- a/src/Data/List/Relation/Binary/Infix/Homogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Infix/Homogeneous/Properties.agda @@ -10,7 +10,9 @@ module Data.List.Relation.Binary.Infix.Homogeneous.Properties where open import Level open import Function.Base using (_∘′_) -open import Relation.Binary +open import Relation.Binary.Core using (REL) +open import Relation.Binary.Structures + using (IsPreorder; IsPartialOrder; IsDecPartialOrder) open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise) open import Data.List.Relation.Binary.Infix.Heterogeneous diff --git a/src/Data/List/Relation/Binary/Lex/NonStrict.agda b/src/Data/List/Relation/Binary/Lex/NonStrict.agda index e87e1e0b45..4afe0f8242 100644 --- a/src/Data/List/Relation/Binary/Lex/NonStrict.agda +++ b/src/Data/List/Relation/Binary/Lex/NonStrict.agda @@ -19,7 +19,13 @@ open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []) import Data.List.Relation.Binary.Lex.Strict as Strict open import Level open import Relation.Nullary -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Bundles + using (Poset; StrictPartialOrder; DecTotalOrder; StrictTotalOrder; Preorder) +open import Relation.Binary.Structures + using (IsEquivalence; IsPartialOrder; IsStrictPartialOrder; IsTotalOrder; IsStrictTotalOrder; IsPreorder; IsDecTotalOrder) +open import Relation.Binary.Definitions + using (Irreflexive; _Respects₂_; Antisymmetric; Asymmetric; Symmetric; Transitive; Decidable; Total; Trichotomous) import Relation.Binary.Construct.NonStrictToStrict as Conv import Data.List.Relation.Binary.Lex as Core diff --git a/src/Data/List/Relation/Binary/Lex/Strict.agda b/src/Data/List/Relation/Binary/Lex/Strict.agda index d79311ba14..9ea73457fe 100644 --- a/src/Data/List/Relation/Binary/Lex/Strict.agda +++ b/src/Data/List/Relation/Binary/Lex/Strict.agda @@ -19,7 +19,13 @@ open import Data.Sum.Base using (inj₁; inj₂) open import Data.List.Base using (List; []; _∷_) open import Level using (_⊔_) open import Relation.Nullary using (yes; no; ¬_) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Bundles + using (StrictPartialOrder; StrictTotalOrder; Preorder; Poset; DecPoset; DecTotalOrder) +open import Relation.Binary.Structures + using (IsEquivalence; IsStrictPartialOrder; IsStrictTotalOrder; IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder; IsDecTotalOrder) +open import Relation.Binary.Definitions + using (Irreflexive; Symmetric; _Respects₂_; Total; Asymmetric; Antisymmetric; Transitive; Trichotomous; Decidable; tri≈; tri<; tri>) open import Relation.Binary.Consequences open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise; []; _∷_; head; tail) diff --git a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda index 6b9fd9c20d..12015b3076 100644 --- a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda +++ b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda @@ -14,7 +14,10 @@ open import Data.List.Relation.Binary.Pointwise.Base as Pointwise open import Data.List.Relation.Binary.Pointwise.Properties as Pointwise using (symmetric) 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.Structures using (IsEquivalence) +open import Relation.Binary.Definitions using (Reflexive; Symmetric) private variable diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional.agda b/src/Data/List/Relation/Binary/Permutation/Propositional.agda index 5d9068755b..aaea103279 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional.agda @@ -10,7 +10,10 @@ module Data.List.Relation.Binary.Permutation.Propositional {a} {A : Set a} where open import Data.List.Base using (List; []; _∷_) -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; Transitive) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) import Relation.Binary.Reasoning.Setoid as EqReasoning diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda index 42430b90ea..82475a505b 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda @@ -27,7 +27,8 @@ open import Function.Equality using (_⟨$⟩_) open import Function.Inverse as Inv using (inverse) open import Level using (Level) open import Relation.Unary using (Pred) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_) +open import Relation.Binary.Definitions using (_Respects_; Decidable) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_ ; refl ; cong; cong₂; _≢_) open import Relation.Nullary diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda index a9a0cf6400..fe3f095ee5 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda @@ -6,7 +6,11 @@ {-# 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) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive) module Data.List.Relation.Binary.Permutation.Setoid {a ℓ} (S : Setoid a ℓ) where diff --git a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda index 5706dbc36e..202bff89b0 100644 --- a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda @@ -25,7 +25,9 @@ open import Function.Base open import Relation.Nullary.Negation using (¬_) open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no; _because_) open import Relation.Unary as U using (Pred) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; REL; _⇒_) +open import Relation.Binary.Definitions + using (Trans; Antisym; Irrelevant; Decidable) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; _≢_) private diff --git a/src/Data/List/Relation/Binary/Prefix/Homogeneous/Properties.agda b/src/Data/List/Relation/Binary/Prefix/Homogeneous/Properties.agda index 97ee8cc41b..ad4291432e 100644 --- a/src/Data/List/Relation/Binary/Prefix/Homogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Prefix/Homogeneous/Properties.agda @@ -10,7 +10,9 @@ module Data.List.Relation.Binary.Prefix.Homogeneous.Properties where open import Level open import Function.Base using (_∘′_) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; REL; _⇒_) +open import Relation.Binary.Structures + using (IsPreorder; IsPartialOrder; IsDecPartialOrder) open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise) open import Data.List.Relation.Binary.Prefix.Heterogeneous diff --git a/src/Data/List/Relation/Binary/Sublist/DecPropositional.agda b/src/Data/List/Relation/Binary/Sublist/DecPropositional.agda index 6604f4aeec..2e1878e906 100644 --- a/src/Data/List/Relation/Binary/Sublist/DecPropositional.agda +++ b/src/Data/List/Relation/Binary/Sublist/DecPropositional.agda @@ -8,7 +8,9 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (DecPoset) +open import Relation.Binary.Structures using (IsDecPartialOrder) +open import Relation.Binary.Definitions using (Decidable) open import Agda.Builtin.Equality using (_≡_) module Data.List.Relation.Binary.Sublist.DecPropositional diff --git a/src/Data/List/Relation/Binary/Sublist/DecSetoid.agda b/src/Data/List/Relation/Binary/Sublist/DecSetoid.agda index 654d6c6a0e..a184386034 100644 --- a/src/Data/List/Relation/Binary/Sublist/DecSetoid.agda +++ b/src/Data/List/Relation/Binary/Sublist/DecSetoid.agda @@ -8,7 +8,10 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (DecSetoid; DecPoset) +open import Relation.Binary.Structures + using (IsDecPartialOrder) +open import Relation.Binary.Definitions using (Decidable) module Data.List.Relation.Binary.Sublist.DecSetoid {c ℓ} (S : DecSetoid c ℓ) where diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous.agda index 698dd789b0..7aa3f4dd5d 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous.agda @@ -11,7 +11,8 @@ open import Data.List.Base using (List; []; _∷_; [_]) open import Data.List.Relation.Unary.Any using (Any; here; there) open import Level using (_⊔_) -open import Relation.Binary +open import Relation.Binary.Core using (REL; _⇒_) +open import Relation.Binary.Definitions using (_⟶_Respects_; Min) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) open import Relation.Unary using (Pred) diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional.agda b/src/Data/List/Relation/Binary/Sublist/Propositional.agda index 7700e10e59..a0f816ad84 100644 --- a/src/Data/List/Relation/Binary/Sublist/Propositional.agda +++ b/src/Data/List/Relation/Binary/Sublist/Propositional.agda @@ -14,7 +14,10 @@ open import Data.List.Base using (List) open import Data.List.Relation.Binary.Equality.Propositional using (≋⇒≡) import Data.List.Relation.Binary.Sublist.Setoid as SetoidSublist open import Data.List.Relation.Unary.Any using (Any) -open import Relation.Binary +open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Bundles using (Preorder; Poset) +open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder) +open import Relation.Binary.Definitions using (Antisymmetric) open import Relation.Binary.PropositionalEquality open import Relation.Unary using (Pred) diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid.agda b/src/Data/List/Relation/Binary/Sublist/Setoid.agda index a07c6ffc25..86e16ab80c 100644 --- a/src/Data/List/Relation/Binary/Sublist/Setoid.agda +++ b/src/Data/List/Relation/Binary/Sublist/Setoid.agda @@ -26,7 +26,9 @@ import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties as HeterogeneousProperties open import Data.Product.Base using (∃; ∃₂; _×_; _,_; proj₂) -open import Relation.Binary +open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Bundles using (Preorder; Poset) +open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) open import Relation.Nullary using (¬_; Dec; yes; no) diff --git a/src/Data/List/Relation/Binary/Subset/Setoid.agda b/src/Data/List/Relation/Binary/Subset/Setoid.agda index 3bb516fb5c..0968e06332 100644 --- a/src/Data/List/Relation/Binary/Subset/Setoid.agda +++ b/src/Data/List/Relation/Binary/Subset/Setoid.agda @@ -6,7 +6,8 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid) module Data.List.Relation.Binary.Subset.Setoid {c ℓ} (S : Setoid c ℓ) where diff --git a/src/Data/List/Relation/Binary/Suffix/Homogeneous/Properties.agda b/src/Data/List/Relation/Binary/Suffix/Homogeneous/Properties.agda index 8f8e9c4a77..0a5298f431 100644 --- a/src/Data/List/Relation/Binary/Suffix/Homogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Suffix/Homogeneous/Properties.agda @@ -10,7 +10,9 @@ module Data.List.Relation.Binary.Suffix.Homogeneous.Properties where open import Level open import Function.Base using (_∘′_) -open import Relation.Binary +open import Relation.Binary.Core using (REL) +open import Relation.Binary.Structures + using (IsPreorder; IsPartialOrder; IsDecPartialOrder) open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise) open import Data.List.Relation.Binary.Suffix.Heterogeneous diff --git a/src/Data/List/Relation/Ternary/Interleaving.agda b/src/Data/List/Relation/Ternary/Interleaving.agda index 8818638518..08d9f728e7 100644 --- a/src/Data/List/Relation/Ternary/Interleaving.agda +++ b/src/Data/List/Relation/Ternary/Interleaving.agda @@ -15,7 +15,7 @@ open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_ open import Data.Product.Base as Prod using (∃; ∃₂; _×_; uncurry; _,_; -,_; proj₂) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Function.Base -open import Relation.Binary +open import Relation.Binary.Core using (REL; _⇒_) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) ------------------------------------------------------------------------ diff --git a/src/Data/List/Relation/Ternary/Interleaving/Properties.agda b/src/Data/List/Relation/Ternary/Interleaving/Properties.agda index da3d687ba5..dff26bb6b2 100644 --- a/src/Data/List/Relation/Ternary/Interleaving/Properties.agda +++ b/src/Data/List/Relation/Ternary/Interleaving/Properties.agda @@ -14,9 +14,7 @@ open import Data.List.Base hiding (_∷ʳ_) open import Data.List.Properties using (reverse-involutive) open import Data.List.Relation.Ternary.Interleaving hiding (map) open import Function.Base using (_$_) -open import Relation.Binary ---open import Relation.Binary.PropositionalEquality --- using (_≡_; refl; sym; cong; module ≡-Reasoning) +open import Relation.Binary.Core using (REL) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; cong; module ≡-Reasoning) open ≡-Reasoning diff --git a/src/Data/List/Relation/Unary/Enumerates/Setoid.agda b/src/Data/List/Relation/Unary/Enumerates/Setoid.agda index 4ac2f914d7..8da8806ce1 100644 --- a/src/Data/List/Relation/Unary/Enumerates/Setoid.agda +++ b/src/Data/List/Relation/Unary/Enumerates/Setoid.agda @@ -8,7 +8,7 @@ open import Data.List.Base using (List) open import Level -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) module Data.List.Relation.Unary.Enumerates.Setoid {a ℓ} (S : Setoid a ℓ) where diff --git a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda index ba400055f3..f5e0a53c5c 100644 --- a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda +++ b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda @@ -22,7 +22,7 @@ open import Function.Bundles using (Surjection) open import Function.Definitions using (Surjective) open import Function.Consequences using (strictlySurjective⇒surjective) open import Level -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid; DecSetoid) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) open import Relation.Binary.Properties.Setoid using (respʳ-flip) diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 43496f3139..0072a2d325 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -27,7 +27,13 @@ open import Function.Base using (_∘_; _$_; id) open import Function.Definitions open import Function.Consequences.Propositional open import Level using (0ℓ) -open import Relation.Binary +open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_) +open import Relation.Binary.Bundles + using (Setoid; DecSetoid; StrictPartialOrder; StrictTotalOrder; Preorder; Poset; TotalOrder; DecTotalOrder) +open import Relation.Binary.Definitions + using (Decidable; Irreflexive; Transitive; Reflexive; Antisymmetric; Total; Trichotomous; tri≈; tri<; tri>) +open import Relation.Binary.Structures + using (IsDecEquivalence; IsStrictPartialOrder; IsStrictTotalOrder; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder) open import Relation.Binary.Consequences open import Relation.Binary.Morphism import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphism diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda index 94bfe8968c..68237de411 100644 --- a/src/Data/Nat/Coprimality.agda +++ b/src/Data/Nat/Coprimality.agda @@ -23,7 +23,8 @@ open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; _≢_; refl; trans; cong; subst; module ≡-Reasoning) open import Relation.Nullary as Nullary hiding (recompute) open import Relation.Nullary.Negation using (contradiction) -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Definitions using (Symmetric; Decidable) open ≤-Reasoning diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index 1b1321906d..ea4814b964 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -18,7 +18,12 @@ open import Function.Bundles using (_⇔_; mk⇔) open import Level using (0ℓ) open import Relation.Nullary.Decidable as Dec using (False; yes; no) open import Relation.Nullary.Negation.Core using (contradiction) -open import Relation.Binary +open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Bundles using (Preorder; Poset) +open import Relation.Binary.Structures + using (IsPreorder; IsPartialOrder) +open import Relation.Binary.Definitions + using (Reflexive; Transitive; Antisymmetric; Decidable) import Relation.Binary.Reasoning.Preorder as PreorderReasoning open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst) diff --git a/src/Data/Nat/GCD.agda b/src/Data/Nat/GCD.agda index f54b09e47f..2aa87002ca 100644 --- a/src/Data/Nat/GCD.agda +++ b/src/Data/Nat/GCD.agda @@ -21,7 +21,7 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) open import Function.Base using (_$_; _∘_) open import Induction using (build) open import Induction.Lexicographic using (_⊗_; [_⊗_]) -open import Relation.Binary +open import Relation.Binary.Definitions using (tri<; tri>; tri≈; Symmetric) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; _≢_; subst; cong) open import Relation.Nullary.Decidable using (Dec) diff --git a/src/Data/Nat/LCM.agda b/src/Data/Nat/LCM.agda index ccb1fbbf5b..545870574f 100644 --- a/src/Data/Nat/LCM.agda +++ b/src/Data/Nat/LCM.agda @@ -19,7 +19,6 @@ open import Data.Product.Base using (_×_; _,_; uncurry′; ∃) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning) -open import Relation.Binary open import Relation.Nullary.Decidable using (False; fromWitnessFalse) private diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 2b9a2a4819..be41e093ac 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -31,7 +31,14 @@ open import Function.Bundles using (_↣_) open import Function.Metric.Nat open import Level using (0ℓ) open import Relation.Unary as U using (Pred) -open import Relation.Binary +open import Relation.Binary.Core + using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_) +open import Relation.Binary.Bundles + using (DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder) +open import Relation.Binary.Structures + using (IsDecEquivalence; IsPreorder; IsTotalPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder) +open import Relation.Binary.Definitions + using (DecidableEquality; Irrelevant; Reflexive; Antisymmetric; Transitive; Total; Decidable; Connex; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri>; tri<; _Respects₂_) open import Relation.Binary.Consequences using (flip-Connex) open import Relation.Binary.PropositionalEquality open import Relation.Nullary hiding (Irrelevant) diff --git a/src/Data/Product/Function/Dependent/Setoid/WithK.agda b/src/Data/Product/Function/Dependent/Setoid/WithK.agda index 3336ecb5e5..b4c30a26aa 100644 --- a/src/Data/Product/Function/Dependent/Setoid/WithK.agda +++ b/src/Data/Product/Function/Dependent/Setoid/WithK.agda @@ -12,7 +12,6 @@ module Data.Product.Function.Dependent.Setoid.WithK where open import Data.Product.Base using (_,_) open import Data.Product.Function.Dependent.Setoid using (surjection) open import Data.Product.Relation.Binary.Pointwise.Dependent -open import Relation.Binary open import Function.Base open import Function.Equality as F using (_⟶_; _⟨$⟩_) open import Function.Equivalence as Eq diff --git a/src/Data/Product/Function/NonDependent/Setoid.agda b/src/Data/Product/Function/NonDependent/Setoid.agda index 93e388da23..1d69d9c85b 100644 --- a/src/Data/Product/Function/NonDependent/Setoid.agda +++ b/src/Data/Product/Function/NonDependent/Setoid.agda @@ -11,7 +11,8 @@ module Data.Product.Function.NonDependent.Setoid where open import Data.Product.Base using (map; _,_; <_,_>; proj₁; proj₂) open import Data.Product.Relation.Binary.Pointwise.NonDependent -open import Relation.Binary +open import Relation.Binary.Core using (_=[_]⇒_) +open import Relation.Binary.Bundles using (Setoid) open import Function.Equality as F using (_⟶_; _⟨$⟩_) open import Function.Equivalence as Eq using (Equivalence; _⇔_; module Equivalence) diff --git a/src/Data/Product/Relation/Binary/Lex/NonStrict.agda b/src/Data/Product/Relation/Binary/Lex/NonStrict.agda index e8752c1caf..534ddd6bdc 100644 --- a/src/Data/Product/Relation/Binary/Lex/NonStrict.agda +++ b/src/Data/Product/Relation/Binary/Lex/NonStrict.agda @@ -14,7 +14,13 @@ module Data.Product.Relation.Binary.Lex.NonStrict where open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) open import Data.Sum.Base using (inj₁; inj₂) open import Level using (Level) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Bundles + using (Poset; DecTotalOrder; TotalOrder) +open import Relation.Binary.Structures + using (IsPartialOrder; IsEquivalence; IsTotalOrder; IsDecTotalOrder) +open import Relation.Binary.Definitions + using (Transitive; Symmetric; Decidable; Antisymmetric; Total; Trichotomous; Irreflexive; Asymmetric; _Respects₂_; tri<; tri>; tri≈) open import Relation.Binary.Consequences import Relation.Binary.Construct.NonStrictToStrict as Conv open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda index d0a09fa4ac..90129350ea 100644 --- a/src/Data/Product/Relation/Binary/Lex/Strict.agda +++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda @@ -20,7 +20,13 @@ open import Function.Base open import Induction.WellFounded open import Level open import Relation.Nullary.Decidable -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Bundles + using (Preorder; StrictPartialOrder; StrictTotalOrder) +open import Relation.Binary.Structures + using (IsEquivalence; IsPreorder; IsStrictPartialOrder; IsStrictTotalOrder) +open import Relation.Binary.Definitions + using (Transitive; Symmetric; Irreflexive; Asymmetric; Total; Decidable; Antisymmetric; Trichotomous; _Respects₂_; _Respectsʳ_; _Respectsˡ_; tri<; tri>; tri≈) open import Relation.Binary.Consequences open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl) diff --git a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda index 16756bf375..ad40326ab4 100644 --- a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda +++ b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda @@ -26,7 +26,13 @@ open import Function.Related open import Function.Surjection as Surj using (Surjection; _↠_; module Surjection) open import Relation.Nullary.Decidable using (_×-dec_) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Bundles + using (Preorder; Setoid; DecSetoid; Poset; StrictPartialOrder) +open import Relation.Binary.Structures + using (IsEquivalence; IsDecEquivalence; IsPreorder; IsPartialOrder; IsStrictPartialOrder) +open import Relation.Binary.Definitions + using (Reflexive; Irreflexive; Symmetric; Transitive; Antisymmetric; Asymmetric; Total; Decidable; _Respects₂_; _Respects_) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) import Relation.Binary.PropositionalEquality.Properties as P diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index 7c74cd2513..8910cc5998 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -49,7 +49,13 @@ import Data.Sign as S open import Function.Base using (_∘_; _∘′_; _∘₂_; _$_; flip) open import Function.Definitions using (Injective) open import Level using (0ℓ) -open import Relation.Binary +open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_) +open import Relation.Binary.Bundles + using (Setoid; DecSetoid; TotalPreorder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder) +open import Relation.Binary.Structures + using (IsPreorder; IsTotalOrder; IsTotalPreorder; IsPartialOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder) +open import Relation.Binary.Definitions + using (DecidableEquality; Reflexive; Transitive; Antisymmetric; Total; Decidable; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri<; tri>; tri≈; _Respectsʳ_; _Respectsˡ_; _Respects₂_) open import Relation.Binary.PropositionalEquality open import Relation.Binary.Morphism.Structures import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphisms diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 2945a8654a..169c3786ad 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -34,7 +34,13 @@ open import Level using (0ℓ) open import Relation.Nullary using (¬_; yes; no) import Relation.Nullary.Decidable as Dec open import Relation.Nullary.Negation using (contradiction; contraposition) -open import Relation.Binary +open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_) +open import Relation.Binary.Bundles + using (Setoid; DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder) +open import Relation.Binary.Structures + using (IsEquivalence; IsDecEquivalence; IsApartnessRelation; IsTotalPreorder; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive; Cotransitive; Tight; Decidable; Antisymmetric; Asymmetric; Total; Trans; Trichotomous; Irreflexive; Irrelevant; _Respectsˡ_; _Respectsʳ_; _Respects₂_; tri≈; tri<; tri>) import Relation.Binary.Consequences as BC open import Relation.Binary.PropositionalEquality import Relation.Binary.Properties.Poset as PosetProperties diff --git a/src/Data/Record.agda b/src/Data/Record.agda index 6d77f87622..6992294a5e 100644 --- a/src/Data/Record.agda +++ b/src/Data/Record.agda @@ -16,7 +16,7 @@ open import Data.Product.Base hiding (proj₁; proj₂) open import Data.Unit.Polymorphic open import Function.Base using (id; _∘_) open import Level -open import Relation.Binary +open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.PropositionalEquality open import Relation.Nullary open import Relation.Nullary.Decidable diff --git a/src/Data/Star/BoundedVec.agda b/src/Data/Star/BoundedVec.agda index 2755554354..5664cf847d 100644 --- a/src/Data/Star/BoundedVec.agda +++ b/src/Data/Star/BoundedVec.agda @@ -17,7 +17,7 @@ open import Data.Star.Pointer open import Data.Star.List using (List) open import Data.Unit open import Function.Base using (const) -open import Relation.Binary +open import Relation.Binary.Core using (_=[_]⇒_) open import Relation.Binary.Consequences open import Relation.Binary.Construct.Closure.ReflexiveTransitive diff --git a/src/Data/Star/Decoration.agda b/src/Data/Star/Decoration.agda index 48c0f4f11a..d4e968388b 100644 --- a/src/Data/Star/Decoration.agda +++ b/src/Data/Star/Decoration.agda @@ -11,7 +11,8 @@ module Data.Star.Decoration where open import Data.Unit open import Function.Base using (flip) open import Level -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _=[_]⇒_; _⇒_) +open import Relation.Binary.Definitions using (NonEmpty; nonEmpty) open import Relation.Binary.Construct.Closure.ReflexiveTransitive -- A predicate on relation "edges" (think of the relation as a graph). diff --git a/src/Data/Star/Nat.agda b/src/Data/Star/Nat.agda index ef81051ff9..aa1eb9a55b 100644 --- a/src/Data/Star/Nat.agda +++ b/src/Data/Star/Nat.agda @@ -10,7 +10,7 @@ module Data.Star.Nat where open import Data.Unit open import Function.Base using (const) -open import Relation.Binary +open import Relation.Binary.Core using (Rel) open import Relation.Binary.Construct.Closure.ReflexiveTransitive open import Relation.Binary.Construct.Always using (Always) diff --git a/src/Data/Star/Vec.agda b/src/Data/Star/Vec.agda index 2fd96ee75b..108fbe7399 100644 --- a/src/Data/Star/Vec.agda +++ b/src/Data/Star/Vec.agda @@ -14,7 +14,6 @@ open import Data.Star.Decoration open import Data.Star.Pointer as Pointer hiding (lookup) open import Data.Star.List using (List) open import Level using (Level) -open import Relation.Binary open import Relation.Binary.Construct.Closure.ReflexiveTransitive open import Function.Base open import Data.Unit diff --git a/src/Data/String/Properties.agda b/src/Data/String/Properties.agda index beb0d869d8..9c5ae194e2 100644 --- a/src/Data/String/Properties.agda +++ b/src/Data/String/Properties.agda @@ -17,7 +17,13 @@ open import Data.String.Base open import Function.Base open import Relation.Nullary.Decidable using (yes; no) open import Relation.Nullary.Decidable using (map′; isYes) -open import Relation.Binary +open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Bundles + using (Setoid; DecSetoid; StrictPartialOrder; StrictTotalOrder; DecTotalOrder; DecPoset) +open import Relation.Binary.Structures + using (IsEquivalence; IsDecEquivalence; IsStrictPartialOrder; IsStrictTotalOrder; IsDecPartialOrder; IsDecTotalOrder) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive; Substitutive; Decidable) open import Relation.Binary.PropositionalEquality.Core import Relation.Binary.Construct.On as On import Relation.Binary.PropositionalEquality.Properties as PropEq diff --git a/src/Data/Sum/Function/Setoid.agda b/src/Data/Sum/Function/Setoid.agda index 277d5feb98..f04798dd50 100644 --- a/src/Data/Sum/Function/Setoid.agda +++ b/src/Data/Sum/Function/Setoid.agda @@ -10,7 +10,8 @@ module Data.Sum.Function.Setoid where open import Data.Sum.Base open import Data.Sum.Relation.Binary.Pointwise -open import Relation.Binary +open import Relation.Binary.Core using (_=[_]⇒_) +open import Relation.Binary.Bundles using (Setoid) open import Function.Equality as F using (_⟶_; _⟨$⟩_) open import Function.Equivalence as Eq using (Equivalence; _⇔_; module Equivalence) diff --git a/src/Data/Sum/Relation/Binary/LeftOrder.agda b/src/Data/Sum/Relation/Binary/LeftOrder.agda index 1ff3b18d05..397bc598dc 100644 --- a/src/Data/Sum/Relation/Binary/LeftOrder.agda +++ b/src/Data/Sum/Relation/Binary/LeftOrder.agda @@ -17,7 +17,13 @@ open import Function.Base using (_$_; _∘_) open import Level open import Relation.Nullary import Relation.Nullary.Decidable as Dec -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Bundles + using (Preorder; Poset; StrictPartialOrder; TotalOrder; DecTotalOrder; StrictTotalOrder) +open import Relation.Binary.Structures + using (IsPreorder; IsPartialOrder; IsStrictPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictTotalOrder) +open import Relation.Binary.Definitions + using (Reflexive; Transitive; Asymmetric; Total; Decidable; Irreflexive; Antisymmetric; Trichotomous; _Respectsʳ_; _Respectsˡ_; _Respects₂_; tri<; tri>; tri≈) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) ------------------------------------------------------------------------ diff --git a/src/Data/Sum/Relation/Binary/Pointwise.agda b/src/Data/Sum/Relation/Binary/Pointwise.agda index 2b9b4d763d..0c4bf6751c 100644 --- a/src/Data/Sum/Relation/Binary/Pointwise.agda +++ b/src/Data/Sum/Relation/Binary/Pointwise.agda @@ -16,7 +16,13 @@ open import Function.Base using (_∘_; id) open import Function.Inverse using (Inverse) open import Relation.Nullary import Relation.Nullary.Decidable as Dec -open import Relation.Binary +open import Relation.Binary.Core using (REL; Rel; _⇒_) +open import Relation.Binary.Bundles + using (Setoid; DecSetoid; Preorder; Poset) +open import Relation.Binary.Structures + using (IsEquivalence; IsDecEquivalence; IsPreorder; IsPartialOrder; IsStrictPartialOrder) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive; Asymmetric; Substitutive; Decidable; Irreflexive; Antisymmetric; _Respectsˡ_; _Respectsʳ_; _Respects₂_) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) import Relation.Binary.PropositionalEquality.Properties as P diff --git a/src/Data/Tree/AVL/Indexed/WithK.agda b/src/Data/Tree/AVL/Indexed/WithK.agda index 169427e986..4a8944757d 100644 --- a/src/Data/Tree/AVL/Indexed/WithK.agda +++ b/src/Data/Tree/AVL/Indexed/WithK.agda @@ -6,7 +6,9 @@ {-# OPTIONS --with-K --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Structures using (IsStrictTotalOrder) +open import Relation.Binary.Bundles using (StrictTotalOrder) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; subst) module Data.Tree.AVL.Indexed.WithK diff --git a/src/Data/Tree/AVL/IndexedMap.agda b/src/Data/Tree/AVL/IndexedMap.agda index 7b46f3391a..54e4d73bbb 100644 --- a/src/Data/Tree/AVL/IndexedMap.agda +++ b/src/Data/Tree/AVL/IndexedMap.agda @@ -8,7 +8,8 @@ open import Data.Product.Base using (map₁; map₂; ∃; _×_; Σ-syntax; proj₁; _,_; -,_) -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Structures using (IsStrictTotalOrder) open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst) import Data.Tree.AVL.Value diff --git a/src/Data/Tree/AVL/Key.agda b/src/Data/Tree/AVL/Key.agda index 5c47ccbacc..6fd5a1b021 100644 --- a/src/Data/Tree/AVL/Key.agda +++ b/src/Data/Tree/AVL/Key.agda @@ -7,7 +7,9 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles + using (StrictTotalOrder; StrictPartialOrder) +open import Relation.Binary.Definitions using (Reflexive) module Data.Tree.AVL.Key {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂) diff --git a/src/Data/Unit/Polymorphic/Properties.agda b/src/Data/Unit/Polymorphic/Properties.agda index dce385f19e..87519aa9ee 100644 --- a/src/Data/Unit/Polymorphic/Properties.agda +++ b/src/Data/Unit/Polymorphic/Properties.agda @@ -16,7 +16,12 @@ open import Data.Sum.Base using (inj₁) open import Data.Unit.Base renaming (⊤ to ⊤*) open import Data.Unit.Polymorphic.Base using (⊤; tt) open import Relation.Nullary -open import Relation.Binary +open import Relation.Binary.Bundles + using (Setoid; DecSetoid; Preorder; Poset; TotalOrder; DecTotalOrder) +open import Relation.Binary.Structures + using (IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder) +open import Relation.Binary.Definitions + using (Decidable; Antisymmetric; Total) open import Relation.Binary.PropositionalEquality private diff --git a/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda b/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda index 603582bf02..5853bd1f68 100644 --- a/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda +++ b/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda @@ -12,7 +12,11 @@ open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise) import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as PW open import Level using (Level) -open import Relation.Binary +open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) module Data.Vec.Functional.Relation.Binary.Equality.Setoid diff --git a/src/Data/Vec/Functional/Relation/Binary/Pointwise.agda b/src/Data/Vec/Functional/Relation/Binary/Pointwise.agda index a954853bc6..c238293aae 100644 --- a/src/Data/Vec/Functional/Relation/Binary/Pointwise.agda +++ b/src/Data/Vec/Functional/Relation/Binary/Pointwise.agda @@ -10,7 +10,7 @@ module Data.Vec.Functional.Relation.Binary.Pointwise where open import Data.Vec.Functional as VF hiding (map) open import Level using (Level) -open import Relation.Binary +open import Relation.Binary.Core using (REL; _⇒_) private variable diff --git a/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda b/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda index feff1ab55c..148fcf346f 100644 --- a/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda +++ b/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda @@ -19,7 +19,12 @@ open import Data.Vec.Functional as VF hiding (map) open import Data.Vec.Functional.Relation.Binary.Pointwise open import Function.Base open import Level using (Level) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; REL) +open import Relation.Binary.Bundles using (Setoid; DecSetoid) +open import Relation.Binary.Structures + using (IsEquivalence; IsDecEquivalence) +open import Relation.Binary.Definitions + using (Reflexive; Transitive; Symmetric; Decidable) open import Relation.Binary.PropositionalEquality.Core using (_≡_) private diff --git a/src/Data/Vec/Relation/Binary/Equality/DecPropositional.agda b/src/Data/Vec/Relation/Binary/Equality/DecPropositional.agda index da50443c31..06f8d50e7d 100644 --- a/src/Data/Vec/Relation/Binary/Equality/DecPropositional.agda +++ b/src/Data/Vec/Relation/Binary/Equality/DecPropositional.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.PropositionalEquality module Data.Vec.Relation.Binary.Equality.DecPropositional diff --git a/src/Data/Vec/Relation/Binary/Equality/DecSetoid.agda b/src/Data/Vec/Relation/Binary/Equality/DecSetoid.agda index f3bd4cb1a9..01fd39b051 100644 --- a/src/Data/Vec/Relation/Binary/Equality/DecSetoid.agda +++ b/src/Data/Vec/Relation/Binary/Equality/DecSetoid.agda @@ -6,7 +6,8 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (DecSetoid) +open import Relation.Binary.Structures using (IsDecEquivalence) module Data.Vec.Relation.Binary.Equality.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where diff --git a/src/Data/Vec/Relation/Binary/Equality/Propositional.agda b/src/Data/Vec/Relation/Binary/Equality/Propositional.agda index 15e85a6bcf..93b837fed6 100644 --- a/src/Data/Vec/Relation/Binary/Equality/Propositional.agda +++ b/src/Data/Vec/Relation/Binary/Equality/Propositional.agda @@ -6,8 +6,6 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary - module Data.Vec.Relation.Binary.Equality.Propositional {a} {A : Set a} where open import Data.Nat.Base using (ℕ; zero; suc; _+_) diff --git a/src/Data/Vec/Relation/Binary/Equality/Setoid.agda b/src/Data/Vec/Relation/Binary/Equality/Setoid.agda index d40bd24998..7e2e743088 100644 --- a/src/Data/Vec/Relation/Binary/Equality/Setoid.agda +++ b/src/Data/Vec/Relation/Binary/Equality/Setoid.agda @@ -6,7 +6,10 @@ {-# 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) +open import Relation.Binary.Definitions using (Reflexive; Sym; Trans) module Data.Vec.Relation.Binary.Equality.Setoid {a ℓ} (S : Setoid a ℓ) where @@ -18,7 +21,6 @@ open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW using (Pointwise) open import Function.Base open import Level using (_⊔_) -open import Relation.Binary open Setoid S renaming (Carrier to A) diff --git a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda index 82036a5352..487caa4c0e 100644 --- a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda +++ b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda @@ -20,7 +20,13 @@ import Data.Vec.Relation.Binary.Lex.Strict as Strict open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise using (Pointwise; []; _∷_; head; tail) open import Function.Base using (id) -open import Relation.Binary +open import Relation.Binary.Core using (REL; Rel; _⇒_) +open import Relation.Binary.Bundles + using (Poset; StrictPartialOrder; DecPoset; DecStrictPartialOrder; DecTotalOrder; StrictTotalOrder; Preorder; TotalOrder) +open import Relation.Binary.Structures + using (IsEquivalence; IsPartialOrder; IsStrictPartialOrder; IsDecPartialOrder; IsDecStrictPartialOrder; IsDecTotalOrder; IsStrictTotalOrder; IsPreorder; IsTotalOrder) +open import Relation.Binary.Definitions + using (Irreflexive; _Respects₂_; Antisymmetric; Asymmetric; Symmetric; Trans; Decidable; Total; Trichotomous) import Relation.Binary.Construct.NonStrictToStrict as Conv open import Relation.Nullary hiding (Irrelevant) open import Level using (Level; _⊔_) diff --git a/src/Data/Vec/Relation/Binary/Lex/Strict.agda b/src/Data/Vec/Relation/Binary/Lex/Strict.agda index 3bafcdca03..450c23809b 100644 --- a/src/Data/Vec/Relation/Binary/Lex/Strict.agda +++ b/src/Data/Vec/Relation/Binary/Lex/Strict.agda @@ -24,7 +24,13 @@ open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise open import Function.Base using (id; _on_; _∘_) open import Induction.WellFounded open import Relation.Nullary using (yes; no; ¬_) -open import Relation.Binary +open import Relation.Binary.Core using (REL; Rel; _⇒_) +open import Relation.Binary.Bundles + using (Poset; StrictPartialOrder; DecPoset; DecStrictPartialOrder; DecTotalOrder; StrictTotalOrder; Preorder; TotalOrder) +open import Relation.Binary.Structures + using (IsEquivalence; IsPartialOrder; IsStrictPartialOrder; IsDecPartialOrder; IsDecStrictPartialOrder; IsDecTotalOrder; IsStrictTotalOrder; IsPreorder; IsTotalOrder; IsPartialEquivalence) +open import Relation.Binary.Definitions + using (Irreflexive; _Respects₂_; _Respectsˡ_; _Respectsʳ_; Antisymmetric; Asymmetric; Symmetric; Trans; Decidable; Total; Trichotomous; Transitive; Irrelevant; tri≈; tri>; tri<) open import Relation.Binary.Consequences open import Relation.Binary.Construct.On as On using (wellFounded) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda index 85bd6df9da..c6835b73e1 100644 --- a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda +++ b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda @@ -16,7 +16,12 @@ open import Data.Vec.Relation.Unary.All using (All; []; _∷_) open import Level using (Level; _⊔_) open import Function.Base using (_∘_) open import Function.Bundles using (_⇔_; mk⇔) -open import Relation.Binary +open import Relation.Binary.Core using (REL; Rel; _⇒_) +open import Relation.Binary.Bundles using (Setoid; DecSetoid) +open import Relation.Binary.Structures + using (IsEquivalence; IsDecEquivalence) +open import Relation.Binary.Definitions + using (Trans; Decidable; Reflexive; Sym) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) open import Relation.Nullary.Decidable using (yes; no; _×-dec_; map′) open import Relation.Unary using (Pred) diff --git a/src/Data/Vec/Relation/Unary/Any/Properties.agda b/src/Data/Vec/Relation/Unary/Any/Properties.agda index 96f8874bd7..6069a6b6db 100644 --- a/src/Data/Vec/Relation/Unary/Any/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Any/Properties.agda @@ -28,7 +28,8 @@ open import Function.Inverse using (_↔_; inverse) open import Level using (Level) open import Relation.Nullary.Negation using (¬_) open import Relation.Unary hiding (_∈_) -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Definitions using (_Respects_) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl) private diff --git a/src/Relation/Binary/Construct/Add/Extrema/Equality.agda b/src/Relation/Binary/Construct/Add/Extrema/Equality.agda index b4992e112d..d34e84602f 100644 --- a/src/Relation/Binary/Construct/Add/Extrema/Equality.agda +++ b/src/Relation/Binary/Construct/Add/Extrema/Equality.agda @@ -9,7 +9,11 @@ -- This module is designed to be used with -- Relation.Nullary.Construct.Add.Extrema -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Structures + using (IsEquivalence; IsDecEquivalence) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive; Decidable; Irrelevant; Substitutive) module Relation.Binary.Construct.Add.Extrema.Equality {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where diff --git a/src/Relation/Binary/Construct/Add/Extrema/NonStrict.agda b/src/Relation/Binary/Construct/Add/Extrema/NonStrict.agda index ac1880044d..35fdf49431 100644 --- a/src/Relation/Binary/Construct/Add/Extrema/NonStrict.agda +++ b/src/Relation/Binary/Construct/Add/Extrema/NonStrict.agda @@ -9,7 +9,11 @@ -- This module is designed to be used with -- Relation.Nullary.Construct.Add.Extrema -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Structures + using (IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder; IsDecTotalOrder) +open import Relation.Binary.Definitions + using (Decidable; Transitive; Minimum; Maximum; Total; Irrelevant; Antisymmetric) module Relation.Binary.Construct.Add.Extrema.NonStrict {a ℓ} {A : Set a} (_≤_ : Rel A ℓ) where diff --git a/src/Relation/Binary/Construct/Add/Extrema/Strict.agda b/src/Relation/Binary/Construct/Add/Extrema/Strict.agda index 1195e265a9..4ed89565ae 100644 --- a/src/Relation/Binary/Construct/Add/Extrema/Strict.agda +++ b/src/Relation/Binary/Construct/Add/Extrema/Strict.agda @@ -9,7 +9,11 @@ -- This module is designed to be used with -- Relation.Nullary.Construct.Add.Extrema -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Structures + using (IsStrictPartialOrder; IsDecStrictPartialOrder; IsStrictTotalOrder) +open import Relation.Binary.Definitions + using (Asymmetric; Transitive; Decidable; Irrelevant; Trichotomous; Irreflexive; Trans; _Respectsˡ_; _Respectsʳ_; _Respects₂_) module Relation.Binary.Construct.Add.Extrema.Strict {a ℓ} {A : Set a} (_<_ : Rel A ℓ) where diff --git a/src/Relation/Binary/Construct/Add/Infimum/Equality.agda b/src/Relation/Binary/Construct/Add/Infimum/Equality.agda index 4c1fd79449..6f5336fc44 100644 --- a/src/Relation/Binary/Construct/Add/Infimum/Equality.agda +++ b/src/Relation/Binary/Construct/Add/Infimum/Equality.agda @@ -9,7 +9,7 @@ -- This module is designed to be used with -- Relation.Nullary.Construct.Add.Infimum -open import Relation.Binary +open import Relation.Binary.Core using (Rel) module Relation.Binary.Construct.Add.Infimum.Equality {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where diff --git a/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda b/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda index b6cd5e4bf6..5d5cb2a214 100644 --- a/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda +++ b/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda @@ -9,7 +9,11 @@ -- This module is designed to be used with -- Relation.Nullary.Construct.Add.Infimum -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Structures + using (IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder; IsDecTotalOrder) +open import Relation.Binary.Definitions + using (Minimum; Transitive; Total; Decidable; Irrelevant; Antisymmetric) module Relation.Binary.Construct.Add.Infimum.NonStrict {a ℓ} {A : Set a} (_≤_ : Rel A ℓ) where diff --git a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda index e4c8f3a974..ae96849340 100644 --- a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda +++ b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda @@ -9,7 +9,11 @@ -- This module is designed to be used with -- Relation.Nullary.Construct.Add.Infimum -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Structures + using (IsStrictPartialOrder; IsDecStrictPartialOrder; IsStrictTotalOrder) +open import Relation.Binary.Definitions + using (Asymmetric; Transitive; Decidable; Irrelevant; Irreflexive; Trans; Trichotomous; tri≈; tri<; tri>; _Respectsˡ_; _Respectsʳ_; _Respects₂_) module Relation.Binary.Construct.Add.Infimum.Strict {a ℓ} {A : Set a} (_<_ : Rel A ℓ) where diff --git a/src/Relation/Binary/Construct/Add/Point/Equality.agda b/src/Relation/Binary/Construct/Add/Point/Equality.agda index 1715d6f2d1..704d963123 100644 --- a/src/Relation/Binary/Construct/Add/Point/Equality.agda +++ b/src/Relation/Binary/Construct/Add/Point/Equality.agda @@ -9,7 +9,11 @@ -- This module is designed to be used with -- Relation.Nullary.Construct.Add.Point -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Structures + using (IsEquivalence; IsDecEquivalence) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive; Decidable; Irrelevant; Substitutive) module Relation.Binary.Construct.Add.Point.Equality {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where diff --git a/src/Relation/Binary/Construct/Add/Supremum/Equality.agda b/src/Relation/Binary/Construct/Add/Supremum/Equality.agda index 04f9376f8e..c0a18a68e5 100644 --- a/src/Relation/Binary/Construct/Add/Supremum/Equality.agda +++ b/src/Relation/Binary/Construct/Add/Supremum/Equality.agda @@ -9,7 +9,7 @@ -- This module is designed to be used with -- Relation.Nullary.Construct.Add.Supremum -open import Relation.Binary +open import Relation.Binary.Core using (Rel) module Relation.Binary.Construct.Add.Supremum.Equality {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where diff --git a/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda b/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda index a509871377..b550dd4924 100644 --- a/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda +++ b/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda @@ -9,7 +9,11 @@ -- This module is designed to be used with -- Relation.Nullary.Construct.Add.Supremum -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Structures + using (IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder; IsDecTotalOrder) +open import Relation.Binary.Definitions + using (Maximum; Transitive; Total; Decidable; Irrelevant; Antisymmetric) module Relation.Binary.Construct.Add.Supremum.NonStrict {a ℓ} {A : Set a} (_≤_ : Rel A ℓ) where diff --git a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda index b09432961d..d927cf45c4 100644 --- a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda +++ b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda @@ -9,7 +9,11 @@ -- This module is designed to be used with -- Relation.Nullary.Construct.Add.Supremum -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Structures + using (IsStrictPartialOrder; IsDecStrictPartialOrder; IsStrictTotalOrder) +open import Relation.Binary.Definitions + using (Asymmetric; Transitive; Decidable; Irrelevant; Irreflexive; Trans; Trichotomous; tri≈; tri>; tri<; _Respectsˡ_; _Respectsʳ_; _Respects₂_) module Relation.Binary.Construct.Add.Supremum.Strict {a r} {A : Set a} (_<_ : Rel A r) where diff --git a/src/Relation/Binary/Construct/Always.agda b/src/Relation/Binary/Construct/Always.agda index 76eb5e5963..70c22e1034 100644 --- a/src/Relation/Binary/Construct/Always.agda +++ b/src/Relation/Binary/Construct/Always.agda @@ -8,7 +8,10 @@ module Relation.Binary.Construct.Always where -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) open import Relation.Binary.Construct.Constant using (Const) open import Data.Unit.Polymorphic using (⊤; tt) diff --git a/src/Relation/Binary/Construct/Closure/Equivalence.agda b/src/Relation/Binary/Construct/Closure/Equivalence.agda index a4aea65266..622bf20e24 100644 --- a/src/Relation/Binary/Construct/Closure/Equivalence.agda +++ b/src/Relation/Binary/Construct/Closure/Equivalence.agda @@ -11,7 +11,11 @@ module Relation.Binary.Construct.Closure.Equivalence where open import Function.Base using (flip; id; _∘_; _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.Structures using (IsEquivalence) +open import Relation.Binary.Definitions + using (Reflexive; Transitive; Symmetric) open import Relation.Binary.Construct.Closure.ReflexiveTransitive as Star using (Star; ε; _◅◅_; reverse) open import Relation.Binary.Construct.Closure.Symmetric as SC diff --git a/src/Relation/Binary/Construct/Closure/Reflexive/Properties/WithK.agda b/src/Relation/Binary/Construct/Closure/Reflexive/Properties/WithK.agda index 26d04320b0..8684bf119a 100644 --- a/src/Relation/Binary/Construct/Closure/Reflexive/Properties/WithK.agda +++ b/src/Relation/Binary/Construct/Closure/Reflexive/Properties/WithK.agda @@ -8,7 +8,8 @@ module Relation.Binary.Construct.Closure.Reflexive.Properties.WithK where -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Definitions using (Irrelevant; Irreflexive) open import Relation.Binary.Construct.Closure.Reflexive open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong) open import Relation.Nullary.Negation using (contradiction) diff --git a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive.agda b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive.agda index ef9f4fe074..71ab8535d8 100644 --- a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive.agda +++ b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive.agda @@ -8,7 +8,9 @@ module Relation.Binary.Construct.Closure.ReflexiveTransitive where -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _=[_]⇒_; _⇒_) +open import Relation.Binary.Definitions + using (Transitive; Trans; Sym; TransFlip; Reflexive) open import Function.Base open import Level using (_⊔_) diff --git a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda index 963c5b6330..b2c173c190 100644 --- a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda +++ b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda @@ -9,7 +9,10 @@ module Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties where open import Function.Base using (id; _∘_; _$_) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _=[_]⇒_; _⇒_) +open import Relation.Binary.Bundles using (Preorder) +open import Relation.Binary.Structures using (IsPreorder) +open import Relation.Binary.Definitions using (Transitive; Reflexive) open import Relation.Binary.Construct.Closure.ReflexiveTransitive open import Relation.Binary.PropositionalEquality.Core as PropEq using (_≡_; refl; sym; cong; cong₂) diff --git a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties/WithK.agda b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties/WithK.agda index aa2fd6e0a5..ee4078a75c 100644 --- a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties/WithK.agda +++ b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties/WithK.agda @@ -12,7 +12,7 @@ module where open import Function.Base using (_∋_) -open import Relation.Binary +open import Relation.Binary.Core using (Rel) open import Relation.Binary.Construct.Closure.ReflexiveTransitive open import Relation.Binary.PropositionalEquality diff --git a/src/Relation/Binary/Construct/Closure/Symmetric.agda b/src/Relation/Binary/Construct/Closure/Symmetric.agda index c1731b5ecd..369b368f20 100644 --- a/src/Relation/Binary/Construct/Closure/Symmetric.agda +++ b/src/Relation/Binary/Construct/Closure/Symmetric.agda @@ -10,7 +10,8 @@ module Relation.Binary.Construct.Closure.Symmetric where open import Function.Base using (id; _on_) open import Level using (Level) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _=[_]⇒_; _⇒_) +open import Relation.Binary.Definitions using (Symmetric) import Relation.Binary.Construct.On as On private diff --git a/src/Relation/Binary/Construct/Closure/SymmetricTransitive.agda b/src/Relation/Binary/Construct/Closure/SymmetricTransitive.agda index 0ef90ba9b4..5766ce704a 100644 --- a/src/Relation/Binary/Construct/Closure/SymmetricTransitive.agda +++ b/src/Relation/Binary/Construct/Closure/SymmetricTransitive.agda @@ -10,7 +10,12 @@ module Relation.Binary.Construct.Closure.SymmetricTransitive where open import Level open import Function.Base -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _=[_]⇒_; _⇒_) +open import Relation.Binary.Bundles using (PartialSetoid; Setoid) +open import Relation.Binary.Structures + using (IsPartialEquivalence; IsEquivalence) +open import Relation.Binary.Definitions + using (Transitive; Symmetric; Reflexive) private variable diff --git a/src/Relation/Binary/Construct/Closure/Transitive/WithK.agda b/src/Relation/Binary/Construct/Closure/Transitive/WithK.agda index b432e3e1dd..c05323903b 100644 --- a/src/Relation/Binary/Construct/Closure/Transitive/WithK.agda +++ b/src/Relation/Binary/Construct/Closure/Transitive/WithK.agda @@ -9,7 +9,7 @@ module Relation.Binary.Construct.Closure.Transitive.WithK where open import Function.Base using (_∋_) -open import Relation.Binary +open import Relation.Binary.Core using (Rel) open import Relation.Binary.Construct.Closure.Transitive open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) diff --git a/src/Relation/Binary/Construct/Composition.agda b/src/Relation/Binary/Construct/Composition.agda index 7f8ba241b0..4d66ae5171 100644 --- a/src/Relation/Binary/Construct/Composition.agda +++ b/src/Relation/Binary/Construct/Composition.agda @@ -11,7 +11,10 @@ module Relation.Binary.Construct.Composition where open import Data.Product.Base using (∃; _×_; _,_) open import Function.Base open import Level -open import Relation.Binary +open import Relation.Binary.Core using (Rel; REL; _⇒_) +open import Relation.Binary.Structures using (IsPreorder) +open import Relation.Binary.Definitions + using (_Respects_; _Respectsʳ_; _Respectsˡ_; _Respects₂_; Reflexive; Transitive) private variable diff --git a/src/Relation/Binary/Construct/Constant.agda b/src/Relation/Binary/Construct/Constant.agda index 1dad265ea7..8566dc6e30 100644 --- a/src/Relation/Binary/Construct/Constant.agda +++ b/src/Relation/Binary/Construct/Constant.agda @@ -9,7 +9,9 @@ module Relation.Binary.Construct.Constant where open import Level -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive) private variable diff --git a/src/Relation/Binary/Construct/Flip/EqAndOrd.agda b/src/Relation/Binary/Construct/Flip/EqAndOrd.agda index c3c4dc2a18..78671dfbdc 100644 --- a/src/Relation/Binary/Construct/Flip/EqAndOrd.agda +++ b/src/Relation/Binary/Construct/Flip/EqAndOrd.agda @@ -8,7 +8,13 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel; REL; _⇒_) +open import Relation.Binary.Bundles + using (Setoid; DecSetoid; Preorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder; TotalPreorder) +open import Relation.Binary.Structures + using (IsEquivalence; IsDecEquivalence; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder; IsTotalPreorder) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive; Asymmetric; Total; _Respects_; _Respects₂_; Minimum; Maximum; Irreflexive; Antisymmetric; Trichotomous; Decidable; tri<; tri>; tri≈) module Relation.Binary.Construct.Flip.EqAndOrd where diff --git a/src/Relation/Binary/Construct/Flip/Ord.agda b/src/Relation/Binary/Construct/Flip/Ord.agda index 4a2eea690f..742a315cc6 100644 --- a/src/Relation/Binary/Construct/Flip/Ord.agda +++ b/src/Relation/Binary/Construct/Flip/Ord.agda @@ -8,7 +8,13 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel; REL; _⇒_) +open import Relation.Binary.Bundles + using (Setoid; DecSetoid; Preorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder) +open import Relation.Binary.Structures + using (IsEquivalence; IsDecEquivalence; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive; Asymmetric; Total; _Respects_; _Respects₂_; Minimum; Maximum; Irreflexive; Antisymmetric; Trichotomous; Decidable) module Relation.Binary.Construct.Flip.Ord where diff --git a/src/Relation/Binary/Construct/FromPred.agda b/src/Relation/Binary/Construct/FromPred.agda index e08997b9a7..eb39112719 100644 --- a/src/Relation/Binary/Construct/FromPred.agda +++ b/src/Relation/Binary/Construct/FromPred.agda @@ -7,7 +7,10 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Bundles using (Setoid; Preorder) +open import Relation.Binary.Structures using (IsPreorder) +open import Relation.Binary.Definitions using (_Respects_; Reflexive; Transitive) open import Relation.Unary using (Pred) module Relation.Binary.Construct.FromPred diff --git a/src/Relation/Binary/Construct/FromRel.agda b/src/Relation/Binary/Construct/FromRel.agda index 13fc1774c7..3cac113912 100644 --- a/src/Relation/Binary/Construct/FromRel.agda +++ b/src/Relation/Binary/Construct/FromRel.agda @@ -7,7 +7,10 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (REL; Rel; _⇒_) +open import Relation.Binary.Bundles using (Setoid; Preorder) +open import Relation.Binary.Structures using (IsPreorder) +open import Relation.Binary.Definitions using (_Respects_; Transitive) open Setoid using (Carrier) module Relation.Binary.Construct.FromRel diff --git a/src/Relation/Binary/Construct/Intersection.agda b/src/Relation/Binary/Construct/Intersection.agda index 17845536ca..0d26d675e6 100644 --- a/src/Relation/Binary/Construct/Intersection.agda +++ b/src/Relation/Binary/Construct/Intersection.agda @@ -12,7 +12,11 @@ open import Data.Product.Base open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]) open import Function.Base using (_∘_) open import Level using (Level; _⊔_) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; REL; _⇒_) +open import Relation.Binary.Structures + using (IsEquivalence; IsDecEquivalence; IsPreorder; IsPartialOrder; IsStrictPartialOrder) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive; Antisymmetric; Decidable; _Respects_; _Respectsˡ_; _Respectsʳ_; _Respects₂_; Minimum; Maximum; Irreflexive) open import Relation.Nullary.Decidable using (yes; no; _×-dec_) private diff --git a/src/Relation/Binary/Construct/NaturalOrder/Left.agda b/src/Relation/Binary/Construct/NaturalOrder/Left.agda index e0ab59e9ca..22a5031d27 100644 --- a/src/Relation/Binary/Construct/NaturalOrder/Left.agda +++ b/src/Relation/Binary/Construct/NaturalOrder/Left.agda @@ -10,7 +10,13 @@ open import Algebra.Core open import Data.Product.Base using (_,_; _×_) open import Data.Sum.Base using (inj₁; inj₂) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Bundles + using (Preorder; Poset; DecPoset; TotalOrder; DecTotalOrder) +open import Relation.Binary.Structures + using (IsEquivalence; IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder; IsDecTotalOrder) +open import Relation.Binary.Definitions + using (Symmetric; Transitive; Reflexive; Antisymmetric; Total; _Respectsʳ_; _Respectsˡ_; _Respects₂_; Decidable) open import Relation.Nullary.Negation using (¬_) import Relation.Binary.Reasoning.Setoid as EqReasoning open import Relation.Binary.Lattice using (Infimum) diff --git a/src/Relation/Binary/Construct/NaturalOrder/Right.agda b/src/Relation/Binary/Construct/NaturalOrder/Right.agda index 5278f0b116..80901f5939 100644 --- a/src/Relation/Binary/Construct/NaturalOrder/Right.agda +++ b/src/Relation/Binary/Construct/NaturalOrder/Right.agda @@ -10,7 +10,14 @@ open import Algebra.Core using (Op₂) open import Data.Product.Base using (_,_; _×_) open import Data.Sum.Base using (inj₁; inj₂) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Bundles + using (Preorder; Poset; DecPoset; TotalOrder; DecTotalOrder) +open import Relation.Binary.Structures + using (IsEquivalence; IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder; IsDecTotalOrder) +open import Relation.Binary.Definitions + using (Symmetric; Transitive; Reflexive; Antisymmetric; Total; _Respectsʳ_; _Respectsˡ_; _Respects₂_; Decidable) + open import Relation.Nullary.Negation using (¬_) import Relation.Binary.Reasoning.Setoid as EqReasoning diff --git a/src/Relation/Binary/Construct/NonStrictToStrict.agda b/src/Relation/Binary/Construct/NonStrictToStrict.agda index d9dd2c57ce..c2eb114004 100644 --- a/src/Relation/Binary/Construct/NonStrictToStrict.agda +++ b/src/Relation/Binary/Construct/NonStrictToStrict.agda @@ -6,7 +6,11 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Structures + using (IsPartialOrder; IsEquivalence; IsStrictPartialOrder; IsDecPartialOrder; IsDecStrictPartialOrder; IsTotalOrder; IsStrictTotalOrder; IsDecTotalOrder) +open import Relation.Binary.Definitions + using (Trichotomous; Antisymmetric; Symmetric; Total; Decidable; Irreflexive; Transitive; _Respectsʳ_; _Respectsˡ_; _Respects₂_; Trans; Asymmetric; tri≈; tri<; tri>) module Relation.Binary.Construct.NonStrictToStrict {a ℓ₁ ℓ₂} {A : Set a} (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) where diff --git a/src/Relation/Binary/Construct/On.agda b/src/Relation/Binary/Construct/On.agda index 122b0d6584..72959ac922 100644 --- a/src/Relation/Binary/Construct/On.agda +++ b/src/Relation/Binary/Construct/On.agda @@ -12,7 +12,13 @@ open import Data.Product.Base using (_,_) open import Function.Base using (_on_; _∘_) open import Induction.WellFounded using (WellFounded; Acc; acc) open import Level using (Level) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Bundles + using (Preorder; Setoid; DecSetoid; Poset; DecPoset; StrictPartialOrder; TotalOrder; DecTotalOrder; StrictTotalOrder) +open import Relation.Binary.Structures + using (IsEquivalence; IsDecEquivalence; IsPreorder; IsPartialOrder; IsDecPartialOrder; IsStrictPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictTotalOrder) +open import Relation.Binary.Definitions + using (Reflexive; Irreflexive; Symmetric; Transitive; Antisymmetric; Asymmetric; Decidable; Total; Trichotomous; _Respects_; _Respects₂_) private variable diff --git a/src/Relation/Binary/Construct/StrictToNonStrict.agda b/src/Relation/Binary/Construct/StrictToNonStrict.agda index 42c76fc80f..d17b6017fc 100644 --- a/src/Relation/Binary/Construct/StrictToNonStrict.agda +++ b/src/Relation/Binary/Construct/StrictToNonStrict.agda @@ -10,7 +10,11 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Structures + using (IsEquivalence; IsPreorder; IsStrictPartialOrder; IsPartialOrder; IsStrictTotalOrder; IsTotalOrder; IsDecTotalOrder) +open import Relation.Binary.Definitions + using (Transitive; Symmetric; Irreflexive; Antisymmetric; Trichotomous; Decidable; Trans; Total; _Respects₂_; _Respectsʳ_; _Respectsˡ_; tri<; tri≈; tri>) module Relation.Binary.Construct.StrictToNonStrict {a ℓ₁ ℓ₂} {A : Set a} diff --git a/src/Relation/Binary/Construct/Subst/Equality.agda b/src/Relation/Binary/Construct/Subst/Equality.agda index 24e465f9f0..95172b57ee 100644 --- a/src/Relation/Binary/Construct/Subst/Equality.agda +++ b/src/Relation/Binary/Construct/Subst/Equality.agda @@ -10,7 +10,9 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Data.Product.Base as Prod -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇔_) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive) module Relation.Binary.Construct.Subst.Equality {a ℓ₁ ℓ₂} {A : Set a} {≈₁ : Rel A ℓ₁} {≈₂ : Rel A ℓ₂} diff --git a/src/Relation/Binary/Construct/Union.agda b/src/Relation/Binary/Construct/Union.agda index 2b70ce8500..45f72c8190 100644 --- a/src/Relation/Binary/Construct/Union.agda +++ b/src/Relation/Binary/Construct/Union.agda @@ -12,7 +12,9 @@ open import Data.Product.Base open import Data.Sum.Base as Sum open import Function.Base using (_∘_) open import Level using (Level; _⊔_) -open import Relation.Binary +open import Relation.Binary.Core using (REL; Rel; _⇒_) +open import Relation.Binary.Definitions + using (Reflexive; Total; Minimum; Maximum; Symmetric; Irreflexive; Decidable; _Respects_; _Respectsˡ_; _Respectsʳ_; _Respects₂_) open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_) private diff --git a/src/Relation/Binary/HeterogeneousEquality.agda b/src/Relation/Binary/HeterogeneousEquality.agda index 3152bbf0cb..866628a71c 100644 --- a/src/Relation/Binary/HeterogeneousEquality.agda +++ b/src/Relation/Binary/HeterogeneousEquality.agda @@ -15,7 +15,10 @@ open import Function.Inverse using (Inverse) open import Level open import Relation.Nullary hiding (Irrelevant) open import Relation.Unary using (Pred) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; REL; _⇒_) +open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder) +open import Relation.Binary.Structures using (IsEquivalence; IsPreorder) +open import Relation.Binary.Definitions using (Substitutive; Irrelevant; Decidable; _Respects₂_) open import Relation.Binary.Consequences open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid) diff --git a/src/Relation/Binary/HeterogeneousEquality/Quotients.agda b/src/Relation/Binary/HeterogeneousEquality/Quotients.agda index fcdc1e97fc..18bc88002a 100644 --- a/src/Relation/Binary/HeterogeneousEquality/Quotients.agda +++ b/src/Relation/Binary/HeterogeneousEquality/Quotients.agda @@ -10,7 +10,7 @@ module Relation.Binary.HeterogeneousEquality.Quotients where open import Function.Base using (_$_; const; _∘_) open import Level hiding (lift) -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.HeterogeneousEquality open ≅-Reasoning diff --git a/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda b/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda index 2dbd39344a..5087b908fc 100644 --- a/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda +++ b/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda @@ -10,7 +10,8 @@ module Relation.Binary.HeterogeneousEquality.Quotients.Examples where open import Relation.Binary.HeterogeneousEquality.Quotients open import Level using (0ℓ) -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Structures using (IsEquivalence) open import Relation.Binary.HeterogeneousEquality hiding (isEquivalence) import Relation.Binary.PropositionalEquality.Core as ≡ open import Data.Nat.Base diff --git a/src/Relation/Binary/Indexed/Heterogeneous/Construct/At.agda b/src/Relation/Binary/Indexed/Heterogeneous/Construct/At.agda index f9c6dd8712..a05a9aa139 100644 --- a/src/Relation/Binary/Indexed/Heterogeneous/Construct/At.agda +++ b/src/Relation/Binary/Indexed/Heterogeneous/Construct/At.agda @@ -9,7 +9,8 @@ module Relation.Binary.Indexed.Heterogeneous.Construct.At where -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid; Preorder) +open import Relation.Binary.Structures using (IsEquivalence; IsPreorder) open import Relation.Binary.Indexed.Heterogeneous ------------------------------------------------------------------------ diff --git a/src/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.agda b/src/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.agda index 800d7e09f3..797e0587bc 100644 --- a/src/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.agda +++ b/src/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.agda @@ -9,7 +9,9 @@ module Relation.Binary.Indexed.Heterogeneous.Construct.Trivial {i} {I : Set i} where -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid; Preorder) +open import Relation.Binary.Structures using (IsEquivalence; IsPreorder) open import Relation.Binary.Indexed.Heterogeneous ------------------------------------------------------------------------ diff --git a/src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda b/src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda index 9899c200b3..14668cfa49 100644 --- a/src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda +++ b/src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda @@ -7,7 +7,9 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Level -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder) +open import Relation.Binary.Structures + using (IsEquivalence; IsDecEquivalence; IsPreorder) open import Relation.Binary.Indexed.Homogeneous module Relation.Binary.Indexed.Homogeneous.Construct.At where diff --git a/src/Relation/Binary/Lattice/Bundles.agda b/src/Relation/Binary/Lattice/Bundles.agda index ffe5dbf50d..7752c79676 100644 --- a/src/Relation/Binary/Lattice/Bundles.agda +++ b/src/Relation/Binary/Lattice/Bundles.agda @@ -13,7 +13,8 @@ module Relation.Binary.Lattice.Bundles where open import Algebra.Core open import Level using (suc; _⊔_) -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Poset; Setoid) open import Relation.Binary.Lattice.Structures ------------------------------------------------------------------------ diff --git a/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda b/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda index a86918081f..276e3a9705 100644 --- a/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda +++ b/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda @@ -18,7 +18,6 @@ open import Algebra.Ordered.Structures using (IsCommutativePomonoid) open import Algebra.Ordered.Bundles using (CommutativePomonoid) open import Data.Product.Base using (_,_) open import Function.Base using (_∘_; flip) -open import Relation.Binary open import Relation.Binary.Properties.Poset poset open import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice using (isPosemigroup; ∨-comm) diff --git a/src/Relation/Binary/Lattice/Properties/BoundedMeetSemilattice.agda b/src/Relation/Binary/Lattice/Properties/BoundedMeetSemilattice.agda index 622c8b6b0c..b0c945c39f 100644 --- a/src/Relation/Binary/Lattice/Properties/BoundedMeetSemilattice.agda +++ b/src/Relation/Binary/Lattice/Properties/BoundedMeetSemilattice.agda @@ -15,7 +15,6 @@ open BoundedMeetSemilattice M open import Algebra.Definitions _≈_ open import Function.Base using (_∘_; flip) -open import Relation.Binary open import Relation.Binary.Properties.Poset poset import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice as J diff --git a/src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda b/src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda index e3bd0170eb..f287e0a05d 100644 --- a/src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda +++ b/src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda @@ -15,7 +15,7 @@ open DistributiveLattice L hiding (refl) open import Algebra.Definitions _≈_ open import Data.Product.Base using (_,_) -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Reasoning.Setoid setoid open import Relation.Binary.Lattice.Properties.Lattice lattice open import Relation.Binary.Lattice.Properties.MeetSemilattice meetSemilattice diff --git a/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda b/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda index faa51120cd..c68467f577 100644 --- a/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda +++ b/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda @@ -20,7 +20,9 @@ open import Algebra.Ordered.Structures using (IsPosemigroup) open import Algebra.Ordered.Bundles using (Posemigroup) open import Data.Product.Base using (_,_) open import Function.Base using (_∘_; flip) -open import Relation.Binary +open import Relation.Binary.Core using (_Preserves₂_⟶_⟶_) +open import Relation.Binary.Structures using (IsDecPartialOrder) +open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.Properties.Poset poset open import Relation.Nullary using (¬_; yes; no) open import Relation.Nullary.Negation using (contraposition) diff --git a/src/Relation/Binary/Lattice/Properties/Lattice.agda b/src/Relation/Binary/Lattice/Properties/Lattice.agda index 633832a26c..fd95effaaf 100644 --- a/src/Relation/Binary/Lattice/Properties/Lattice.agda +++ b/src/Relation/Binary/Lattice/Properties/Lattice.agda @@ -18,7 +18,6 @@ import Algebra.Structures as Alg open import Algebra.Definitions _≈_ open import Data.Product.Base using (_,_) open import Function.Base using (flip) -open import Relation.Binary open import Relation.Binary.Properties.Poset poset import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice as J import Relation.Binary.Lattice.Properties.MeetSemilattice meetSemilattice as M diff --git a/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda b/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda index f072cb2199..a78d4fea6a 100644 --- a/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda +++ b/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda @@ -15,7 +15,8 @@ open MeetSemilattice M open import Algebra.Definitions _≈_ open import Function.Base using (flip) -open import Relation.Binary +open import Relation.Binary.Structures using (IsDecPartialOrder) +open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.Properties.Poset poset import Relation.Binary.Lattice.Properties.JoinSemilattice as J diff --git a/src/Relation/Binary/Lattice/Structures.agda b/src/Relation/Binary/Lattice/Structures.agda index 07dbfad6a5..77d9604167 100644 --- a/src/Relation/Binary/Lattice/Structures.agda +++ b/src/Relation/Binary/Lattice/Structures.agda @@ -9,7 +9,9 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Structures using (IsPartialOrder) +open import Relation.Binary.Definitions using (Minimum; Maximum) module Relation.Binary.Lattice.Structures {a ℓ₁ ℓ₂} {A : Set a} diff --git a/src/Relation/Binary/Morphism/Construct/Composition.agda b/src/Relation/Binary/Morphism/Construct/Composition.agda index 5f6fe9bf32..d86860b6bb 100644 --- a/src/Relation/Binary/Morphism/Construct/Composition.agda +++ b/src/Relation/Binary/Morphism/Construct/Composition.agda @@ -9,7 +9,9 @@ open import Function.Base using (_∘_) open import Function.Construct.Composition using (surjective) open import Level using (Level) -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid; Preorder; Poset) +open import Relation.Binary.Definitions using (Transitive) open import Relation.Binary.Morphism.Bundles open import Relation.Binary.Morphism.Structures diff --git a/src/Relation/Binary/Morphism/Construct/Constant.agda b/src/Relation/Binary/Morphism/Construct/Constant.agda index d31c274bfa..f3a1bd2212 100644 --- a/src/Relation/Binary/Morphism/Construct/Constant.agda +++ b/src/Relation/Binary/Morphism/Construct/Constant.agda @@ -8,7 +8,9 @@ open import Function.Base using (const) open import Level using (Level) -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid; Preorder) +open import Relation.Binary.Definitions using (Reflexive) open import Relation.Binary.Morphism.Structures open import Relation.Binary.Morphism.Bundles diff --git a/src/Relation/Binary/Morphism/Construct/Identity.agda b/src/Relation/Binary/Morphism/Construct/Identity.agda index 302881b4aa..2a11d642ad 100644 --- a/src/Relation/Binary/Morphism/Construct/Identity.agda +++ b/src/Relation/Binary/Morphism/Construct/Identity.agda @@ -10,7 +10,9 @@ open import Data.Product.Base using (_,_) open import Function.Base using (id) import Function.Construct.Identity as Id open import Level using (Level) -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid; Preorder; Poset) +open import Relation.Binary.Definitions using (Reflexive) open import Relation.Binary.Morphism.Structures open import Relation.Binary.Morphism.Bundles diff --git a/src/Relation/Binary/Morphism/OrderMonomorphism.agda b/src/Relation/Binary/Morphism/OrderMonomorphism.agda index 3d788184c2..49d7c4e2e3 100644 --- a/src/Relation/Binary/Morphism/OrderMonomorphism.agda +++ b/src/Relation/Binary/Morphism/OrderMonomorphism.agda @@ -12,7 +12,11 @@ open import Algebra.Morphism.Definitions open import Function.Base open import Data.Product.Base using (_,_; map) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Structures + using (IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder) +open import Relation.Binary.Definitions + using (Irreflexive; Antisymmetric; Trichotomous; tri<; tri≈; tri>; _Respectsˡ_; _Respectsʳ_; _Respects₂_) open import Relation.Binary.Morphism import Relation.Binary.Morphism.RelMonomorphism as RawRelation diff --git a/src/Relation/Binary/Morphism/RelMonomorphism.agda b/src/Relation/Binary/Morphism/RelMonomorphism.agda index e500fa4368..73a873fae5 100644 --- a/src/Relation/Binary/Morphism/RelMonomorphism.agda +++ b/src/Relation/Binary/Morphism/RelMonomorphism.agda @@ -10,7 +10,10 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Function.Base -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive; Total; Asymmetric; Decidable) open import Relation.Binary.Morphism module Relation.Binary.Morphism.RelMonomorphism diff --git a/src/Relation/Binary/OrderMorphism.agda b/src/Relation/Binary/OrderMorphism.agda index fbf3781c78..d516d5342e 100644 --- a/src/Relation/Binary/OrderMorphism.agda +++ b/src/Relation/Binary/OrderMorphism.agda @@ -14,7 +14,8 @@ module Relation.Binary.OrderMorphism where Use Relation.Binary.Reasoning.Morphism instead." #-} -open import Relation.Binary +open import Relation.Binary.Core using (_=[_]⇒_) +open import Relation.Binary.Bundles using (Poset; DecTotalOrder) open Poset import Function.Base as F open import Level diff --git a/src/Relation/Binary/Properties/DecTotalOrder.agda b/src/Relation/Binary/Properties/DecTotalOrder.agda index 386bb2189b..2923a0d047 100644 --- a/src/Relation/Binary/Properties/DecTotalOrder.agda +++ b/src/Relation/Binary/Properties/DecTotalOrder.agda @@ -6,7 +6,10 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Structures + using (IsDecTotalOrder; IsStrictTotalOrder) +open import Relation.Binary.Bundles + using (DecTotalOrder; StrictTotalOrder) module Relation.Binary.Properties.DecTotalOrder {d₁ d₂ d₃} (DT : DecTotalOrder d₁ d₂ d₃) where diff --git a/src/Relation/Binary/Properties/HeytingAlgebra.agda b/src/Relation/Binary/Properties/HeytingAlgebra.agda index 8786792e78..87cb01899d 100644 --- a/src/Relation/Binary/Properties/HeytingAlgebra.agda +++ b/src/Relation/Binary/Properties/HeytingAlgebra.agda @@ -18,7 +18,7 @@ open import Algebra.Definitions _≈_ open import Data.Product.Base using (_,_) open import Function.Base using (_$_; flip; _∘_) open import Level using (_⊔_) -open import Relation.Binary +open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_) import Relation.Binary.Reasoning.PartialOrder as POR open import Relation.Binary.Lattice.Properties.MeetSemilattice meetSemilattice open import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice diff --git a/src/Relation/Binary/Properties/Poset.agda b/src/Relation/Binary/Properties/Poset.agda index 5d1d6e9fe8..add0e20b28 100644 --- a/src/Relation/Binary/Properties/Poset.agda +++ b/src/Relation/Binary/Properties/Poset.agda @@ -7,7 +7,12 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Function.Base using (flip; _∘_) -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _Preserves_⟶_) +open import Relation.Binary.Bundles using (Poset; StrictPartialOrder) +open import Relation.Binary.Structures + using (IsPartialOrder; IsStrictPartialOrder; IsDecPartialOrder) +open import Relation.Binary.Definitions + using (_Respectsˡ_; _Respectsʳ_; Decidable) import Relation.Binary.Consequences as Consequences open import Relation.Nullary using (¬_; yes; no) open import Relation.Nullary.Negation using (contradiction) diff --git a/src/Relation/Binary/Properties/Preorder.agda b/src/Relation/Binary/Properties/Preorder.agda index e09bd0f3f1..dc9bd2913b 100644 --- a/src/Relation/Binary/Properties/Preorder.agda +++ b/src/Relation/Binary/Properties/Preorder.agda @@ -6,7 +6,8 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (Preorder; Setoid) +open import Relation.Binary.Structures using (IsPreorder) module Relation.Binary.Properties.Preorder {p₁ p₂ p₃} (P : Preorder p₁ p₂ p₃) where diff --git a/src/Relation/Binary/Properties/Setoid.agda b/src/Relation/Binary/Properties/Setoid.agda index 050177c629..968256077f 100644 --- a/src/Relation/Binary/Properties/Setoid.agda +++ b/src/Relation/Binary/Properties/Setoid.agda @@ -10,7 +10,10 @@ open import Data.Product.Base using (_,_) open import Function.Base using (_∘_; id; _$_; flip) open import Relation.Nullary.Negation.Core using (¬_) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid; Preorder; Poset) +open import Relation.Binary.Definitions + using (Symmetric; _Respectsˡ_; _Respectsʳ_; _Respects₂_) +open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder) module Relation.Binary.Properties.Setoid {a ℓ} (S : Setoid a ℓ) where diff --git a/src/Relation/Binary/Properties/StrictPartialOrder.agda b/src/Relation/Binary/Properties/StrictPartialOrder.agda index 7b6043af77..7420a2e24f 100644 --- a/src/Relation/Binary/Properties/StrictPartialOrder.agda +++ b/src/Relation/Binary/Properties/StrictPartialOrder.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (StrictPartialOrder; Poset) module Relation.Binary.Properties.StrictPartialOrder {s₁ s₂ s₃} (SPO : StrictPartialOrder s₁ s₂ s₃) where @@ -14,7 +14,7 @@ module Relation.Binary.Properties.StrictPartialOrder import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd import Relation.Binary.Construct.StrictToNonStrict -open Relation.Binary.StrictPartialOrder SPO +open StrictPartialOrder SPO ------------------------------------------------------------------------ -- The inverse relation is also a strict partial order. diff --git a/src/Relation/Binary/Properties/StrictTotalOrder.agda b/src/Relation/Binary/Properties/StrictTotalOrder.agda index ab82e8ea54..f8b0062474 100644 --- a/src/Relation/Binary/Properties/StrictTotalOrder.agda +++ b/src/Relation/Binary/Properties/StrictTotalOrder.agda @@ -6,13 +6,13 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (StrictTotalOrder; DecTotalOrder) module Relation.Binary.Properties.StrictTotalOrder {s₁ s₂ s₃} (STO : StrictTotalOrder s₁ s₂ s₃) where -open Relation.Binary.StrictTotalOrder STO +open StrictTotalOrder STO open import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_ import Relation.Binary.Properties.StrictPartialOrder as SPO open import Relation.Binary.Consequences diff --git a/src/Relation/Binary/Properties/TotalOrder.agda b/src/Relation/Binary/Properties/TotalOrder.agda index 18e7095985..540de19905 100644 --- a/src/Relation/Binary/Properties/TotalOrder.agda +++ b/src/Relation/Binary/Properties/TotalOrder.agda @@ -6,7 +6,9 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (TotalOrder; DecTotalOrder) +open import Relation.Binary.Definitions using (Decidable) +open import Relation.Binary.Structures using (IsTotalOrder) module Relation.Binary.Properties.TotalOrder {t₁ t₂ t₃} (T : TotalOrder t₁ t₂ t₃) where diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda index 37c891312b..62bd7ca246 100644 --- a/src/Relation/Binary/PropositionalEquality.agda +++ b/src/Relation/Binary/PropositionalEquality.agda @@ -16,7 +16,8 @@ open import Level using (Level; _⊔_) open import Data.Product.Base using (∃) open import Relation.Nullary.Decidable using (yes; no; dec-yes-irr; dec-no) -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid) import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial diff --git a/src/Relation/Binary/PropositionalEquality/Properties.agda b/src/Relation/Binary/PropositionalEquality/Properties.agda index 48bb2a257e..9515b77700 100644 --- a/src/Relation/Binary/PropositionalEquality/Properties.agda +++ b/src/Relation/Binary/PropositionalEquality/Properties.agda @@ -14,7 +14,12 @@ module Relation.Binary.PropositionalEquality.Properties where open import Function.Base using (id; _∘_) open import Level using (Level) -open import Relation.Binary +open import Relation.Binary.Bundles + using (Setoid; DecSetoid; Preorder; Poset) +open import Relation.Binary.Structures + using (IsEquivalence; IsDecEquivalence; IsPreorder; IsPartialOrder) +open import Relation.Binary.Definitions + using (Decidable; DecidableEquality) import Relation.Binary.Properties.Setoid as Setoid open import Relation.Binary.PropositionalEquality.Core open import Relation.Unary using (Pred) diff --git a/src/Relation/Binary/PropositionalEquality/WithK.agda b/src/Relation/Binary/PropositionalEquality/WithK.agda index d14ec1d9f3..db49b97b2c 100644 --- a/src/Relation/Binary/PropositionalEquality/WithK.agda +++ b/src/Relation/Binary/PropositionalEquality/WithK.agda @@ -10,7 +10,7 @@ module Relation.Binary.PropositionalEquality.WithK where open import Axiom.UniquenessOfIdentityProofs.WithK -open import Relation.Binary +open import Relation.Binary.Definitions using (Irrelevant) open import Relation.Binary.PropositionalEquality.Core ------------------------------------------------------------------------ diff --git a/src/Relation/Binary/Reasoning/Base/Apartness.agda b/src/Relation/Binary/Reasoning/Base/Apartness.agda index 7a52568664..6e0e239a02 100644 --- a/src/Relation/Binary/Reasoning/Base/Apartness.agda +++ b/src/Relation/Binary/Reasoning/Base/Apartness.agda @@ -7,7 +7,9 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Binary.Definitions using (Transitive; Symmetric; Trans) module Relation.Binary.Reasoning.Base.Apartness {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_#_ : Rel A ℓ₂} diff --git a/src/Relation/Binary/Reasoning/Base/Double.agda b/src/Relation/Binary/Reasoning/Base/Double.agda index 07761c5144..aa61052b0c 100644 --- a/src/Relation/Binary/Reasoning/Base/Double.agda +++ b/src/Relation/Binary/Reasoning/Base/Double.agda @@ -10,7 +10,8 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Structures using (IsPreorder) module Relation.Binary.Reasoning.Base.Double {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_∼_ : Rel A ℓ₂} (isPreorder : IsPreorder _≈_ _∼_) diff --git a/src/Relation/Binary/Reasoning/Base/Single.agda b/src/Relation/Binary/Reasoning/Base/Single.agda index 97da6b06b8..43b553c7d1 100644 --- a/src/Relation/Binary/Reasoning/Base/Single.agda +++ b/src/Relation/Binary/Reasoning/Base/Single.agda @@ -6,7 +6,8 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Definitions using (Reflexive; Transitive) module Relation.Binary.Reasoning.Base.Single {a ℓ} {A : Set a} (_∼_ : Rel A ℓ) diff --git a/src/Relation/Binary/Reasoning/Base/Triple.agda b/src/Relation/Binary/Reasoning/Base/Triple.agda index c18aa9bf94..fe931722da 100644 --- a/src/Relation/Binary/Reasoning/Base/Triple.agda +++ b/src/Relation/Binary/Reasoning/Base/Triple.agda @@ -10,7 +10,10 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Structures using (IsPreorder) +open import Relation.Binary.Definitions + using (Transitive; _Respects₂_; Trans) module Relation.Binary.Reasoning.Base.Triple {a ℓ₁ ℓ₂ ℓ₃} {A : Set a} {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} {_<_ : Rel A ℓ₃} diff --git a/src/Relation/Binary/Reasoning/MultiSetoid.agda b/src/Relation/Binary/Reasoning/MultiSetoid.agda index 7737e6a779..194e7ae410 100644 --- a/src/Relation/Binary/Reasoning/MultiSetoid.agda +++ b/src/Relation/Binary/Reasoning/MultiSetoid.agda @@ -28,7 +28,7 @@ module Relation.Binary.Reasoning.MultiSetoid where open import Function.Base using (flip) open import Level using (_⊔_) -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) import Relation.Binary.Reasoning.Setoid as EqR diff --git a/src/Relation/Binary/Reasoning/PartialOrder.agda b/src/Relation/Binary/Reasoning/PartialOrder.agda index fbf1bef25f..80102d77f2 100644 --- a/src/Relation/Binary/Reasoning/PartialOrder.agda +++ b/src/Relation/Binary/Reasoning/PartialOrder.agda @@ -39,7 +39,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (Poset) module Relation.Binary.Reasoning.PartialOrder {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where diff --git a/src/Relation/Binary/Reasoning/PartialSetoid.agda b/src/Relation/Binary/Reasoning/PartialSetoid.agda index 78f7c065d5..e679474016 100644 --- a/src/Relation/Binary/Reasoning/PartialSetoid.agda +++ b/src/Relation/Binary/Reasoning/PartialSetoid.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (PartialSetoid) module Relation.Binary.Reasoning.PartialSetoid {s₁ s₂} (S : PartialSetoid s₁ s₂) where diff --git a/src/Relation/Binary/Reasoning/Preorder.agda b/src/Relation/Binary/Reasoning/Preorder.agda index 599be2f37b..933e8f0a45 100644 --- a/src/Relation/Binary/Reasoning/Preorder.agda +++ b/src/Relation/Binary/Reasoning/Preorder.agda @@ -23,7 +23,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (Preorder) module Relation.Binary.Reasoning.Preorder {p₁ p₂ p₃} (P : Preorder p₁ p₂ p₃) where diff --git a/src/Relation/Binary/Reasoning/Setoid.agda b/src/Relation/Binary/Reasoning/Setoid.agda index 77b1879db1..5b731767eb 100644 --- a/src/Relation/Binary/Reasoning/Setoid.agda +++ b/src/Relation/Binary/Reasoning/Setoid.agda @@ -20,7 +20,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) module Relation.Binary.Reasoning.Setoid {s₁ s₂} (S : Setoid s₁ s₂) where diff --git a/src/Relation/Binary/Reasoning/StrictPartialOrder.agda b/src/Relation/Binary/Reasoning/StrictPartialOrder.agda index 2e18d1fab7..8e2b7a3a3d 100644 --- a/src/Relation/Binary/Reasoning/StrictPartialOrder.agda +++ b/src/Relation/Binary/Reasoning/StrictPartialOrder.agda @@ -40,7 +40,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (StrictPartialOrder) module Relation.Binary.Reasoning.StrictPartialOrder {p₁ p₂ p₃} (S : StrictPartialOrder p₁ p₂ p₃) where diff --git a/src/Relation/Binary/Reflection.agda b/src/Relation/Binary/Reflection.agda index 20e2054cfc..a21288100a 100644 --- a/src/Relation/Binary/Reflection.agda +++ b/src/Relation/Binary/Reflection.agda @@ -13,7 +13,7 @@ open import Data.Vec.Base as Vec using (Vec; allFin) open import Function.Base using (id; _⟨_⟩_) open import Function.Bundles using (module Equivalence) open import Level using (Level) -open import Relation.Binary +open import Relation.Binary.Bundles using (Setoid) import Relation.Binary.PropositionalEquality.Core as P -- Think of the parameters as follows: diff --git a/src/Relation/Unary/Closure/Base.agda b/src/Relation/Unary/Closure/Base.agda index 4d80a5af1d..52ecac9ecf 100644 --- a/src/Relation/Unary/Closure/Base.agda +++ b/src/Relation/Unary/Closure/Base.agda @@ -6,7 +6,8 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Definitions using (Transitive; Reflexive) module Relation.Unary.Closure.Base {a b} {A : Set a} (R : Rel A b) where diff --git a/src/Relation/Unary/Closure/Preorder.agda b/src/Relation/Unary/Closure/Preorder.agda index 8c261b0283..374669aa30 100644 --- a/src/Relation/Unary/Closure/Preorder.agda +++ b/src/Relation/Unary/Closure/Preorder.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (Preorder) module Relation.Unary.Closure.Preorder {a r e} (P : Preorder a e r) where diff --git a/src/Relation/Unary/Closure/StrictPartialOrder.agda b/src/Relation/Unary/Closure/StrictPartialOrder.agda index 889977fd02..81d5fb48f1 100644 --- a/src/Relation/Unary/Closure/StrictPartialOrder.agda +++ b/src/Relation/Unary/Closure/StrictPartialOrder.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +open import Relation.Binary.Bundles using (StrictPartialOrder) module Relation.Unary.Closure.StrictPartialOrder {a r e} (P : StrictPartialOrder a e r) where diff --git a/tests/system/directory/Main.agda b/tests/system/directory/Main.agda index 0cde09f459..dabcdd433c 100644 --- a/tests/system/directory/Main.agda +++ b/tests/system/directory/Main.agda @@ -10,7 +10,7 @@ import Data.String.Properties as Stringₚ open import IO open import Function.Base using (_$_) -open import Relation.Binary +open import Relation.Binary.Bundles using (DecTotalOrder) import Relation.Binary.Construct.On as On open import System.Directory