[DRY] Refactor Data.List.Relation.Binary.Equality.Setoid exports (#…

…2490) * refactor `Data.List.Relation.Binary.Equality.DecSetoid` * refactor `Data.List.Relation.Binary.Equality.Setoid` * oops! get import/export of `setoid` correctt * knock-on: tighten `impport`s
agda · Oct 7, 2024 · 22bfd05 · 22bfd05
1 parent 7e94c15
commit 22bfd05
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 37 deletions.
diff --git a/src/Data/List/Relation/Binary/Equality/DecSetoid.agda b/src/Data/List/Relation/Binary/Equality/DecSetoid.agda
@@ -7,33 +7,25 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 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
 
 import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
-import Data.List.Relation.Binary.Pointwise as PW
-open import Level
-open import Relation.Binary.Definitions using (Decidable)
-open DecSetoid DS
-
-------------------------------------------------------------------------
--- Make all definitions from setoid equality available
-
-open SetoidEquality setoid public
+open import Data.List.Relation.Binary.Pointwise using (decSetoid)
+open DecSetoid DS using (setoid)
 
 ------------------------------------------------------------------------
 -- Additional properties
 
-infix 4 _≋?_
+≋-decSetoid : DecSetoid _ _
+≋-decSetoid = decSetoid DS
 
-_≋?_ : Decidable _≋_
-_≋?_ = PW.decidable _≟_
+open DecSetoid ≋-decSetoid public
+  using ()
+  renaming (isDecEquivalence to ≋-isDecEquivalence; _≟_ to _≋?_)
 
-≋-isDecEquivalence : IsDecEquivalence _≋_
-≋-isDecEquivalence = PW.isDecEquivalence isDecEquivalence
+------------------------------------------------------------------------
+-- Make all definitions from setoid equality available
 
-≋-decSetoid : DecSetoid a (a ⊔ ℓ)
-≋-decSetoid = PW.decSetoid DS
+open SetoidEquality setoid public
diff --git a/src/Data/List/Relation/Binary/Equality/Setoid.agda b/src/Data/List/Relation/Binary/Equality/Setoid.agda
@@ -48,24 +48,17 @@ open PW public
 -- Relational properties
 ------------------------------------------------------------------------
 
-≋-refl : Reflexive _≋_
-≋-refl = PW.refl refl
-
-≋-reflexive : _≡_ ⇒ _≋_
-≋-reflexive ≡.refl = ≋-refl
-
-≋-sym : Symmetric _≋_
-≋-sym = PW.symmetric sym
-
-≋-trans : Transitive _≋_
-≋-trans = PW.transitive trans
-
-≋-isEquivalence : IsEquivalence _≋_
-≋-isEquivalence = PW.isEquivalence isEquivalence
-
 ≋-setoid : Setoid _ _
 ≋-setoid = PW.setoid S
 
+open Setoid ≋-setoid public
+  using ()
+  renaming ( refl to ≋-refl
+           ; reflexive to ≋-reflexive
+           ; sym to ≋-sym
+           ; trans to ≋-trans
+           ; isEquivalence to ≋-isEquivalence)
+
 ------------------------------------------------------------------------
 -- Relationships to predicates
 ------------------------------------------------------------------------

diff --git a/src/Data/List/Relation/Binary/Subset/DecSetoid.agda b/src/Data/List/Relation/Binary/Subset/DecSetoid.agda
@@ -14,10 +14,10 @@ open import Function.Base using (_∘_)
 open import Data.List.Base using ([]; _∷_)
 open import Data.List.Relation.Unary.Any using (here; there; map)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary using (yes; no)
-open DecSetoid S
-open import Data.List.Relation.Binary.Equality.DecSetoid S
-open import Data.List.Membership.DecSetoid S
+open import Relation.Nullary.Decidable.Core using (yes; no)
+
+open DecSetoid S using (setoid; refl; trans)
+open import Data.List.Membership.DecSetoid S using (_∈?_)
 
 -- Re-export definitions
 open import Data.List.Relation.Binary.Subset.Setoid setoid public