Final Relation.Binary simplifications (#2068)

agda · Oct 13, 2023 · c7f5fc7 · c7f5fc7
1 parent 45ec837
commit c7f5fc7
Show file tree

Hide file tree

Showing 161 changed files with 513 additions and 169 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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