From 8d319f1e2af4ac61a21964d44ad9fd4ec555e26d Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 11 Apr 2026 10:22:22 +0100
Subject: [PATCH 1/2] [ refactor ] Make `Data.Irrelevant.Irrelevant` a proper
 `Monad`

---
 CHANGELOG.md                           | 13 +++++++++++++
 src/Data/Irrelevant.agda               | 25 ++++++++++++++++++++++---
 src/Relation/Nullary/Recomputable.agda | 14 +++++---------
 3 files changed, 40 insertions(+), 12 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 42844d01ef..4af98d621a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -24,6 +24,12 @@ Non-backwards compatible changes
 Minor improvements
 ------------------
 
+* The function `Data.Irrelevant._>>=_` now has the correct type for a 'bind'
+  operation of a `Monad`, by moving the property `irrelevant-recompute`
+  from `Relation.Nullary.Recomputable` to `Data.Irrelevant` as `recompute`,
+  and re-exporting it from the former module with the old name. This should
+  be backwards compatible.
+
 * The function `Data.Nat.LCG.step` is now a manifest field of the record type
   `Generator`, as per the discussion on #2936 and upstream issues/PRs. This is
   consistent with a minimal API for such LCGs, and should be backwards compatible.
@@ -94,6 +100,13 @@ Deprecated names
   ¬∀⟶∃¬-          ↦   ¬∀⇒∃¬
   ```
 
+* In `Data.Irrelevant`:
+  ```agda
+  _$∙⁺_     : (.A → B) → Irrelevant A → B
+  _$∙⁻_     : (Irrelevant A → B) → .A → B
+  recompute : Recomputable (Irrelevant A)
+  ```
+
 * In `Data.List.Fresh.Membership.Setoid.Properties`:
   ```agda
   ≈-subst-∈   ↦   ∈-resp-≈
diff --git a/src/Data/Irrelevant.agda b/src/Data/Irrelevant.agda
index 7701cfc82e..53b8fd4638 100644
--- a/src/Data/Irrelevant.agda
+++ b/src/Data/Irrelevant.agda
@@ -14,6 +14,7 @@
 module Data.Irrelevant where
 
 open import Level using (Level)
+open import Relation.Nullary.Recomputable.Core using (Recomputable)
 
 private
   variable
@@ -31,7 +32,25 @@ record Irrelevant (A : Set a) : Set a where
 open Irrelevant public
 
 ------------------------------------------------------------------------
--- Algebraic structure: Functor, Appplicative and Monad-like
+-- Relationship with the . modality: wrapped/unwrapped application
+
+infixr -1 _$∙⁺_ _$∙⁻_
+
+_$∙⁺_ : (.A → B) → Irrelevant A → B
+f $∙⁺ [ a ] = f a
+{-# INLINE _$∙⁺_ #-}
+
+_$∙⁻_ : (Irrelevant A → B) → .A → B
+f $∙⁻ a = f [ a ]
+{-# INLINE _$∙⁻_ #-}
+
+-- Irrelevant types are Recomputable
+
+recompute : Recomputable (Irrelevant A)
+irrelevant (recompute [ a ]) = a
+
+------------------------------------------------------------------------
+-- Algebraic structure: Functor, Appplicative and Monad
 
 map : (A → B) → Irrelevant A → Irrelevant B
 map f [ a ] = [ f a ]
@@ -44,8 +63,8 @@ _<*>_ : Irrelevant (A → B) → Irrelevant A → Irrelevant B
 [ f ] <*> [ a ] = [ f a ]
 
 infixl 1 _>>=_
-_>>=_ : Irrelevant A → (.A → Irrelevant B) → Irrelevant B
-[ a ] >>= f = f a
+_>>=_ : Irrelevant A → (A → Irrelevant B) → Irrelevant B
+[ a ] >>= f = recompute (f a)
 
 ------------------------------------------------------------------------
 -- Other functions
diff --git a/src/Relation/Nullary/Recomputable.agda b/src/Relation/Nullary/Recomputable.agda
index a7671b339c..f4c5a74939 100644
--- a/src/Relation/Nullary/Recomputable.agda
+++ b/src/Relation/Nullary/Recomputable.agda
@@ -9,7 +9,6 @@
 module Relation.Nullary.Recomputable where
 
 open import Data.Empty using (⊥)
-open import Data.Irrelevant using (Irrelevant; irrelevant; [_])
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Level using (Level)
 open import Relation.Nullary.Negation.Core using (¬_)
@@ -21,20 +20,17 @@ private
     B : Set b
 
 ------------------------------------------------------------------------
--- Re-export
+-- Re-export core definitions
 
 open import Relation.Nullary.Recomputable.Core public
 
-
-------------------------------------------------------------------------
--- Constructions
-
 -- Irrelevant types are Recomputable
 
-irrelevant-recompute : Recomputable (Irrelevant A)
-irrelevant (irrelevant-recompute [ a ]) = a
+open import Data.Irrelevant public
+  using () renaming (recompute to irrelevant-recompute)
 
--- Corollary: so too is ⊥
+------------------------------------------------------------------------
+-- Constructions
 
 ⊥-recompute : Recomputable ⊥
 ⊥-recompute = irrelevant-recompute

From a563cddb69e1c088f1db8a97787d551acf3c228d Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 18 Apr 2026 14:53:48 +0100
Subject: [PATCH 2/2] fix: names

---
 CHANGELOG.md             |  4 ++--
 src/Data/Irrelevant.agda | 16 +++++++---------
 2 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4af98d621a..f85f2c9285 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -102,8 +102,8 @@ Deprecated names
 
 * In `Data.Irrelevant`:
   ```agda
-  _$∙⁺_     : (.A → B) → Irrelevant A → B
-  _$∙⁻_     : (Irrelevant A → B) → .A → B
+  λ∙⁻       : (.A → B) → Irrelevant A → B
+  λ∙⁺       : (Irrelevant A → B) → .A → B
   recompute : Recomputable (Irrelevant A)
   ```
 
diff --git a/src/Data/Irrelevant.agda b/src/Data/Irrelevant.agda
index 53b8fd4638..d23bfa02b6 100644
--- a/src/Data/Irrelevant.agda
+++ b/src/Data/Irrelevant.agda
@@ -32,17 +32,15 @@ record Irrelevant (A : Set a) : Set a where
 open Irrelevant public
 
 ------------------------------------------------------------------------
--- Relationship with the . modality: wrapped/unwrapped application
+-- Relationship with the . modality: wrapped/unwrapped abstraction
 
-infixr -1 _$∙⁺_ _$∙⁻_
+λ∙⁻ : (.A → B) → Irrelevant A → B
+λ∙⁻ f [ a ] = f a
+{-# INLINE λ∙⁻ #-}
 
-_$∙⁺_ : (.A → B) → Irrelevant A → B
-f $∙⁺ [ a ] = f a
-{-# INLINE _$∙⁺_ #-}
-
-_$∙⁻_ : (Irrelevant A → B) → .A → B
-f $∙⁻ a = f [ a ]
-{-# INLINE _$∙⁻_ #-}
+λ∙⁺ : (Irrelevant A → B) → .A → B
+λ∙⁺ f a = f [ a ]
+{-# INLINE λ∙⁺ #-}
 
 -- Irrelevant types are Recomputable