refactor: simplify definitions/exports (#2480)

agda · Sep 11, 2024 · 577008e · 577008e
1 parent 9a5ec9f
commit 577008e
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 11 deletions.
diff --git a/src/Data/List/Relation/Unary/Unique/Propositional.agda b/src/Data/List/Relation/Unary/Unique/Propositional.agda
@@ -9,9 +9,9 @@
 module Data.List.Relation.Unary.Unique.Propositional {a} {A : Set a} where
 
 open import Relation.Binary.PropositionalEquality.Properties using (setoid)
-open import Data.List.Relation.Unary.Unique.Setoid as SetoidUnique
 
 ------------------------------------------------------------------------
 -- Re-export the contents of setoid uniqueness
 
-open SetoidUnique (setoid A) public
+open import Data.List.Relation.Unary.Unique.Setoid (setoid A) public
+
diff --git a/src/Data/List/Relation/Unary/Unique/Setoid.agda b/src/Data/List/Relation/Unary/Unique/Setoid.agda
@@ -6,23 +6,17 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Nullary.Negation using (¬_)
 
 module Data.List.Relation.Unary.Unique.Setoid {a ℓ} (S : Setoid a ℓ) where
 
-open Setoid S renaming (Carrier to A)
+open Setoid S using (_≉_)
 
 ------------------------------------------------------------------------
 -- Definition
 
-private
-  Distinct : Rel A ℓ
-  Distinct x y = ¬ (x ≈ y)
-
-open import Data.List.Relation.Unary.AllPairs.Core Distinct public
+open import Data.List.Relation.Unary.AllPairs.Core _≉_ public
   renaming (AllPairs to Unique)
 
-open import Data.List.Relation.Unary.AllPairs {R = Distinct} public
+open import Data.List.Relation.Unary.AllPairs {R = _≉_} public
   using (head; tail)