diff --git a/CHANGELOG.md b/CHANGELOG.md
index d4cb710fe2..9098c29df3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -169,6 +169,8 @@ New modules
 
 * `Relation.Binary.Properties.PartialSetoid` to systematise properties of a PER
 
+* `Relation.Nullary.Recomputable.Core`
+
 Additions to existing modules
 -----------------------------
 
@@ -337,10 +339,17 @@ Additions to existing modules
   <₋-wellFounded   : WellFounded _<_ → WellFounded _<₋_
   ```
 
+* In `Relation.Nullary.Decidable`:
+  ```agda
+  dec-yes-recompute : (a? : Dec A) → .(a : A) → a? ≡ yes (recompute a? a)
+  ```
+
 * In `Relation.Nullary.Decidable.Core`:
   ```agda
   ⊤-dec : Dec {a} ⊤
   ⊥-dec : Dec {a} ⊥
+  recompute-irrelevant-id : (a? : Decidable A) → Irrelevant A →
+                            (a : A) → recompute a? a ≡ a
   ```
 
 * In `Relation.Nullary.Negation.Core`:
@@ -352,6 +361,7 @@ Additions to existing modules
   ```agda
   ⊤-reflects : Reflects (⊤ {a}) true
   ⊥-reflects : Reflects (⊥ {a}) false
+  ```
 
 * In `Data.List.Relation.Unary.AllPairs.Properties`:
   ```agda
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index dab9a4a1d3..e9e16a8c88 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -18,7 +18,7 @@ open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary.Irrelevant using (Irrelevant)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; refl; sym; trans)
 
 private
@@ -77,15 +77,19 @@ dec-false : (a? : Dec A) → ¬ A → does a? ≡ false
 dec-false (false because  _ ) ¬a = refl
 dec-false (true  because [a]) ¬a = contradiction (invert [a]) ¬a
 
+dec-yes-recompute : (a? : Dec A) → .(a : A) → a? ≡ yes (recompute a? a)
+dec-yes-recompute a? a with yes _ ← a? | refl ← dec-true a? (recompute a? a) = refl
+
+dec-yes-irr : (a? : Dec A) → Irrelevant A → (a : A) → a? ≡ yes a
+dec-yes-irr a? irr a =
+  trans (dec-yes-recompute a? a) (≡.cong yes (recompute-irrelevant-id a? irr a))
+
 dec-yes : (a? : Dec A) → A → ∃ λ a → a? ≡ yes a
-dec-yes a? a with yes a′ ← a? | refl ← dec-true a? a = a′ , refl
+dec-yes a? a = _ , dec-yes-recompute a? a
 
 dec-no : (a? : Dec A) (¬a : ¬ A) → a? ≡ no ¬a
 dec-no a? ¬a with no _ ← a? | refl ← dec-false a? ¬a = refl
 
-dec-yes-irr : (a? : Dec A) → Irrelevant A → (a : A) → a? ≡ yes a
-dec-yes-irr a? irr a with a′ , eq ← dec-yes a? a rewrite irr a a′ = eq
-
 ⌊⌋-map′ : ∀ t f (a? : Dec A) → ⌊ map′ {B = B} t f a? ⌋ ≡ ⌊ a? ⌋
 ⌊⌋-map′ t f a? = trans (isYes≗does (map′ t f a?)) (sym (isYes≗does a?))
 
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 9a2f72bf81..47b9e55b55 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -22,8 +22,9 @@ open import Data.Empty.Polymorphic using (⊥)
 open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; const; _$_; flip)
-open import Relation.Nullary.Recomputable as Recomputable
-  hiding (recompute-constant)
+open import Relation.Nullary.Irrelevant using (Irrelevant)
+open import Relation.Nullary.Recomputable.Core as Recomputable
+  using (Recomputable)
 open import Relation.Nullary.Reflects as Reflects
   hiding (recompute; recompute-constant)
 open import Relation.Nullary.Negation.Core
@@ -84,6 +85,9 @@ recompute = Reflects.recompute ∘ proof
 recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
 recompute-constant = Recomputable.recompute-constant ∘ recompute
 
+recompute-irrelevant-id : (a? : Dec A) → Irrelevant A → (a : A) → recompute a? a ≡ a
+recompute-irrelevant-id = Recomputable.recompute-irrelevant-id ∘ recompute
+
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
 
diff --git a/src/Relation/Nullary/Recomputable.agda b/src/Relation/Nullary/Recomputable.agda
index a3a416441e..a7671b339c 100644
--- a/src/Relation/Nullary/Recomputable.agda
+++ b/src/Relation/Nullary/Recomputable.agda
@@ -8,7 +8,6 @@
 
 module Relation.Nullary.Recomputable where
 
-open import Agda.Builtin.Equality using (_≡_; refl)
 open import Data.Empty using (⊥)
 open import Data.Irrelevant using (Irrelevant; irrelevant; [_])
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
@@ -22,22 +21,10 @@ private
     B : Set b
 
 ------------------------------------------------------------------------
--- Definition
---
--- The idea of being 'recomputable' is that, given an *irrelevant* proof
--- of a proposition `A` (signalled by being a value of type `.A`, all of
--- whose inhabitants are identified up to definitional equality, and hence
--- do *not* admit pattern-matching), one may 'promote' such a value to a
--- 'genuine' value of `A`, available for subsequent eg. pattern-matching.
-
-Recomputable : (A : Set a) → Set a
-Recomputable A = .A → A
+-- Re-export
 
-------------------------------------------------------------------------
--- Fundamental property: 'promotion' is a constant function
+open import Relation.Nullary.Recomputable.Core public
 
-recompute-constant : (r : Recomputable A) (p q : A) → r p ≡ r q
-recompute-constant r p q = refl
 
 ------------------------------------------------------------------------
 -- Constructions
diff --git a/src/Relation/Nullary/Recomputable/Core.agda b/src/Relation/Nullary/Recomputable/Core.agda
new file mode 100644
index 0000000000..91d56c0b61
--- /dev/null
+++ b/src/Relation/Nullary/Recomputable/Core.agda
@@ -0,0 +1,45 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Recomputable types and their algebra as Harrop formulas
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Nullary.Recomputable.Core where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Level using (Level)
+open import Relation.Nullary.Irrelevant using (Irrelevant)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+
+------------------------------------------------------------------------
+-- Definition
+--
+-- The idea of being 'recomputable' is that, given an *irrelevant* proof
+-- of a proposition `A` (signalled by being a value of type `.A`, all of
+-- whose inhabitants are identified up to definitional equality, and hence
+-- do *not* admit pattern-matching), one may 'promote' such a value to a
+-- 'genuine' value of `A`, available for subsequent eg. pattern-matching.
+
+Recomputable : (A : Set a) → Set a
+Recomputable A = .A → A
+
+------------------------------------------------------------------------
+-- Fundamental properties:
+-- given `Recomputable A`, `recompute` is a constant function;
+-- moreover, the identity, if `A` is propositionally irrelevant.
+
+module _ (recompute : Recomputable A) where
+
+  recompute-constant : (p q : A) → recompute p ≡ recompute q
+  recompute-constant _ _ = refl
+
+  recompute-irrelevant-id : Irrelevant A → (a : A) → recompute a ≡ a
+  recompute-irrelevant-id irr a = irr (recompute a) a
+