From 577008ed887eb9d33be6eb3b216ecfdd852667ff Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Wed, 11 Sep 2024 12:13:12 +0100
Subject: [PATCH] refactor: simplify definitions/exports (#2480)

---
 .../List/Relation/Unary/Unique/Propositional.agda    |  4 ++--
 src/Data/List/Relation/Unary/Unique/Setoid.agda      | 12 +++---------
 2 files changed, 5 insertions(+), 11 deletions(-)

diff --git a/src/Data/List/Relation/Unary/Unique/Propositional.agda b/src/Data/List/Relation/Unary/Unique/Propositional.agda
index 2c32f0da46..2fc10ca752 100644
--- 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
index 041b68ec9b..abad6b3e02 100644
--- 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)