From 9a543dc8eb1abce4853c356de35c870d66a27984 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Wed, 10 Jun 2026 17:53:40 +0200
Subject: [PATCH 1/2] [ re agda/#8557 ] Move irrelevant-recompute and
 corollaries to Unsafe module with --irrelevant-projections flag

---
 src/Relation/Nullary/Recomputable.agda        | 14 ------
 src/Relation/Nullary/Recomputable/Unsafe.agda | 45 +++++++++++++++++++
 2 files changed, 45 insertions(+), 14 deletions(-)
 create mode 100644 src/Relation/Nullary/Recomputable/Unsafe.agda

diff --git a/src/Relation/Nullary/Recomputable.agda b/src/Relation/Nullary/Recomputable.agda
index a7671b339c..715534d92f 100644
--- a/src/Relation/Nullary/Recomputable.agda
+++ b/src/Relation/Nullary/Recomputable.agda
@@ -29,16 +29,6 @@ open import Relation.Nullary.Recomputable.Core public
 ------------------------------------------------------------------------
 -- Constructions
 
--- Irrelevant types are Recomputable
-
-irrelevant-recompute : Recomputable (Irrelevant A)
-irrelevant (irrelevant-recompute [ a ]) = a
-
--- Corollary: so too is ⊥
-
-⊥-recompute : Recomputable ⊥
-⊥-recompute = irrelevant-recompute
-
 _×-recompute_ : Recomputable A → Recomputable B → Recomputable (A × B)
 (rA ×-recompute rB) p = rA (p .proj₁) , rB (p .proj₂)
 
@@ -51,8 +41,4 @@ _→-recompute_ : (A : Set a) → Recomputable B → Recomputable (A → B)
 ∀-recompute : (B : A → Set b) → (∀ {x} → Recomputable (B x)) → Recomputable (∀ {x} → B x)
 ∀-recompute B rB f = rB f
 
--- Corollary: negations are Recomputable
-
-¬-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..295b89f469
--- /dev/null
+++ b/src/Relation/Nullary/Recomputable/Unsafe.agda
@@ -0,0 +1,45 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Recomputable types and their algebra as Harrop formulas
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --irrelevant-projections #-}
+
+module Relation.Nullary.Recomputable.Unsafe 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 (¬_)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+------------------------------------------------------------------------
+-- Re-export
+
+open import Relation.Nullary.Recomputable public
+
+
+------------------------------------------------------------------------
+-- Constructions
+
+-- Irrelevant types are Recomputable
+
+irrelevant-recompute : Recomputable (Irrelevant A)
+irrelevant (irrelevant-recompute a) = irrelevant a
+
+-- Corollary: so too is ⊥
+
+⊥-recompute : Recomputable ⊥
+⊥-recompute = irrelevant-recompute
+
+-- Corollary: negations are Recomputable
+
+¬-recompute : Recomputable (¬ A)
+¬-recompute {A = A} = A →-recompute ⊥-recompute

From 5f11340bdfda744306a07d4db7f8206de12da1e4 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Thu, 11 Jun 2026 10:06:37 +0200
Subject: [PATCH 2/2] =?UTF-8?q?[=20re=20agda/#8557=20]=20Restore=20?=
 =?UTF-8?q?=E2=8A=A5-recompute=20and=20=C2=AC-recompute=20as=20safe?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Relation/Nullary/Recomputable.agda        | 6 ++++++
 src/Relation/Nullary/Recomputable/Unsafe.agda | 9 ---------
 2 files changed, 6 insertions(+), 9 deletions(-)

diff --git a/src/Relation/Nullary/Recomputable.agda b/src/Relation/Nullary/Recomputable.agda
index 715534d92f..7f80ad8f8c 100644
--- a/src/Relation/Nullary/Recomputable.agda
+++ b/src/Relation/Nullary/Recomputable.agda
@@ -29,6 +29,9 @@ open import Relation.Nullary.Recomputable.Core public
 ------------------------------------------------------------------------
 -- Constructions
 
+⊥-recompute : Recomputable ⊥
+⊥-recompute ()
+
 _×-recompute_ : Recomputable A → Recomputable B → Recomputable (A × B)
 (rA ×-recompute rB) p = rA (p .proj₁) , rB (p .proj₂)
 
@@ -41,4 +44,7 @@ _→-recompute_ : (A : Set a) → Recomputable B → Recomputable (A → B)
 ∀-recompute : (B : A → Set b) → (∀ {x} → Recomputable (B x)) → Recomputable (∀ {x} → B x)
 ∀-recompute B rB f = rB f
 
+-- Corollary: negations are Recomputable
 
+¬-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
index 295b89f469..baa32be178 100644
--- a/src/Relation/Nullary/Recomputable/Unsafe.agda
+++ b/src/Relation/Nullary/Recomputable/Unsafe.agda
@@ -34,12 +34,3 @@ open import Relation.Nullary.Recomputable public
 irrelevant-recompute : Recomputable (Irrelevant A)
 irrelevant (irrelevant-recompute a) = irrelevant a
 
--- Corollary: so too is ⊥
-
-⊥-recompute : Recomputable ⊥
-⊥-recompute = irrelevant-recompute
-
--- Corollary: negations are Recomputable
-
-¬-recompute : Recomputable (¬ A)
-¬-recompute {A = A} = A →-recompute ⊥-recompute