From e825f54ad054453cc2ff5b04af9aaa7f386cfb48 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 31 Jul 2025 12:49:04 +0100
Subject: [PATCH 1/2] add: flipped version of `contradiction`

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3cf9a9ac90..391395de13 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -26,3 +26,8 @@ New modules
 
 Additions to existing modules
 -----------------------------
+
+* In `Relation.Nullary.Negation.Core`:
+  ```agda
+  contradiction′ : ¬ A → A → Whatever
+  ```
diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda
index 5372ac5f5e..7ff8bc2dc0 100644
--- a/src/Relation/Nullary/Negation.agda
+++ b/src/Relation/Nullary/Negation.agda
@@ -72,7 +72,7 @@ open import Relation.Nullary.Negation.Core public
 -- ⊥).
 
 call/cc : ((A → Whatever) → DoubleNegation A) → DoubleNegation A
-call/cc hyp ¬a = hyp (flip contradiction ¬a) ¬a
+call/cc hyp ¬a = hyp (contradiction′ ¬a) ¬a
 
 -- The "independence of premise" rule, in the double-negation monad.
 -- It is assumed that the index set (A) is inhabited.
@@ -82,7 +82,7 @@ independence-of-premise {A = A} {B = B} {P = P} q f = ¬¬-map helper ¬¬-exclu
   where
   helper : Dec B → Σ[ x ∈ A ] (B → P x)
   helper (yes p) = Product.map₂ const (f p)
-  helper (no ¬p) = (q , flip contradiction ¬p)
+  helper (no ¬p) = (q , contradiction′ ¬p)
 
 -- The independence of premise rule for binary sums.
 
@@ -91,7 +91,7 @@ independence-of-premise-⊎ {A = A} {B = B} {C = C} f = ¬¬-map helper ¬¬-exc
   where
   helper : Dec A → (A → B) ⊎ (A → C)
   helper (yes p) = Sum.map const const (f p)
-  helper (no ¬p) = inj₁ (flip contradiction ¬p)
+  helper (no ¬p) = inj₁ (contradiction′ ¬p)
 
 private
 
diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 73876e876c..899534d724 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -53,6 +53,9 @@ contradiction-irr a ¬a = ⊥-elim-irr (¬a a)
 contradiction : A → ¬ A → Whatever
 contradiction a = contradiction-irr a
 
+contradiction′ : ¬ A → A → Whatever
+contradiction′ ¬a a = contradiction-irr a ¬a
+
 contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
 contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a
 contradiction₂ (inj₂ b) ¬a ¬b = contradiction b ¬b

From 727bb46750cfc86561db5d0112ddd710fb510afe Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 1 Aug 2025 07:06:00 +0100
Subject: [PATCH 2/2] add: comment to `CHANGELOG`

---
 CHANGELOG.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4c6cb0b8ed..54165922d8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -57,7 +57,9 @@ Additions to existing modules
   ∸-suc : m ≤ n → suc n ∸ m ≡ suc (n ∸ m)
   ```
 
-* In `Relation.Nullary.Negation.Core`:
+* In `Relation.Nullary.Negation.Core`: because the *eager* insertion of
+  implicit arguments during type inference interacts badly with `contradiction`,
+  we introduce an explicit name for its `flip`ped version
   ```agda
   contradiction′ : ¬ A → A → Whatever
   ```