From 0b3e5cd8e586e98715e2a283454bfc5f1a59e66f Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 17 Jan 2024 17:29:33 +0000
Subject: [PATCH 1/2] fixes #2091

---
 CHANGELOG.md                         | 17 +++++++++++
 src/Relation/Binary/Definitions.agda | 43 +++++++++++++++-------------
 src/Relation/Nullary.agda            | 13 ++++++++-
 src/Relation/Unary.agda              | 37 +++++++++++++++---------
 4 files changed, 75 insertions(+), 35 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5b3079dee4..ada31cf605 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -88,3 +88,20 @@ Additions to existing modules
 
 * In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can
   be used infix.
+
+* Added new definitions in `Relation.Binary`
+  ```
+  Stable          : Pred A ℓ → Set _
+  ```
+
+* Added new definitions in `Relation.Nullary`
+  ```
+  Recomputable    : Set _
+  WeaklyDecidable : Set _
+  ```
+
+* Added new definitions in `Relation.Unary`
+  ```
+  Stable          : Pred A ℓ → Set _
+  WeaklyDecidable : Pred A ℓ → Set _
+  ```
diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda
index 887cb7c4a6..dd0e016c12 100644
--- a/src/Relation/Binary/Definitions.agda
+++ b/src/Relation/Binary/Definitions.agda
@@ -12,14 +12,12 @@ module Relation.Binary.Definitions where
 
 open import Agda.Builtin.Equality using (_≡_)
 
-open import Data.Maybe.Base using (Maybe)
 open import Data.Product.Base using (_×_; ∃-syntax)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_on_; flip)
 open import Level
 open import Relation.Binary.Core
-open import Relation.Nullary.Decidable.Core using (Dec)
-open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Nullary as Nullary using (¬_; Dec)
 
 private
   variable
@@ -206,35 +204,40 @@ P Respects₂ _∼_ = (P Respectsʳ _∼_) × (P Respectsˡ _∼_)
 Substitutive : Rel A ℓ₁ → (ℓ₂ : Level) → Set _
 Substitutive {A = A} _∼_ p = (P : A → Set p) → P Respects _∼_
 
--- Decidability - it is possible to determine whether a given pair of
--- elements are related.
+-- Irrelevancy - all proofs that a given pair of elements are related
+-- are indistinguishable.
 
-Decidable : REL A B ℓ → Set _
-Decidable _∼_ = ∀ x y → Dec (x ∼ y)
+Irrelevant : REL A B ℓ → Set _
+Irrelevant _∼_ = ∀ {x y} → Nullary.Irrelevant (x ∼ y)
+
+-- Recomputability - we can rebuild a relevant proof given an
+-- irrelevant one.
+
+Recomputable : REL A B ℓ → Set _
+Recomputable _∼_ = ∀ {x y} → Nullary.Recomputable (x ∼ y)
+
+-- Stability
+
+Stable : REL A B ℓ → Set _
+Stable _∼_ = ∀ x y → Nullary.Stable (x ∼ y)
 
 -- Weak decidability - it is sometimes possible to determine if a given
 -- pair of elements are related.
 
 WeaklyDecidable : REL A B ℓ → Set _
-WeaklyDecidable _∼_ = ∀ x y → Maybe (x ∼ y)
+WeaklyDecidable _∼_ = ∀ x y → Nullary.WeaklyDecidable (x ∼ y)
+
+-- Decidability - it is possible to determine whether a given pair of
+-- elements are related.
+
+Decidable : REL A B ℓ → Set _
+Decidable _∼_ = ∀ x y → Dec (x ∼ y)
 
 -- Propositional equality is decidable for the type.
 
 DecidableEquality : (A : Set a) → Set _
 DecidableEquality A = Decidable {A = A} _≡_
 
--- Irrelevancy - all proofs that a given pair of elements are related
--- are indistinguishable.
-
-Irrelevant : REL A B ℓ → Set _
-Irrelevant _∼_ = ∀ {x y} (a b : x ∼ y) → a ≡ b
-
--- Recomputability - we can rebuild a relevant proof given an
--- irrelevant one.
-
-Recomputable : REL A B ℓ → Set _
-Recomputable _∼_ = ∀ {x y} → .(x ∼ y) → x ∼ y
-
 -- Universal - all pairs of elements are related
 
 Universal : REL A B ℓ → Set _
diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index 0b0f83f77b..3272bbc5d1 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -10,7 +10,10 @@
 
 module Relation.Nullary where
 
