From e12010d069e130cfa4d682508b66ed5f75647295 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 19 Oct 2026 16:35:26 +0100 Subject: [PATCH 1/2] [ irrelevant-projections ] clean version of #3012 --- src/Data/Irrelevant.agda | 26 ++++++-------- src/Data/Irrelevant/Unsafe.agda | 35 +++++++++++++++++++ src/Relation/Nullary/Recomputable.agda | 10 ++---- src/Relation/Nullary/Recomputable/Unsafe.agda | 31 ++++++++++++++++ 4 files changed, 79 insertions(+), 23 deletions(-) create mode 100644 src/Data/Irrelevant/Unsafe.agda create mode 100644 src/Relation/Nullary/Recomputable/Unsafe.agda diff --git a/src/Data/Irrelevant.agda b/src/Data/Irrelevant.agda index 11a2c58d2e..e65f30ad82 100644 --- a/src/Data/Irrelevant.agda +++ b/src/Data/Irrelevant.agda @@ -14,7 +14,6 @@ module Data.Irrelevant where open import Level using (Level) -open import Relation.Nullary.Recomputable.Core using (Recomputable) private variable @@ -32,23 +31,20 @@ record Irrelevant (A : Set a) : Set a where open Irrelevant public ------------------------------------------------------------------------ --- Relationship with the . modality: wrapped/unwrapped abstraction +-- Relationship with the . modality: wrapped/unwrapped application -λ∙⁻ : (.A → B) → Irrelevant A → B -λ∙⁻ f [ a ] = f a -{-# INLINE λ∙⁻ #-} +infixr -1 _$⁺_ _$⁻_ -λ∙⁺ : (Irrelevant A → B) → .A → B -λ∙⁺ f a = f [ a ] -{-# INLINE λ∙⁺ #-} +_$⁺_ : (.A → B) → Irrelevant A → B +f $⁺ [ a ] = f a +{-# INLINE _$⁺_ #-} --- Irrelevant types are Recomputable - -recompute : Recomputable (Irrelevant A) -irrelevant (recompute [ a ]) = a +_$⁻_ : (Irrelevant A → B) → .A → B +f $⁻ a = f [ a ] +{-# INLINE _$⁻_ #-} ------------------------------------------------------------------------ --- Algebraic structure: Functor, Appplicative and Monad +-- Algebraic structure: Functor, Appplicative and Monad-like map : (A → B) → Irrelevant A → Irrelevant B map f [ a ] = [ f a ] @@ -61,8 +57,8 @@ _<*>_ : Irrelevant (A → B) → Irrelevant A → Irrelevant B [ f ] <*> [ a ] = [ f a ] infixl 1 _>>=_ -_>>=_ : Irrelevant A → (A → Irrelevant B) → Irrelevant B -[ a ] >>= f = recompute (f a) +_>>=_ : Irrelevant A → (.A → Irrelevant B) → Irrelevant B +[ a ] >>= f = f a ------------------------------------------------------------------------ -- Other functions diff --git a/src/Data/Irrelevant/Unsafe.agda b/src/Data/Irrelevant/Unsafe.agda new file mode 100644 index 0000000000..c89eef4128 --- /dev/null +++ b/src/Data/Irrelevant/Unsafe.agda @@ -0,0 +1,35 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Unsafe properties of the proof irrelevance modality +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --irrelevant-projections #-} + +module Data.Irrelevant.Unsafe where + +open import Data.Irrelevant hiding (_>>=_) +open import Level using (Level) + +private + variable + a b : Level + A : Set a + B : Set b + + +------------------------------------------------------------------------ +-- Irrelevant types are Recomputable + +open import Relation.Nullary.Recomputable.Unsafe public + using () renaming (irrelevant-recompute to recompute) + +------------------------------------------------------------------------ +-- Algebraic structure: Monadic bind and join + +join : Irrelevant (Irrelevant A) → Irrelevant A +join = recompute $⁺_ + +infixl 1 _>>=_ +_>>=_ : Irrelevant A → (A → Irrelevant B) → Irrelevant B +[ a ] >>= f = recompute (f a) diff --git a/src/Relation/Nullary/Recomputable.agda b/src/Relation/Nullary/Recomputable.agda index e67853500a..5feac255b4 100644 --- a/src/Relation/Nullary/Recomputable.agda +++ b/src/Relation/Nullary/Recomputable.agda @@ -20,20 +20,15 @@ private B : Set b ------------------------------------------------------------------------ --- Re-export core definitions +-- Re-export open import Relation.Nullary.Recomputable.Core public --- Irrelevant types are Recomputable - -open import Data.Irrelevant public - using () renaming (recompute to irrelevant-recompute) - ------------------------------------------------------------------------ -- Constructions ⊥-recompute : Recomputable ⊥ -⊥-recompute = irrelevant-recompute +⊥-recompute () _×-recompute_ : Recomputable A → Recomputable B → Recomputable (A × B) (rA ×-recompute rB) p = rA (p .proj₁) , rB (p .proj₂) @@ -51,4 +46,3 @@ _→-recompute_ : (A : Set a) → Recomputable B → Recomputable (A → B) ¬-recompute : Recomputable (¬ A) ¬-recompute {A = A} = A →-recompute ⊥-recompute - diff --git a/src/Relation/Nullary/Recomputable/Unsafe.agda b/src/Relation/Nullary/Recomputable/Unsafe.agda new file mode 100644 index 0000000000..d74c35a17b --- /dev/null +++ b/src/Relation/Nullary/Recomputable/Unsafe.agda @@ -0,0 +1,31 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Irrelevant types are Recomputable +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --irrelevant-projections #-} + +module Relation.Nullary.Recomputable.Unsafe where + +open import Data.Irrelevant using (Irrelevant; irrelevant) +open import Level using (Level) + +private + variable + a : Level + A : Set a + + +------------------------------------------------------------------------ +-- Re-export + +open import Relation.Nullary.Recomputable public + +------------------------------------------------------------------------ +-- Constructions + +-- Irrelevant types are Recomputable + +irrelevant-recompute : Recomputable (Irrelevant A) +irrelevant (irrelevant-recompute a) = irrelevant a From bc4af0185aedbdf5b2f804a724ee0c715fd22511 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 29 Oct 2026 15:54:42 +0000 Subject: [PATCH 2/2] [ changelog ] attempt at a CHANGELOG entry --- CHANGELOG.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 218e84bd3f..a75ff6e090 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -161,6 +161,13 @@ Non-backwards compatible changes the `record POINTWISE` has been lowered to `ℓ₁ ⊔ ℓ₂` given the universe levels `ℓ₁`, resp. `ℓ₂` of the argument relations `_R₁_`, resp. `_R₂_`. +* [Issue #3127](https://github.com/agda/agda-stdlib/pull/3127) + Following an upstream breaking change prompted by a proof of false + ([Agda Issue #8557](https://github.com/agda/agda/issues/8557), + `Irrelevant` cannot be proved to be a monad within `--safe` anymore. + Correspondingly, the relevant definitions have been moved to the new + module `Data.Irrelevant.Unsafe`. + Minor improvements ------------------ @@ -220,6 +227,12 @@ Deprecated names gcd[0,0]≡0 ↦ gcd[i,i]≡∣i∣ ``` +* In `Data.Irrelevant`: + ```agda + λ∙⁻ ↦ _$⁺_ + λ∙⁺ ↦ _$⁻_ + ``` + * In `Data.Nat.GCD`: ```agda gcd[0,0]≡0 ↦ gcd[n,n]≡n