diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1e72ea222c..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
@@ -427,3 +432,15 @@ 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 _
+  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/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)
diff --git a/src/Data/Product.agda b/src/Data/Product.agda
index 9e032765c4..ae28327e52 100644
--- a/src/Data/Product.agda
+++ b/src/Data/Product.agda
@@ -8,8 +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 (Pred; _≐_; UniqueSuchThat)
+open import Relation.Unary.Properties using (≐-sym)
 
 private
   variable
@@ -48,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 b) → Set (a ⊔ b ⊔ ℓ)
-∃! _≈_ B = ∃ λ x → B x × (∀ {y} → B y → x ≈ y)
-
 -- Syntax
 
 infix 2 ∄-syntax
@@ -61,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)
diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 1146fef6cb..af787e76f4 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -198,6 +198,19 @@ 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
+
+  UniqueGivenThat : Pred A _
+  UniqueGivenThat x = P x → Unique x
+
+  UniqueSuchThat : Pred A _
+  UniqueSuchThat x = P x × Unique x
+
 ------------------------------------------------------------------------
 -- Operations on sets
 
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 _)