From fc2ca8a3545677bbd64c7df04d5ad19bc3212da1 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 10 Apr 2025 15:09:22 +0100
Subject: [PATCH 1/3] add: obvious lemma about self-contradiction

---
 CHANGELOG.md                            | 5 +++++
 src/Relation/Nullary/Negation/Core.agda | 7 ++++++-
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a6f66aa2f5..a3ffe081b5 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
+  self-contradiction : (A → ¬ A) → ¬ A
+  ```
diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 8d29075c38..45433ebf6f 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-module Relation.Nullary.Negation.Core where
+module Relation.Nullary.Negation.CoreNEW where
 
 open import Data.Empty using (⊥; ⊥-elim-irr)
 open import Data.Sum.Base using (_⊎_; [_,_]; inj₁; inj₂)
@@ -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
+
+self-contradiction : (A → ¬ A) → ¬ A
+self-contradiction 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))

From e9403ed50c56e08e174c5c9e6545aad3648f731a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 10 Apr 2025 15:11:34 +0100
Subject: [PATCH 2/3] add: obvious lemma about self-contradiction

---
 src/Relation/Nullary/Negation/Core.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 45433ebf6f..32a4b74bed 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-module Relation.Nullary.Negation.CoreNEW where
+module Relation.Nullary.Negation.Core where
 
 open import Data.Empty using (⊥; ⊥-elim-irr)
 open import Data.Sum.Base using (_⊎_; [_,_]; inj₁; inj₂)

From 0ec848b368c9b81f9e3b553a52030e87c1d02289 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 17 Apr 2025 09:11:12 +0100
Subject: [PATCH 3/3] fix: change name

---
 CHANGELOG.md                            | 2 +-
 src/Relation/Nullary/Negation/Core.agda | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a3ffe081b5..3a11051f76 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -247,5 +247,5 @@ Additions to existing modules
 
 * In `Relation.Nullary.Negation.Core`:
   ```agda
-  self-contradiction : (A → ¬ A) → ¬ A
+  contra-diagonal : (A → ¬ A) → ¬ A
   ```
diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 32a4b74bed..73876e876c 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -60,10 +60,10 @@ 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
+-- Self-contradictory propositions are false by 'diagonalisation'
 
-self-contradiction : (A → ¬ A) → ¬ A
-self-contradiction self a = self a a
+contra-diagonal : (A → ¬ A) → ¬ A
+contra-diagonal self a = self a a
 
 -- Everything is stable in the double-negation monad.
 stable : ¬ ¬ Stable A