From e0d96694fd349de54b18b3998c8dc1e813965572 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 30 Oct 2025 12:13:06 +0000
Subject: [PATCH] fix: issue #2847

---
 CHANGELOG.md       | 5 +++++
 src/Data/Bool.agda | 8 ++++++++
 2 files changed, 13 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6679049fd0..9e78aca1d7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -132,6 +132,11 @@ Additions to existing modules
   ```
   NB. the latter is based on `IsCommutativeRing`, with the former on `IsSemiring`.
 
+* In `Data.Bool`:
+  ```agda
+  contradiction : b ≡ true → b ≡ false → Whatever
+  ```
+
 * In `Data.Fin.Permutation.Components`:
   ```agda
   transpose[i,i,j]≡j  : (i j : Fin n) → transpose i i j ≡ j
diff --git a/src/Data/Bool.agda b/src/Data/Bool.agda
index 55ed146e2c..e0b6cbdcf3 100644
--- a/src/Data/Bool.agda
+++ b/src/Data/Bool.agda
@@ -8,6 +8,8 @@
 
 module Data.Bool where
 
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+
 ------------------------------------------------------------------------
 -- The boolean type and some operations
 
@@ -18,3 +20,9 @@ open import Data.Bool.Base public
 
 open import Data.Bool.Properties public
   using (T?; _≟_; _≤?_; _<?_)
+
+------------------------------------------------------------------------
+-- Other functions
+
+contradiction : ∀ {w} {Whatever : Set w} {b} → b ≡ true → b ≡ false → Whatever
+contradiction refl ()