[ add ] obvious lemma about self-contradiction to Relation.Nullary.Negation.Core (#2693)

* add: obvious lemma about self-contradiction

* add: obvious lemma about self-contradiction

* fix: change name

Author: jamesmckinna

CHANGELOG.md

@@ -287,3 +287,8 @@ Additions to existing modules
   ⊤-dec : Dec {a} ⊤
   ⊥-dec : Dec {a} ⊥
   ```
+
+* In `Relation.Nullary.Negation.Core`:
+  ```agda
+  contra-diagonal : (A → ¬ A) → ¬ A
+  ```

src/Relation/Nullary/Negation/Core.agda

@@ -60,6 +60,11 @@ 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))