Systematise relational definitions at all arities (#2259)

* fixes #2091

* revised along the lines of @MatthewDaggitt's suggestions

---------

Co-authored-by: MatthewDaggitt <[email protected]>

Author: jamesmckinna

CHANGELOG.md

@@ -147,6 +147,23 @@ 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 _
+  ```
+
 * Added new proof in `Relation.Nullary.Decidable`:
   ```agda
   ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋

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 _

src/Relation/Nullary.agda

@@ -10,7 +10,15 @@
 
 module Relation.Nullary where
 
-open import Agda.Builtin.Equality
+open import Agda.Builtin.Equality using (_≡_)
+open import Agda.Builtin.Maybe using (Maybe)
+open import Level using (Level)
+
+private
+  variable
+    p : Level
+    P : Set p
+
 
 ------------------------------------------------------------------------
 -- Re-exports
@@ -22,5 +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 : 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

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