From a59ac04bb358fa718ad56a09c42d13b323e35383 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 26 Jul 2025 14:27:03 +0100 Subject: [PATCH] refactor: weaken type of `contradiction-irr` --- CHANGELOG.md | 4 ++++ src/Relation/Nullary/Negation/Core.agda | 4 ++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3cf9a9ac90..e4cb912f3d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -15,6 +15,10 @@ Non-backwards compatible changes Minor improvements ------------------ +* The type of `Relation.Nullary.Negation.Core.contradiction-irr` has been further + weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is + safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`. + Deprecated modules ------------------ diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda index 73876e876c..b1e9425bf2 100644 --- a/src/Relation/Nullary/Negation/Core.agda +++ b/src/Relation/Nullary/Negation/Core.agda @@ -47,11 +47,11 @@ _¬-⊎_ = [_,_] ------------------------------------------------------------------------ -- Uses of negation -contradiction-irr : .A → ¬ A → Whatever +contradiction-irr : .A → .(¬ A) → Whatever contradiction-irr a ¬a = ⊥-elim-irr (¬a a) contradiction : A → ¬ A → Whatever -contradiction a = contradiction-irr a +contradiction a ¬a = contradiction-irr a ¬a contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a