refactoring; move Stable to Relation.Unary

Author: jamesmckinna

CHANGELOG.md

@@ -3213,6 +3213,7 @@ Additions to existing modules
   _≐_  : Pred A ℓ₁ → Pred A ℓ₂ → Set _
   _≐′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
   _∖_  : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
+  Stable : Pred A ℓ → Set _
   ```
 
 * Added new proofs in `Relation.Unary.Properties`:

src/Induction/NoInfiniteDescent.agda

@@ -20,7 +20,7 @@ open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Construct.Closure.Transitive
 open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Nullary.Negation.Core as Negation using (¬_)
-open import Relation.Unary using (Pred; _∩_; _⇒_; Universal; IUniversal)
+open import Relation.Unary using (Pred; _∩_; _⇒_; Universal; IUniversal; Stable)
 
 private
   variable
@@ -204,20 +204,17 @@ module FurtherCorollaries {_<_ : Rel A r} (P : Pred A ℓ) where
 CounterExample : Pred A ℓ → Pred A ℓ
 CounterExample P = ¬_ ∘ P
 
-Stable : Pred A ℓ → Set _
-Stable P = ∀ {x} → Negation.Stable (P x)
-
 module _ {_<_ : Rel A r} {P : Pred A ℓ} (stable : Stable P) where
 
   open FurtherCorollaries {_<_ = _<_} (CounterExample P)
     using (acc⇒noInfiniteDescent⁺; wf⇒noInfiniteDescent⁺)
     renaming (Acc⇒Descent⁺ to NoSmallestCounterExample)
 
   acc⇒noSmallestCounterExample : NoSmallestCounterExample → ∀[ Acc _<_ ⇒ P ]
-  acc⇒noSmallestCounterExample noSmallest = stable ∘ (acc⇒noInfiniteDescent⁺ noSmallest)
+  acc⇒noSmallestCounterExample noSmallest = stable _ ∘ acc⇒noInfiniteDescent⁺ noSmallest
 
   wf⇒noSmallestCounterExample : WellFounded _<_ → NoSmallestCounterExample → ∀[ P ]
-  wf⇒noSmallestCounterExample wf noSmallest = stable (wf⇒noInfiniteDescent⁺ noSmallest wf)
+  wf⇒noSmallestCounterExample wf noSmallest = stable _ (wf⇒noInfiniteDescent⁺ noSmallest wf)
 
 ------------------------------------------------------------------------
 -- Exports

src/Relation/Unary.agda

@@ -15,7 +15,7 @@ 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.Negation.Core as Negation using (¬_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 private
@@ -162,6 +162,11 @@ IUniversal P = ∀ {x} → x ∈ P
 
 syntax IUniversal P = ∀[ P ]
 
+-- Stability - instances of P are stable wrt double negation
+
+Stable : Pred A ℓ → Set _
+Stable P = ∀ x → Negation.Stable (P x)
+
 -- Decidability - it is possible to determine if an arbitrary element
 -- satisfies P.