[ refactor ] reorganise Relation.Nullary.Negation.Core to make clean separation of properties

CHANGELOG.md

@@ -21,6 +21,11 @@ Minor improvements
   weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is
   safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`.
 
+* More generally, `Relation.Nullary.Negation.Core` has been reorganised into two
+  parts: the first concerns definitions and properties of negation considered as
+  a connective in *minimal logic*; the second making actual use of *ex falso* in
+  the form of `Data.Empty.⊥-elim`.
+
 * Refactored usages of `+-∸-assoc 1` to `∸-suc` in:
   ```agda
   README.Data.Fin.Relation.Unary.Top

src/Relation/Nullary/Negation/Core.agda

@@ -10,7 +10,7 @@ module Relation.Nullary.Negation.Core where
 
 open import Data.Empty using (⊥; ⊥-elim-irr)
 open import Data.Sum.Base using (_⊎_; [_,_]; inj₁; inj₂)
-open import Function.Base using (flip; _∘_; const)
+open import Function.Base using (_∘_; const)
 open import Level using (Level; _⊔_)
 
 private
@@ -20,37 +20,51 @@ private
     Whatever : Set w
 
 ------------------------------------------------------------------------
--- Negation.
+-- Definition.
 
 infix 3 ¬_
 ¬_ : Set a → Set a
 ¬ A = A → ⊥
 
 ------------------------------------------------------------------------
--- Stability.
+-- Properties, I: as a definition in *minimal logic*
+
+-- Contraposition
+contraposition : (A → B) → ¬ B → ¬ A
+contraposition f ¬b a =  ¬b (f a)
+
+-- Relationship to sum
+infixr 1 _¬-⊎_
+_¬-⊎_ : ¬ A → ¬ B → ¬ (A ⊎ B)
+_¬-⊎_ = [_,_]
+
+-- Self-contradictory propositions are false by 'diagonalisation'
+contra-diagonal : (A → ¬ A) → ¬ A
+contra-diagonal self a = self a a
 
 -- Double-negation
 DoubleNegation : Set a → Set a
 DoubleNegation A = ¬ ¬ A
 
 -- Eta law for double-negation
-
 ¬¬-η : A → ¬ ¬ A
 ¬¬-η a ¬a = ¬a a
 
+-- Functoriality for double-negation
+¬¬-map : (A → B) → ¬ ¬ A → ¬ ¬ B
+¬¬-map = contraposition ∘ contraposition
+
+------------------------------------------------------------------------
 -- Stability under double-negation.
 Stable : Set a → Set a
 Stable A = ¬ ¬ A → A
 
-------------------------------------------------------------------------
--- Relationship to sum
-
-infixr 1 _¬-⊎_
-_¬-⊎_ : ¬ A → ¬ B → ¬ (A ⊎ B)
-_¬-⊎_ = [_,_]
+-- Negated predicates are stable.
+negated-stable : Stable (¬ A)
+negated-stable ¬¬¬a a = ¬¬¬a (¬¬-η a)
 
 ------------------------------------------------------------------------
--- Uses of negation
+-- Properties, II: using the *ex falso* rule ⊥-elim
 
 contradiction-irr : .A → .(¬ A) → Whatever
 contradiction-irr a ¬a = ⊥-elim-irr (¬a a)
@@ -62,27 +76,7 @@ contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
 contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a
 contradiction₂ (inj₂ b) ¬a ¬b = contradiction b ¬b
 
-contraposition : (A → B) → ¬ B → ¬ A
-contraposition f ¬b a = contradiction (f a) ¬b
-
--- Self-contradictory propositions are false by 'diagonalisation'
-
-contra-diagonal : (A → ¬ A) → ¬ A
-contra-diagonal self a = self a a
-
 -- Everything is stable in the double-negation monad.
 stable : ¬ ¬ Stable A
 stable ¬[¬¬a→a] = ¬[¬¬a→a] (contradiction (¬[¬¬a→a] ∘ const))
 
--- Negated predicates are stable.
-negated-stable : Stable (¬ A)
-negated-stable ¬¬¬a a = ¬¬¬a (contradiction a)
-
-¬¬-map : (A → B) → ¬ ¬ A → ¬ ¬ B
-¬¬-map f = contraposition (contraposition f)
-
--- Note also the following use of flip:
-private
-  note : (A → ¬ B) → B → ¬ A
-  note = flip
-