From 23af80f3f4dab6a913b0cfa2a1e6418e9a85b205 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 10 Jul 2026 13:28:52 +0100
Subject: [PATCH 1/6] [ refactor ] add `Relation.Unary.Unique`

---
 CHANGELOG.md            |  6 ++++++
 src/Data/Product.agda   |  5 +++--
 src/Relation/Unary.agda | 10 ++++++++++
 3 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1e72ea222c..433bfd5704 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -427,3 +427,9 @@ Additions to existing modules
     StarRightDestructive  : ∀ (_+_ _*_ : Fun₂ A) (_⋆ : Fun₁ A) → Set _
     StarDestructive       : ∀ (_+_ _*_ : Fun₂ A) (_⋆ : Fun₁ A) → Set _
   ```
+
+* In `Relation.Unary`:
+  ```agda
+  Unique         : (A → A → Set ℓ₁) (P : Pred A ℓ₂) → Pred A _
+  UniqueSuchThat : (A → A → Set ℓ₁) (P : Pred A ℓ₂) → Pred A _
+  ```
diff --git a/src/Data/Product.agda b/src/Data/Product.agda
index 9e032765c4..7c8d21e7c2 100644
--- a/src/Data/Product.agda
+++ b/src/Data/Product.agda
@@ -10,6 +10,7 @@ module Data.Product where
 
 open import Level using (Level; _⊔_)
 open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Unary using (UniqueSuchThat)
 
 private
   variable
@@ -50,8 +51,8 @@ zipWith _∙_ _∘_ _*_ (a , p) (b , q) = (a ∙ b) * (p ∘ q)
 
 -- Unique existence (parametrised by an underlying equality).
 
-∃! : {A : Set a} → (A → A → Set ℓ) → (A → Set b) → Set (a ⊔ b ⊔ ℓ)
-∃! _≈_ B = ∃ λ x → B x × (∀ {y} → B y → x ≈ y)
+∃! : ∀ {A : Set a} → (A → A → Set ℓ) → (A → Set p) → Set (a ⊔ p ⊔ ℓ)
+∃! _≈_ P = ∃ (UniqueSuchThat _≈_ P)
 
 -- Syntax
 
diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 1146fef6cb..8042560bda 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -198,6 +198,16 @@ Decidable P = ∀ x → Dec (P x)
 ⌊_⌋ : {P : Pred A ℓ} → Decidable P → Pred A ℓ
 ⌊ P? ⌋ a = Lift _ (True (P? a))
 
+-- Uniqueness
+
+module _ (_≈_ : A → A → Set ℓ₁) (P : Pred A ℓ₂) where
+
+  Unique : Pred A _
+  Unique x = ∀ {z} → P z → z ≈ x
+
+  UniqueSuchThat : Pred A _
+  UniqueSuchThat x = P x × Unique x
+
 ------------------------------------------------------------------------
 -- Operations on sets
 

From 668e74fc764d9e5f30d9e9832b1e3d495610d8c3 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 10 Jul 2026 15:06:27 +0100
Subject: [PATCH 2/6] add: `UniqueGivenThat`

---
 src/Relation/Unary.agda | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 8042560bda..af787e76f4 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -205,6 +205,9 @@ module _ (_≈_ : A → A → Set ℓ₁) (P : Pred A ℓ₂) where
   Unique : Pred A _
   Unique x = ∀ {z} → P z → z ≈ x
 
+  UniqueGivenThat : Pred A _
+  UniqueGivenThat x = P x → Unique x
+
   UniqueSuchThat : Pred A _
   UniqueSuchThat x = P x × Unique x
 

From f3dcf945b2e97e5e86ccc2cbdcf1339c52d0c54d Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 10 Jul 2026 15:08:13 +0100
Subject: [PATCH 3/6] add: `UniqueGivenThat`

---
 CHANGELOG.md | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 433bfd5704..5e1f9cff8e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -430,6 +430,7 @@ Additions to existing modules
 
 * In `Relation.Unary`:
   ```agda
