diff --git a/CHANGELOG.md b/CHANGELOG.md
index a6f66aa2f5..3a11051f76 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -244,3 +244,8 @@ Additions to existing modules
   ⊤-dec : Dec {a} ⊤
   ⊥-dec : Dec {a} ⊥
   ```
+
+* In `Relation.Nullary.Negation.Core`:
+  ```agda
+  contra-diagonal : (A → ¬ A) → ¬ A
+  ```
diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 8d29075c38..73876e876c 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/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))