refactor: tighten imports (#2575)

Author: jamesmckinna

src/Axiom/DoubleNegationElimination.agda

@@ -10,26 +10,30 @@ module Axiom.DoubleNegationElimination where
 
 open import Axiom.ExcludedMiddle
 open import Level
-open import Relation.Nullary
-open import Relation.Nullary.Negation
-open import Relation.Nullary.Decidable
+open import Relation.Nullary.Decidable.Core
+  using (decidable-stable; ¬¬-excluded-middle)
+open import Relation.Nullary.Negation.Core using (Stable)
+
+private
+  variable
+    ℓ : Level
 
 ------------------------------------------------------------------------
 -- Definition
 
 -- The classical statement of double negation elimination says that
 -- if a property is not not true then it is true.
 
-DoubleNegationElimination : (ℓ : Level) → Set (suc ℓ)
-DoubleNegationElimination ℓ = {P : Set ℓ} → ¬ ¬ P → P
+DoubleNegationElimination : ∀ ℓ → Set (suc ℓ)
+DoubleNegationElimination ℓ = {P : Set ℓ} → Stable P
 
 ------------------------------------------------------------------------
 -- Properties
 
 -- Double negation elimination is equivalent to excluded middle
 
-em⇒dne : ∀ {ℓ} → ExcludedMiddle ℓ → DoubleNegationElimination ℓ
+em⇒dne : ExcludedMiddle ℓ → DoubleNegationElimination ℓ
 em⇒dne em = decidable-stable em
 
-dne⇒em : ∀ {ℓ} → DoubleNegationElimination ℓ → ExcludedMiddle ℓ
+dne⇒em : DoubleNegationElimination ℓ → ExcludedMiddle ℓ
 dne⇒em dne = dne ¬¬-excluded-middle

src/Axiom/ExcludedMiddle.agda

@@ -9,13 +9,13 @@
 module Axiom.ExcludedMiddle where
 
 open import Level
-open import Relation.Nullary
+open import Relation.Nullary.Decidable.Core using (Dec)
 
 ------------------------------------------------------------------------
 -- Definition
 
 -- The classical statement of excluded middle says that every
 -- statement/set is decidable (i.e. it either holds or it doesn't hold).
 
-ExcludedMiddle : (ℓ : Level) → Set (suc ℓ)
+ExcludedMiddle : ∀ ℓ → Set (suc ℓ)
 ExcludedMiddle ℓ = {P : Set ℓ} → Dec P