-  Unique         : (A → A → Set ℓ₁) (P : Pred A ℓ₂) → Pred A _
-  UniqueSuchThat : (A → A → Set ℓ₁) (P : Pred A ℓ₂) → Pred A _
+  Unique          : (A → A → Set ℓ₁) (P : Pred A ℓ₂) → Pred A _
+  UniqueGivenThat : (A → A → Set ℓ₁) (P : Pred A ℓ₂) → Pred A _
+  UniqueSuchThat  : (A → A → Set ℓ₁) (P : Pred A ℓ₂) → Pred A _
   ```

From 341a4bba0f1a3da487e2861beef719ecbe1b4ef7 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 10 Jul 2026 15:09:02 +0100
Subject: [PATCH 4/6] use: new definitions for `Levenshtein` edit distance

---
 .../List/Relation/Binary/Distance/Levenshtein/Core.agda   | 3 ++-
 .../Relation/Binary/Distance/Levenshtein/Dist/Setoid.agda | 6 +++---
 .../Relation/Binary/Distance/Levenshtein/Edit/Setoid.agda | 8 ++++----
 3 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Distance/Levenshtein/Core.agda b/src/Data/List/Relation/Binary/Distance/Levenshtein/Core.agda
index 5bd8bac2a9..f0e84e078a 100644
--- a/src/Data/List/Relation/Binary/Distance/Levenshtein/Core.agda
+++ b/src/Data/List/Relation/Binary/Distance/Levenshtein/Core.agda
@@ -16,10 +16,11 @@ There are no backwards compatibility guarantees whatsoever on its content."
 open import Data.Nat.Base using (ℕ; _≤_; _+_)
 open import Level using (_⊔_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Unary using (UniqueGivenThat)
 
 -- These definitions surely need to go somewhere else
 Unique : ∀ {a ℓ} {A : Set a} (dist : A → A → ℕ → Set ℓ) → Set (a ⊔ ℓ)
-Unique dist = ∀ x y k l → dist x y k → dist x y l → k ≡ l
+Unique dist = ∀ x y k → UniqueGivenThat _≡_ (dist x y) k
 
 Triangle : ∀ {a ℓ} {A : Set a} (dist : A → A → ℕ → Set ℓ) → Set (a ⊔ ℓ)
 Triangle dist = ∀ x y z k l m → dist x y k → dist y z l → dist x z m → m ≤ k + l
diff --git a/src/Data/List/Relation/Binary/Distance/Levenshtein/Dist/Setoid.agda b/src/Data/List/Relation/Binary/Distance/Levenshtein/Dist/Setoid.agda
index c2e5e1c0f5..ef88076849 100644
--- a/src/Data/List/Relation/Binary/Distance/Levenshtein/Dist/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Distance/Levenshtein/Dist/Setoid.agda
@@ -83,11 +83,11 @@ symmetric (d , m) .edit = Edit.symmetric d
 symmetric (d , m) .minimal = λ c d′ → m c (Edit.symmetric d′)
 
 -- The relation is indeed unique
-unique : Unique {A = List A} Dist
-unique _ _ _ _ (dk , mk) (dl , ml) = ≤-antisym (mk _ dl) (ml _ dk)
+unique : Unique Dist
+unique _ _ _ (dk , mk) (dl , ml) = ≤-antisym (ml _ dk) (mk _ dl)
 
 -- And it respects the triangle inequality
-triangle : Triangle {A = List A} Dist
+triangle : Triangle Dist
 triangle _ _ _ _ _ _ (dlm , _) (dmr , _) (dlr , mlr)
   = let (m , dlr′ , m≤) = Edit.compose dlm dmr in
   ≤-trans (mlr m dlr′) m≤
diff --git a/src/Data/List/Relation/Binary/Distance/Levenshtein/Edit/Setoid.agda b/src/Data/List/Relation/Binary/Distance/Levenshtein/Edit/Setoid.agda
index 94f0411fe5..ed277f646c 100644
--- a/src/Data/List/Relation/Binary/Distance/Levenshtein/Edit/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Distance/Levenshtein/Edit/Setoid.agda
@@ -86,14 +86,14 @@ open import Data.List.Relation.Binary.Distance.Levenshtein.Core
 module _ (x : A) where
 
   -- the "distance" defined by the relation is not unique
-  not-unique : ¬ Unique {A = List A} Edit
+  not-unique : ¬ Unique Edit
   not-unique unique =
     let xs = x ∷ []
-        hyp = unique xs xs 0 1 reflexive (swap done)
-    in 0≢1+n hyp
+        hyp = unique xs xs 0 reflexive (swap done)
+    in 0≢1+n (sym hyp)
 
   -- the relation does not satisfy the triangle inequality
-  not-triangle : ¬ (Triangle {A = List A} Edit)
+  not-triangle : ¬ Triangle Edit
   not-triangle triangle =
       let xs = x ∷ []
           hyp = triangle xs xs xs 0 0 1 reflexive reflexive (swap done)

From bb5c900ad2ba202b5bcfd9bb60e1afb36e5eeb1c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 12 Jul 2026 14:12:23 +0100
Subject: [PATCH 5/6] add: uniqueness lemma

---
 CHANGELOG.md                       |  5 +++++
 src/Relation/Unary/Properties.agda | 12 +++++++++++-
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5e1f9cff8e..2f7bc87270 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -434,3 +434,8 @@ Additions to existing modules
   UniqueGivenThat : (A → A → Set ℓ₁) (P : Pred A ℓ₂) → Pred A _
   UniqueSuchThat  : (A → A → Set ℓ₁) (P : Pred A ℓ₂) → Pred A _
   ```