-open import Agda.Builtin.Equality
+open import Agda.Builtin.Equality using (_≡_)
+open import Agda.Builtin.Maybe public
+  using (nothing; just)
+  renaming (Maybe to WeaklyDecidable)
 
 ------------------------------------------------------------------------
 -- Re-exports
@@ -24,3 +27,11 @@ open import Relation.Nullary.Decidable.Core public
 
 Irrelevant : ∀ {p} → Set p → Set p
 Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
+
+------------------------------------------------------------------------
+-- Recomputability - we can rebuild a relevant proof given an
+-- irrelevant one.
+
+Recomputable : ∀ {p} → Set p → Set p
+Recomputable P = .P → P
+
diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index f6d7cb13b0..357237a2be 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -14,8 +14,7 @@ open import Data.Product.Base using (_×_; _,_; Σ-syntax; ∃; uncurry; swap)
 open import Data.Sum.Base using (_⊎_; [_,_])
 open import Function.Base using (_∘_; _|>_)
 open import Level using (Level; _⊔_; 0ℓ; suc; Lift)
-open import Relation.Nullary.Decidable.Core using (Dec; True)
-open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Nullary as Nullary using (¬_; Dec; True)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 private
@@ -162,6 +161,28 @@ IUniversal P = ∀ {x} → x ∈ P
 
 syntax IUniversal P = ∀[ P ]
 
+-- Irrelevance - any two proofs that an element satifies P are
+-- indistinguishable.
+
+Irrelevant : Pred A ℓ → Set _
+Irrelevant P = ∀ {x} → Nullary.Irrelevant (P x)
+
+-- Recomputability - we can rebuild a relevant proof given an
+-- irrelevant one.
+
+Recomputable : Pred A ℓ → Set _
+Recomputable P = ∀ {x} → Nullary.Recomputable (P x)
+
+-- Weak Decidability
+
+Stable : Pred A ℓ → Set _
+Stable P = ∀ x → Nullary.Stable (P x)
+
+-- Weak Decidability
+
+WeaklyDecidable : Pred A ℓ → Set _
+WeaklyDecidable P = ∀ x → Nullary.WeaklyDecidable (P x)
+
 -- Decidability - it is possible to determine if an arbitrary element
 -- satisfies P.
 
@@ -174,18 +195,6 @@ Decidable P = ∀ x → Dec (P x)
 ⌊_⌋ : {P : Pred A ℓ} → Decidable P → Pred A ℓ
 ⌊ P? ⌋ a = Lift _ (True (P? a))
 
--- Irrelevance - any two proofs that an element satifies P are
--- indistinguishable.
-
-Irrelevant : Pred A ℓ → Set _
-Irrelevant P = ∀ {x} (a : P x) (b : P x) → a ≡ b
-
--- Recomputability - we can rebuild a relevant proof given an
--- irrelevant one.
-
-Recomputable : Pred A ℓ → Set _
-Recomputable P = ∀ {x} → .(P x) → P x
-
 ------------------------------------------------------------------------
 -- Operations on sets
 

From 35caf79d02525cad24d7fef154824b475eccb7d5 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 20 Jan 2024 14:49:03 +0000
Subject: [PATCH 2/2] revised along the lines of @MatthewDaggitt's suggestions

---
 src/Relation/Nullary.agda | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index 3272bbc5d1..92e0607f4d 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -11,9 +11,14 @@
 module Relation.Nullary where
 
 open import Agda.Builtin.Equality using (_≡_)
-open import Agda.Builtin.Maybe public
-  using (nothing; just)
-  renaming (Maybe to WeaklyDecidable)
+open import Agda.Builtin.Maybe using (Maybe)
+open import Level using (Level)
+
+private
+  variable
+    p : Level
+    P : Set p
+
 
 ------------------------------------------------------------------------
 -- Re-exports
@@ -25,13 +30,19 @@ open import Relation.Nullary.Decidable.Core public
 ------------------------------------------------------------------------
 -- Irrelevant types
 
-Irrelevant : ∀ {p} → Set p → Set p
+Irrelevant : Set p → Set p
 Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
 
 ------------------------------------------------------------------------
 -- Recomputability - we can rebuild a relevant proof given an
 -- irrelevant one.
 
-Recomputable : ∀ {p} → Set p → Set p
+Recomputable : Set p → Set p
 Recomputable P = .P → P
 
+------------------------------------------------------------------------
+-- Weak decidability
+-- `nothing` is 'don't know'/'give up'; `just` is `yes`/`definitely`
+
+WeaklyDecidable : Set p → Set p
+WeaklyDecidable = Maybe