Skip to content

[ refactor ] weaken type of Relation.Nullary.Negation.Core.contradiction-irr #2785

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Aug 2, 2025
+6 −2
Merged

[ refactor ] weaken type of Relation.Nullary.Negation.Core.contradiction-irr #2785

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a59ac04
refactor: weaken type of `contradiction-irr`
jamesmckinna Jul 26, 2025
1286e35
Merge branch 'master' into contradiction-irr
jamesmckinna Jul 31, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,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`.

* Refactored usages of `+-∸-assoc 1` to `∸-suc` in:
```agda
README.Data.Fin.Relation.Unary.Top
Expand Down
4 changes: 2 additions & 2 deletions src/Relation/Nullary/Negation/Core.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Was this changed forced? And if so, is this therefore a breaking change?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Two good questions, to which my evasive, equivocating answers would be: "yes, but...; no, but..."

As in the CHANGELOG, I regard this as a minor improvement : non-breaking, but arguably better move the commentary to non-backwards compatible (at least for the downstream consequences, because the unfolding behaviour of the proposed revised function definitions changes subtly)?

While the suggestion been punted before, I might still argue that the type of contradiction itself should be changed to .A → .(¬ A) → Whatever, but I thought that would be a step too far here... but perhaps one way out is simply to agree here and now that that is what we will do for v3.0 (and get rid of contradiction-irr completely!), and I'll move the milestone on the downstream PRs, but I don't want to have to relitigate these things for a third time then... ;-)


contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a
Expand Down