+
+* In `Relation.Unary.Properties`:
+  ```agda
+  unique-given-suchthat : P ∩ UniqueGivenThat _≈_ P ≐ P ∩ UniqueSuchThat _≈_ P
+  ```
diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index e3fbe0c068..2bb5c2d86f 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -8,7 +8,8 @@
 
 module Relation.Unary.Properties where
 
-open import Data.Product.Base as Product using (_×_; _,_; -,_; swap; proj₁; zip′; curry)
+open import Data.Product.Base as Product
+  using (_×_; _,_; -,_; swap; proj₁; zip′; curry)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Unit.Base using (tt)
 open import Function.Base using (id; _$_; _∘_; _∘₂_)
@@ -335,3 +336,12 @@ U-irrelevant a b = refl
 
 ∁-irrelevant : (P : Pred A ℓ) → Irrelevant (∁ P)
 ∁-irrelevant P a b = refl
+
+------------------------------------------------------------------------
+-- Uniqueness properties
+
+unique-given-suchthat : {_≈_ : Rel A ℓ₁} {P : Pred A ℓ₂} →
+                        P ∩ UniqueGivenThat _≈_ P ≐ P ∩ UniqueSuchThat _≈_ P
+unique-given-suchthat =
+  (λ (Px , !Px) → Px , Px , (!Px Px)) , Product.map₂ λ (_ , !Px) → λ _ → !Px
+-- Product.map₂ (λ !Px → {!!} , !Px _)

From 41260f69edd11b56fa564076461027dd66b1fc32 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 12 Jul 2026 14:58:48 +0100
Subject: [PATCH 6/6] add: unique existence lemma

---
 CHANGELOG.md          |  5 +++++
 src/Data/Product.agda | 22 ++++++++++++++++------
 2 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2f7bc87270..4440913008 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -396,6 +396,11 @@ Additions to existing modules
   *-almostCancelʳ-≡ : AlmostRightCancellative 0 _*_
   ```
 
+* In `Data.Product`:
+  ```agda
+  ∃!-≐ : P ≐ Q → ∃! _≈_ P → ∃! _≈_ Q
+  ```
+
 * In `Data.Rational.Properties`:
   ```agda
   ↥[i/1]≡i  : (i : ℤ) → ↥ (i / 1) ≡ i
diff --git a/src/Data/Product.agda b/src/Data/Product.agda
index 7c8d21e7c2..ae28327e52 100644
--- a/src/Data/Product.agda
+++ b/src/Data/Product.agda
@@ -8,9 +8,13 @@
 
 module Data.Product where
 
+open import Function.Base using (_∘_; _$_)
+open import Function.Bundles using (_↔_; mk↔ₛ′)
 open import Level using (Level; _⊔_)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary.Negation.Core using (¬_)
-open import Relation.Unary using (UniqueSuchThat)
+open import Relation.Unary using (Pred; _≐_; UniqueSuchThat)
+open import Relation.Unary.Properties using (≐-sym)
 
 private
   variable
@@ -49,11 +53,6 @@ zipWith _∙_ _∘_ _*_ (a , p) (b , q) = (a ∙ b) * (p ∘ q)
 ∄ : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
 ∄ P = ¬ ∃ P
 
--- Unique existence (parametrised by an underlying equality).
-
-∃! : ∀ {A : Set a} → (A → A → Set ℓ) → (A → Set p) → Set (a ⊔ p ⊔ ℓ)
-∃! _≈_ P = ∃ (UniqueSuchThat _≈_ P)
-
 -- Syntax
 
 infix 2 ∄-syntax
@@ -62,3 +61,14 @@ infix 2 ∄-syntax
 ∄-syntax = ∄
 
 syntax ∄-syntax (λ x → B) = ∄[ x ] B
+
+------------------------------------------------------------------------
+-- Unique existence (parameterised by an underlying equality).
+
+module _ (_≈_ : Rel A ℓ) where
+
+  ∃! : (P : Pred A p) → Set _
+  ∃! P = ∃ (UniqueSuchThat _≈_ P)
+
+  ∃!-≐ : {P : Pred A p} {Q : Pred A q} → P ≐ Q → ∃! P → ∃! Q
+  ∃!-≐ (P⊆Q , Q⊆P) = map₂ (map P⊆Q λ !P → !P ∘ Q⊆P)