From 0db48743c0ab989f01d8c26b02b69a00d79e5921 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 4 Aug 2025 08:39:10 +0100 Subject: [PATCH 01/10] [ refactor ] make `contradiction` and friends entirely proof-irrelevant --- CHANGELOG.md | 60 +++---------------------- doc/style-guide.md | 6 +++ src/Relation/Nullary/Negation/Core.agda | 43 +++++++++--------- src/Relation/Nullary/Reflects.agda | 4 +- 4 files changed, 36 insertions(+), 77 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ef9533efc6..5f2a36a419 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,4 +1,4 @@ -Version 2.4-dev +Version 3.0-dev =============== The library has been tested using Agda 2.8.0. @@ -9,26 +9,16 @@ Highlights Bug-fixes --------- -* Fix a type error in `README.Data.Fin.Relation.Unary.Top` within the definition of `>-weakInduction`. - 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`. +* In `Relation.Nullary.Negation.Core`, all the various types of `contradiction` + have been weakened as far as possible to make their arguments definitionally + proof-irrelevant. As a consequence, there is no longer any need for the + separate v2.4 `contradiction-irr`. -* Refactored usages of `+-∸-assoc 1` to `∸-suc` in: - ```agda - README.Data.Fin.Relation.Unary.Top - Algebra.Properties.Semiring.Binomial - Data.Fin.Subset.Properties - Data.Nat.Binary.Subtraction - Data.Nat.Combinatorics - ``` +Other major improvements +------------------------ Deprecated modules ------------------ @@ -36,44 +26,8 @@ Deprecated modules Deprecated names ---------------- -* In `Algebra.Properties.CommutativeSemigroup`: - ```agda - interchange ↦ medial - ``` - New modules ----------- -* `Data.List.Relation.Binary.Permutation.Algorithmic{.Properties}` for the Choudhury and Fiore definition of permutation, and its equivalence with `Declarative` below. - -* `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition. - Additions to existing modules ----------------------------- - -* In `Algebra.Properties.RingWithoutOne`: - ```agda - [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y - ``` - -* In `Data.Fin.Permutation.Components`: - ```agda - transpose[i,i,j]≡j : (i j : Fin n) → transpose i i j ≡ j - transpose[i,j,j]≡i : (i j : Fin n) → transpose i j j ≡ i - transpose[i,j,i]≡j : (i j : Fin n) → transpose i j i ≡ j - transpose-transpose : transpose i j k ≡ l → transpose j i l ≡ k - ``` - -* In `Data.Fin.Properties`: - ```agda - ≡-irrelevant : Irrelevant {A = Fin n} _≡_ - ≟-≡ : (eq : i ≡ j) → (i ≟ j) ≡ yes eq - ≟-≡-refl : (i : Fin n) → (i ≟ i) ≡ yes refl - ≟-≢ : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j - ``` - -* In `Data.Nat.Properties`: - ```agda - ≟-≢ : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n - ∸-suc : m ≤ n → suc n ∸ m ≡ suc (n ∸ m) - ``` diff --git a/doc/style-guide.md b/doc/style-guide.md index 7da14eb7f5..30cd26caaf 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -717,3 +717,9 @@ used successfully in PR systematic for `Nary` relations in PR [#811](https://github.com/agda/agda-stdlib/pull/811) +## Prefer use of `Relation.Nullary.Negation.Core.contradiction` + +Where possible use `contradiction` between two explicit arguments rather +than appealing to the lower-level `Data.Empty.⊥-elim`. This provides +clearer documentation for readers of the code, but also permits a wider +range of application, thanks to its arguments being made proof-irrelevant. \ No newline at end of file diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda index b1e9425bf2..331bed3e53 100644 --- a/src/Relation/Nullary/Negation/Core.agda +++ b/src/Relation/Nullary/Negation/Core.agda @@ -26,6 +26,18 @@ infix 3 ¬_ ¬_ : Set a → Set a ¬ A = A → ⊥ +-- Note the following use of flip: +private + note : (A → ¬ B) → B → ¬ A + note = flip + +------------------------------------------------------------------------ +-- Relationship to sum + +infixr 1 _¬-⊎_ +_¬-⊎_ : ¬ A → ¬ B → ¬ (A ⊎ B) +_¬-⊎_ = [_,_] + ------------------------------------------------------------------------ -- Stability. @@ -37,27 +49,20 @@ DoubleNegation A = ¬ ¬ A Stable : Set a → Set a Stable A = ¬ ¬ A → A ------------------------------------------------------------------------- --- Relationship to sum - -infixr 1 _¬-⊎_ -_¬-⊎_ : ¬ A → ¬ B → ¬ (A ⊎ B) -_¬-⊎_ = [_,_] - ------------------------------------------------------------------------ -- Uses of negation -contradiction-irr : .A → .(¬ A) → Whatever -contradiction-irr a ¬a = ⊥-elim-irr (¬a a) +contradiction : .A → .(¬ A) → Whatever +contradiction a ¬a = ⊥-elim-irr (¬a a) -contradiction : A → ¬ A → Whatever -contradiction a ¬a = contradiction-irr a ¬a +contradiction′ : .(¬ A) → .A → Whatever +contradiction′ ¬a a = ⊥-elim-irr (¬a a) -contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever +contradiction₂ : A ⊎ B → .(¬ A) → .(¬ B) → Whatever contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a contradiction₂ (inj₂ b) ¬a ¬b = contradiction b ¬b -contraposition : (A → B) → ¬ B → ¬ A +contraposition : (A → B) → .(¬ B) → ¬ A contraposition f ¬b a = contradiction (f a) ¬b -- Self-contradictory propositions are false by 'diagonalisation' @@ -67,17 +72,11 @@ contra-diagonal 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)) +stable ¬[¬¬a→a] = ¬[¬¬a→a] λ ¬¬a → contradiction (¬[¬¬a→a] ∘ const) ¬¬a -- Negated predicates are stable. negated-stable : Stable (¬ A) -negated-stable ¬¬¬a a = ¬¬¬a (contradiction a) +negated-stable ¬¬¬a a = ¬¬¬a λ ¬a → contradiction a ¬a ¬¬-map : (A → B) → ¬ ¬ A → ¬ ¬ B -¬¬-map f = contraposition (contraposition f) - --- Note also the following use of flip: -private - note : (A → ¬ B) → B → ¬ A - note = flip - +¬¬-map f ¬¬a = contraposition (λ ¬b → contraposition f ¬b) ¬¬a diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda index f89fbcf313..537c6c6726 100644 --- a/src/Relation/Nullary/Reflects.agda +++ b/src/Relation/Nullary/Reflects.agda @@ -18,7 +18,7 @@ open import Data.Empty.Polymorphic using (⊥) open import Level using (Level) open import Function.Base using (_$_; _∘_; const; id) open import Relation.Nullary.Negation.Core - using (¬_; contradiction-irr; contradiction; _¬-⊎_) + using (¬_; contradiction; _¬-⊎_) open import Relation.Nullary.Recomputable as Recomputable using (Recomputable) private @@ -61,7 +61,7 @@ invert (ofⁿ ¬a) = ¬a recompute : ∀ {b} → Reflects A b → Recomputable A recompute (ofʸ a) _ = a -recompute (ofⁿ ¬a) a = contradiction-irr a ¬a +recompute (ofⁿ ¬a) a = contradiction a ¬a recompute-constant : ∀ {b} (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q From 1c7b74e2e2c54e42f161c25bcd359f2eb8ad1bc3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 4 Aug 2025 08:51:38 +0100 Subject: [PATCH 02/10] fix: whitespace --- doc/style-guide.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/style-guide.md b/doc/style-guide.md index 30cd26caaf..36d70af28c 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -722,4 +722,4 @@ systematic for `Nary` relations in PR Where possible use `contradiction` between two explicit arguments rather than appealing to the lower-level `Data.Empty.⊥-elim`. This provides clearer documentation for readers of the code, but also permits a wider -range of application, thanks to its arguments being made proof-irrelevant. \ No newline at end of file +range of application, thanks to its arguments being made proof-irrelevant. From c4cb90fc408056edbbad48abeab60024d5d47e4e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 4 Aug 2025 09:13:16 +0100 Subject: [PATCH 03/10] =?UTF-8?q?add:=20eta=20law=20for=20=C2=AC=C2=AC=20m?= =?UTF-8?q?onad?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 5 +++++ src/Relation/Nullary/Decidable/Core.agda | 4 ++-- src/Relation/Nullary/Negation.agda | 2 +- src/Relation/Nullary/Negation/Core.agda | 5 +++++ 4 files changed, 13 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5f2a36a419..1d66b32c4c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -31,3 +31,8 @@ New modules Additions to existing modules ----------------------------- + +* In `Relation.Nullary.Negation.Core` + ```agda + ¬¬-η : A → ¬ ¬ A + ``` diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda index 47b9e55b55..b964141439 100644 --- a/src/Relation/Nullary/Decidable/Core.agda +++ b/src/Relation/Nullary/Decidable/Core.agda @@ -28,7 +28,7 @@ open import Relation.Nullary.Recomputable.Core as Recomputable open import Relation.Nullary.Reflects as Reflects hiding (recompute; recompute-constant) open import Relation.Nullary.Negation.Core - using (¬_; Stable; negated-stable; contradiction; DoubleNegation) + using (¬_; ¬¬-η; Stable; negated-stable; contradiction; DoubleNegation) private @@ -215,7 +215,7 @@ decidable-stable (true because [a]) ¬¬a = invert [a] decidable-stable (false because [¬a]) ¬¬a = contradiction (invert [¬a]) ¬¬a ¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A) -¬-drop-Dec ¬¬a? = map′ negated-stable contradiction (¬? ¬¬a?) +¬-drop-Dec ¬¬a? = map′ negated-stable ¬¬-η (¬? ¬¬a?) -- A double-negation-translated variant of excluded middle (or: every -- nullary relation is decidable in the double-negation monad). diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda index 5372ac5f5e..706c238220 100644 --- a/src/Relation/Nullary/Negation.agda +++ b/src/Relation/Nullary/Negation.agda @@ -56,7 +56,7 @@ open import Relation.Nullary.Negation.Core public ¬¬-Monad : RawMonad {a} DoubleNegation ¬¬-Monad = mkRawMonad DoubleNegation - contradiction + ¬¬-eta (λ x f → negated-stable (¬¬-map f x)) ¬¬-push : DoubleNegation Π[ P ] → Π[ DoubleNegation ∘ P ] diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda index 331bed3e53..3fd239e5df 100644 --- a/src/Relation/Nullary/Negation/Core.agda +++ b/src/Relation/Nullary/Negation/Core.agda @@ -45,6 +45,11 @@ _¬-⊎_ = [_,_] DoubleNegation : Set a → Set a DoubleNegation A = ¬ ¬ A +-- Eta law for double-negation + +¬¬-η : A → ¬ ¬ A +¬¬-η a ¬a = ¬a a + -- Stability under double-negation. Stable : Set a → Set a Stable A = ¬ ¬ A → A From 00c0354849a2cb8169ffdbc79207911fed7c207c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 4 Aug 2025 09:57:57 +0100 Subject: [PATCH 04/10] fix: more eta-expansion needed --- src/Relation/Nullary/Negation.agda | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda index 706c238220..eb35ae5a34 100644 --- a/src/Relation/Nullary/Negation.agda +++ b/src/Relation/Nullary/Negation.agda @@ -56,7 +56,7 @@ open import Relation.Nullary.Negation.Core public ¬¬-Monad : RawMonad {a} DoubleNegation ¬¬-Monad = mkRawMonad DoubleNegation - ¬¬-eta + ¬¬-η (λ x f → negated-stable (¬¬-map f x)) ¬¬-push : DoubleNegation Π[ P ] → Π[ DoubleNegation ∘ P ] @@ -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 (λ a → contradiction a ¬a) ¬a -- The "independence of premise" rule, in the double-negation monad. -- It is assumed that the index set (A) is inhabited. @@ -81,8 +81,8 @@ independence-of-premise : A → (B → Σ A P) → DoubleNegation (Σ[ x ∈ A ] independence-of-premise {A = A} {B = B} {P = P} q f = ¬¬-map helper ¬¬-excluded-middle 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 (yes b) = Product.map₂ const (f b) + helper (no ¬b) = (q , λ b → contradiction b ¬b) -- The independence of premise rule for binary sums. @@ -90,8 +90,8 @@ independence-of-premise-⊎ : (A → B ⊎ C) → DoubleNegation ((A → B) ⊎ independence-of-premise-⊎ {A = A} {B = B} {C = C} f = ¬¬-map helper ¬¬-excluded-middle 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 (yes a) = Sum.map const const (f a) + helper (no ¬a) = inj₁ λ a → contradiction a ¬a private From 863d63c6a5baa5ed53c4a93ccea4f5c915e8d276 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 4 Aug 2025 10:15:36 +0100 Subject: [PATCH 05/10] fix: more eta-expansion needed --- src/Algebra/Module/Properties/Semimodule.agda | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Module/Properties/Semimodule.agda b/src/Algebra/Module/Properties/Semimodule.agda index d7686b25ef..e05b4ea1e7 100644 --- a/src/Algebra/Module/Properties/Semimodule.agda +++ b/src/Algebra/Module/Properties/Semimodule.agda @@ -16,25 +16,28 @@ module Algebra.Module.Properties.Semimodule (semimod : Semimodule semiring m ℓm) where +open import Relation.Nullary.Negation using (contraposition) + open CommutativeSemiring semiring open Semimodule semimod open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid -open import Relation.Nullary.Negation using (contraposition) + +------------------------------------------------------------------------ x≈0⇒x*y≈0 : ∀ {x y} → x ≈ 0# → x *ₗ y ≈ᴹ 0ᴹ -x≈0⇒x*y≈0 {x} {y} x≈0 = begin +x≈0⇒x*y≈0 {x = x} {y = y} x≈0 = begin x *ₗ y ≈⟨ *ₗ-congʳ x≈0 ⟩ 0# *ₗ y ≈⟨ *ₗ-zeroˡ y ⟩ 0ᴹ ∎ y≈0⇒x*y≈0 : ∀ {x y} → y ≈ᴹ 0ᴹ → x *ₗ y ≈ᴹ 0ᴹ -y≈0⇒x*y≈0 {x} {y} y≈0 = begin +y≈0⇒x*y≈0 {x = x} {y = y} y≈0 = begin x *ₗ y ≈⟨ *ₗ-congˡ y≈0 ⟩ x *ₗ 0ᴹ ≈⟨ *ₗ-zeroʳ x ⟩ 0ᴹ ∎ x*y≉0⇒x≉0 : ∀ {x y} → x *ₗ y ≉ᴹ 0ᴹ → x ≉ 0# -x*y≉0⇒x≉0 = contraposition x≈0⇒x*y≈0 +x*y≉0⇒x≉0 x≈0 = contraposition x≈0⇒x*y≈0 x≈0 x*y≉0⇒y≉0 : ∀ {x y} → x *ₗ y ≉ᴹ 0ᴹ → y ≉ᴹ 0ᴹ -x*y≉0⇒y≉0 = contraposition y≈0⇒x*y≈0 +x*y≉0⇒y≉0 y≈0 = contraposition y≈0⇒x*y≈0 y≈0 From 757f28a20a6c9bf4a5181fc12646a355a01b9601 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 4 Aug 2025 10:25:43 +0100 Subject: [PATCH 06/10] fix: `_-uno` bad fit for irrelevant arguments --- .../Relation/Binary/Sublist/Heterogeneous/Properties.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda index a80d689ec5..5c9e2c5227 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda @@ -409,17 +409,17 @@ module Antisymmetry length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩ length zs ≤⟨ ℕ.n≤1+n (length zs) ⟩ length (z ∷ zs) ≤⟨ length-mono-≤ rs ⟩ - length ys₁ ∎) $ ℕ.<-irrefl ≡.refl + length ys₁ ∎) (ℕ.<-irrefl ≡.refl) antisym (_∷ʳ_ {xs} {ys₁} y rs) (_∷_ {y} {ys₂} {z} {zs} s ss) = contradiction (begin length (z ∷ zs) ≤⟨ length-mono-≤ rs ⟩ length ys₁ ≤⟨ length-mono-≤ ss ⟩ - length zs ∎) $ ℕ.<-irrefl ≡.refl + length zs ∎) (ℕ.<-irrefl ≡.refl) antisym (_∷_ {x} {xs} {y} {ys₁} r rs) (_∷ʳ_ {ys₂} {zs} z ss) = contradiction (begin length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩ length xs ≤⟨ length-mono-≤ rs ⟩ - length ys₁ ∎) $ ℕ.<-irrefl ≡.refl + length ys₁ ∎) (ℕ.<-irrefl ≡.refl) open Antisymmetry public From 9ce9d09e8d62587a0c6b0ceb586713e79290f0d5 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 4 Aug 2025 10:31:44 +0100 Subject: [PATCH 07/10] fix: more eta-expansion needed --- src/Data/Nat/Primality.agda | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index c70cc5c3bc..d4399c11cb 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -22,7 +22,8 @@ open import Function.Base using (flip; _∘_; _∘′_) open import Function.Bundles using (_⇔_; mk⇔) open import Relation.Nullary.Decidable as Dec using (yes; no; from-yes; from-no; ¬?; _×-dec_; _⊎-dec_; _→-dec_; decidable-stable) -open import Relation.Nullary.Negation.Core using (¬_; contradiction; contradiction₂) +open import Relation.Nullary.Negation.Core + using (¬_; contradiction; contradiction′; contradiction₂) open import Relation.Unary using (Pred; Decidable) open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core @@ -347,8 +348,9 @@ irreducible[2] {suc _} d∣2 with ∣⇒≤ d∣2 ... | s Date: Mon, 4 Aug 2025 11:07:00 +0100 Subject: [PATCH 08/10] fix: more eta-expansion needed --- src/Algebra/Module/Morphism/ModuleHomomorphism.agda | 2 +- src/Data/List/Relation/Unary/First/Properties.agda | 6 +++--- src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda | 4 ++-- src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/Algebra/Module/Morphism/ModuleHomomorphism.agda b/src/Algebra/Module/Morphism/ModuleHomomorphism.agda index 5ed32380de..fe099814be 100644 --- a/src/Algebra/Module/Morphism/ModuleHomomorphism.agda +++ b/src/Algebra/Module/Morphism/ModuleHomomorphism.agda @@ -51,7 +51,7 @@ x≈0⇒fx≈0 {x} x≈0 = begin⟨ B.≈ᴹ-setoid ⟩ B.0ᴹ ∎ fx≉0⇒x≉0 : ∀ {x} → f x B.≉ᴹ B.0ᴹ → x A.≉ᴹ A.0ᴹ -fx≉0⇒x≉0 = contraposition x≈0⇒fx≈0 +fx≉0⇒x≉0 x≈0 = contraposition x≈0⇒fx≈0 x≈0 -- Zero is a unique output of non-trivial (i.e. - ≉ `const 0`) linear map. x≉0⇒f[x]≉0 : ∀ {x} → NonTrivial x → x A.≉ᴹ A.0ᴹ → f x B.≉ᴹ B.0ᴹ diff --git a/src/Data/List/Relation/Unary/First/Properties.agda b/src/Data/List/Relation/Unary/First/Properties.agda index dac49597b1..e80d0d2b68 100644 --- a/src/Data/List/Relation/Unary/First/Properties.agda +++ b/src/Data/List/Relation/Unary/First/Properties.agda @@ -18,7 +18,7 @@ import Data.Sum.Base as Sum open import Function.Base using (_∘′_; _∘_; id) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; _≗_) open import Relation.Nullary.Decidable.Core as Dec -open import Relation.Nullary.Negation.Core using (contradiction) +open import Relation.Nullary.Negation.Core using (¬¬-η; contradiction) open import Relation.Nullary.Reflects using (invert) open import Relation.Unary using (Pred; _⊆_; ∁; Irrelevant; Decidable) @@ -54,7 +54,7 @@ module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where All⇒¬First : P ⊆ ∁ Q → All P ⊆ ∁ (First P Q) - All⇒¬First p⇒¬q (px ∷ pxs) [ qx ] = contradiction qx (p⇒¬q px) + All⇒¬First p⇒¬q (px ∷ pxs) [ qx ] = p⇒¬q px qx All⇒¬First p⇒¬q (_ ∷ pxs) (_ ∷ hf) = All⇒¬First p⇒¬q pxs hf First⇒¬All : Q ⊆ ∁ P → First P Q ⊆ ∁ (All P) @@ -97,7 +97,7 @@ module _ {a p} {A : Set a} {P : Pred A p} where first? : Decidable P → Decidable (First P (∁ P)) first? P? = Dec.fromSum - ∘ Sum.map₂ (All⇒¬First contradiction) + ∘ Sum.map₂ (All⇒¬First ¬¬-η) ∘ first (Dec.toSum ∘ P?) cofirst? : Decidable P → Decidable (First (∁ P) P) diff --git a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda index 616247b696..fec3098491 100644 --- a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda +++ b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda @@ -49,11 +49,11 @@ module _ (S : Setoid a ℓ₁) (R : Setoid b ℓ₂) where map⁺ : ∀ {f} → (∀ {x y} → f x ≈₂ f y → x ≈₁ y) → ∀ {xs} → Unique S xs → Unique R (map f xs) - map⁺ inj xs! = AllPairs.map⁺ (AllPairs.map (contraposition inj) xs!) + map⁺ inj xs! = AllPairs.map⁺ (AllPairs.map (λ x≈y → contraposition inj x≈y) xs!) map⁻ : ∀ {f} → Congruent _≈₁_ _≈₂_ f → ∀ {xs} → Unique R (map f xs) → Unique S xs - map⁻ cong fxs! = AllPairs.map (contraposition cong) (AllPairs.map⁻ fxs!) + map⁻ cong fxs! = AllPairs.map (λ fx≉fy → contraposition cong fx≉fy) (AllPairs.map⁻ fxs!) ------------------------------------------------------------------------ -- ++ diff --git a/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda b/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda index fa19dc3e21..8ab066083e 100644 --- a/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda @@ -39,7 +39,7 @@ module _ (S : Setoid a ℓ₁) (R : Setoid b ℓ₂) where map⁺ : ∀ {f} → (∀ {x y} → f x ≈₂ f y → x ≈₁ y) → ∀ {n xs} → Unique S {n} xs → Unique R {n} (map f xs) - map⁺ inj xs! = AllPairs.map⁺ (AllPairs.map (contraposition inj) xs!) + map⁺ inj xs! = AllPairs.map⁺ (AllPairs.map (λ x≈y → contraposition inj x≈y) xs!) ------------------------------------------------------------------------ -- take & drop From 680839b00596a3fbf304c80e1c27583842a3011e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 4 Aug 2025 15:18:49 +0100 Subject: [PATCH 09/10] fix: remove named telescopes --- src/Algebra/Module/Properties/Semimodule.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Module/Properties/Semimodule.agda b/src/Algebra/Module/Properties/Semimodule.agda index e05b4ea1e7..131b0a3263 100644 --- a/src/Algebra/Module/Properties/Semimodule.agda +++ b/src/Algebra/Module/Properties/Semimodule.agda @@ -25,13 +25,13 @@ open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid ------------------------------------------------------------------------ x≈0⇒x*y≈0 : ∀ {x y} → x ≈ 0# → x *ₗ y ≈ᴹ 0ᴹ -x≈0⇒x*y≈0 {x = x} {y = y} x≈0 = begin +x≈0⇒x*y≈0 {x} {y} x≈0 = begin x *ₗ y ≈⟨ *ₗ-congʳ x≈0 ⟩ 0# *ₗ y ≈⟨ *ₗ-zeroˡ y ⟩ 0ᴹ ∎ y≈0⇒x*y≈0 : ∀ {x y} → y ≈ᴹ 0ᴹ → x *ₗ y ≈ᴹ 0ᴹ -y≈0⇒x*y≈0 {x = x} {y = y} y≈0 = begin +y≈0⇒x*y≈0 {x} {y} y≈0 = begin x *ₗ y ≈⟨ *ₗ-congˡ y≈0 ⟩ x *ₗ 0ᴹ ≈⟨ *ₗ-zeroʳ x ⟩ 0ᴹ ∎ From 9e2ee23fc8aa8c1d7a0383c4ee8e9710c9943610 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 5 Aug 2025 06:54:52 +0100 Subject: [PATCH 10/10] fix: `CHANGELOG` --- CHANGELOG.md | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 04eb3b4d65..5f2a36a419 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -31,13 +31,3 @@ New modules Additions to existing modules ----------------------------- - -* In `Relation.Nullary.Negation.Core` - ```agda - ¬¬-η : A → ¬ ¬ A - ``` - -* In `Relation.Nullary.Negation.Core` - ```agda - ¬¬-η : A → ¬ ¬ A - ```