From e4768a93774c84118db759cd41faf1be750d9a0f Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Jun 2025 19:32:52 +0100
Subject: [PATCH 01/16] add: new lemma

---
 CHANGELOG.md                           |  6 ++++++
 src/Relation/Nullary/Recomputable.agda | 15 ++++++++++++---
 2 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9a75fdaee8..eaaf85434c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -323,6 +323,12 @@ Additions to existing modules
   contra-diagonal : (A → ¬ A) → ¬ A
   ```
 
+* In `Relation.Nullary.Recomputable`:
+  ```agda
+  recompute-irr≗id : (promote : Recomputable A) → Nullary.Irrelevant A →
+                     (a : A) → promote a ≡ a
+  ```
+
 * In `Relation.Nullary.Reflects`:
   ```agda
   ⊤-reflects : Reflects (⊤ {a}) true
diff --git a/src/Relation/Nullary/Recomputable.agda b/src/Relation/Nullary/Recomputable.agda
index a3a416441e..124f1517c0 100644
--- a/src/Relation/Nullary/Recomputable.agda
+++ b/src/Relation/Nullary/Recomputable.agda
@@ -14,6 +14,7 @@ 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 (¬_)
+import Relation.Nullary.Irrelevant as Nullary
 
 private
   variable
@@ -34,10 +35,18 @@ Recomputable : (A : Set a) → Set a
 Recomputable A = .A → A
 
 ------------------------------------------------------------------------
--- Fundamental property: 'promotion' is a constant function
+-- Fundamental properties:
+-- 'promotion' is a constant function.
+-- it is moreover the identity, if `A` is propositionally irrelevant.
+
+module _ (promote : Recomputable A) where
+
+  recompute-constant : (p q : A) → promote p ≡ promote q
+  recompute-constant _ _ = refl
+
+  recompute-irr≗id : Nullary.Irrelevant A → (a : A) → promote a ≡ a
+  recompute-irr≗id irr a = irr (promote a) a
 
-recompute-constant : (r : Recomputable A) (p q : A) → r p ≡ r q
-recompute-constant r p q = refl
 
 ------------------------------------------------------------------------
 -- Constructions

From 3890a61c0c71356e2177745de7a8eef96ef47838 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Jun 2025 19:40:42 +0100
Subject: [PATCH 02/16] add: corollary

---
 CHANGELOG.md                             | 2 ++
 src/Relation/Nullary/Decidable/Core.agda | 6 +++++-
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index eaaf85434c..f0ef20fbec 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -316,6 +316,8 @@ Additions to existing modules
   ```agda
   ⊤-dec : Dec {a} ⊤
   ⊥-dec : Dec {a} ⊥
+  recompute-irr≗id : (a? : Decidable A) → Nullary.Irrelevant A →
+                     (a : A) → recompute a? a ≡ a
   ```
 
 * In `Relation.Nullary.Negation.Core`:
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 9a2f72bf81..7293941d23 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.Irrelevant using (Irrelevant)
 open import Relation.Nullary.Recomputable as Recomputable
-  hiding (recompute-constant)
+  hiding (recompute-constant; recompute-irr≗id)
 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-irr≗id : (a? : Dec A) → Irrelevant A → (a : A) → recompute a? a ≡ a
+recompute-irr≗id = Recomputable.recompute-irr≗id ∘ recompute
+
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
 

From bff365eedd8431794e2c0805c58d971e0623abb9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Jun 2025 19:49:52 +0100
Subject: [PATCH 03/16] add: sharper corollary; deprecate old version

---
 CHANGELOG.md                        | 10 ++++++++++
 src/Relation/Nullary/Decidable.agda | 23 ++++++++++++++++++++---
 2 files changed, 30 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f0ef20fbec..85b823e850 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -150,6 +150,11 @@ Deprecated names
   left-inverse ↦ rightInverse
   ```
 
+* In `Relation.Nullary.Decidable`:
+  ```agda
+  dec-yes  ↦ dec-yes-recompute
+  ```
+
 New modules
 -----------
 
@@ -312,6 +317,11 @@ 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} ⊤
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 7c0137b830..70b2ebede2 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -69,14 +69,14 @@ 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 : (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-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-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
+dec-yes-irr a? irr a rewrite dec-yes-recompute a? a | recompute-irr≗id a? irr a = refl
 
 ⌊⌋-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?))
@@ -87,3 +87,20 @@ does-≡ a? (no ¬a) = dec-false a? ¬a
 
 does-⇔ : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b?
 does-⇔ A⇔B a? = does-≡ (map A⇔B a?)
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.3
+
+dec-yes : (a? : Dec A) → A → ∃ λ a → a? ≡ yes a
+dec-yes a? a = _ , dec-yes-recompute a? a
+{-# WARNING_ON_USAGE dec-yes
+"Warning: dec-yes was deprecated in v2.3.
+Please use dec-yes-recompute instead, with a sharper type."
+#-}
+

From daa7a5824e7908556b3904b17f39f6af15b0d236 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 21 Jun 2025 01:21:08 +0100
Subject: [PATCH 04/16] fix: knock-ons

---
 src/Data/Fin/Permutation.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 794b93f76b..1db89452cd 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -26,7 +26,7 @@ open import Function.Base using (_∘_)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary using (does; ¬_; yes; no)
-open import Relation.Nullary.Decidable using (dec-yes; dec-no)
+open import Relation.Nullary.Decidable using (dec-yes-recompute; dec-no)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl; sym; trans; subst; cong; cong₂)
@@ -197,7 +197,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
 
   inverseʳ′ : StrictlyInverseʳ _≡_ to from
   inverseʳ′ k with i ≟ k
-  ... | yes i≡k rewrite proj₂ (dec-yes (j ≟ j) refl) = i≡k
+  ... | yes i≡k rewrite dec-yes-recompute (j ≟ j) refl = i≡k -- rewrite {!dec-yes-recompute (j ≟ j) refl!} = i≡k
   ... | no  i≢k
     with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym
     rewrite dec-no (j ≟ punchIn j (π ⟨$⟩ʳ punchOut i≢k)) j≢punchInⱼπʳpunchOuti≢k
@@ -210,7 +210,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
 
   inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ k with j ≟ k
-  ... | yes j≡k rewrite proj₂ (dec-yes (i ≟ i) refl) = j≡k
+  ... | yes j≡k rewrite dec-yes-recompute (i ≟ i) refl = j≡k
   ... | no  j≢k
     with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym
     rewrite dec-no (i ≟ punchIn i (π ⟨$⟩ˡ punchOut j≢k)) i≢punchInᵢπˡpunchOutj≢k

From e58de493e9184742d9aa35ff4f3a6cee46c79bbe Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 21 Jun 2025 01:38:45 +0100
Subject: [PATCH 05/16] fix: clean-up

---
 src/Data/Fin/Permutation.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 1db89452cd..275594ef96 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -197,7 +197,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
 
   inverseʳ′ : StrictlyInverseʳ _≡_ to from
   inverseʳ′ k with i ≟ k
-  ... | yes i≡k rewrite dec-yes-recompute (j ≟ j) refl = i≡k -- rewrite {!dec-yes-recompute (j ≟ j) refl!} = i≡k
+  ... | yes i≡k rewrite dec-yes-recompute (j ≟ j) refl = i≡k
   ... | no  i≢k
     with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym
     rewrite dec-no (j ≟ punchIn j (π ⟨$⟩ʳ punchOut i≢k)) j≢punchInⱼπʳpunchOuti≢k

From 90d483c3fc679ee007ed71c059824dd6ba1bc045 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 21 Jun 2025 11:35:43 +0100
Subject: [PATCH 06/16] refactor: remove `rewrite` steps

---
 src/Relation/Nullary/Decidable.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 70b2ebede2..3bde71920e 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; cong′)
 
 private
@@ -76,7 +76,8 @@ 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 rewrite dec-yes-recompute a? a | recompute-irr≗id a? irr a = refl
+dec-yes-irr a? irr a =
+  trans (dec-yes-recompute a? a) (≡.cong yes (recompute-irr≗id a? irr a))
 
 ⌊⌋-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?))
@@ -103,4 +104,3 @@ dec-yes a? a = _ , dec-yes-recompute a? a
 "Warning: dec-yes was deprecated in v2.3.
 Please use dec-yes-recompute instead, with a sharper type."
 #-}
-

From 8ea22e2960246c5c2439ebb70fadb99a0837b475 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Jun 2025 11:50:08 +0100
Subject: [PATCH 07/16] fix: `CHANGELOG` note

---
 CHANGELOG.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c76763234b..552e0ad5e0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -152,8 +152,9 @@ Deprecated names
 
 * In `Relation.Nullary.Decidable`:
   ```agda
-  dec-yes  ↦ dec-yes-recompute
+  dec-yes  ↦ dec-yes-recompute : (a? : Dec A) → .(a : A) → a? ≡ yes (recompute a? a)
   ```
+  with a more precise type.
 
 New modules
 -----------

From 82df9d62ed75ed1111be76ab666a0cb134281b6a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Jun 2025 11:56:19 +0100
Subject: [PATCH 08/16] fix: broken qualified `import`

---
 src/Relation/Nullary/Decidable.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index a4bee613df..70635b59c5 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

From ca0a425b1f8e1adaab6e32132b5ca5c4ea4513c1 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Jun 2025 11:56:58 +0100
Subject: [PATCH 09/16] fix: module paramater name

---
 src/Relation/Nullary/Recomputable.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Relation/Nullary/Recomputable.agda b/src/Relation/Nullary/Recomputable.agda
index 124f1517c0..cdf9aeade8 100644
--- a/src/Relation/Nullary/Recomputable.agda
+++ b/src/Relation/Nullary/Recomputable.agda
@@ -39,13 +39,13 @@ Recomputable A = .A → A
 -- 'promotion' is a constant function.
 -- it is moreover the identity, if `A` is propositionally irrelevant.
 
-module _ (promote : Recomputable A) where
+module _ (recompute : Recomputable A) where
 
-  recompute-constant : (p q : A) → promote p ≡ promote q
+  recompute-constant : (p q : A) → recompute p ≡ recompute q
   recompute-constant _ _ = refl
 
-  recompute-irr≗id : Nullary.Irrelevant A → (a : A) → promote a ≡ a
-  recompute-irr≗id irr a = irr (promote a) a
+  recompute-irr≗id : Nullary.Irrelevant A → (a : A) → recompute a ≡ a
+  recompute-irr≗id irr a = irr (recompute a) a
 
 
 ------------------------------------------------------------------------

From d13f8af45582ae36b8f13621d110fba96896d145 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Jun 2025 12:07:40 +0100
Subject: [PATCH 10/16] fix: lemma names

---
 CHANGELOG.md                             | 7 ++++---
 src/Relation/Nullary/Decidable/Core.agda | 4 ++--
 src/Relation/Nullary/Recomputable.agda   | 4 ++--
 3 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 552e0ad5e0..195714694f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -352,7 +352,7 @@ Additions to existing modules
   ```agda
   ⊤-dec : Dec {a} ⊤
   ⊥-dec : Dec {a} ⊥
-  recompute-irr≗id : (a? : Decidable A) → Nullary.Irrelevant A →
+  recompute-irr≗id : (a? : Decidable A) → Irrelevant A →
                      (a : A) → recompute a? a ≡ a
   ```
 
@@ -363,14 +363,15 @@ Additions to existing modules
 
 * In `Relation.Nullary.Recomputable`:
   ```agda
-  recompute-irr≗id : (promote : Recomputable A) → Nullary.Irrelevant A →
-                     (a : A) → promote a ≡ a
+  recompute-irrelevant-id : (recompute : Recomputable A) → Nullary.Irrelevant A →
+                            (a : A) → recompute a ≡ a
   ```
 
 * In `Relation.Nullary.Reflects`:
   ```agda
   ⊤-reflects : Reflects (⊤ {a}) true
   ⊥-reflects : Reflects (⊥ {a}) false
+  ```
 
 * In `Data.List.Relation.Unary.AllPairs.Properties`:
   ```agda
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 7293941d23..45bd39fbb7 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -24,7 +24,7 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; const; _$_; flip)
 open import Relation.Nullary.Irrelevant using (Irrelevant)
 open import Relation.Nullary.Recomputable as Recomputable
-  hiding (recompute-constant; recompute-irr≗id)
+  using (Recomputable)
 open import Relation.Nullary.Reflects as Reflects
   hiding (recompute; recompute-constant)
 open import Relation.Nullary.Negation.Core
@@ -86,7 +86,7 @@ recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a?
 recompute-constant = Recomputable.recompute-constant ∘ recompute
 
 recompute-irr≗id : (a? : Dec A) → Irrelevant A → (a : A) → recompute a? a ≡ a
-recompute-irr≗id = Recomputable.recompute-irr≗id ∘ recompute
+recompute-irr≗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 cdf9aeade8..095d47a89f 100644
--- a/src/Relation/Nullary/Recomputable.agda
+++ b/src/Relation/Nullary/Recomputable.agda
@@ -44,8 +44,8 @@ module _ (recompute : Recomputable A) where
   recompute-constant : (p q : A) → recompute p ≡ recompute q
   recompute-constant _ _ = refl
 
-  recompute-irr≗id : Nullary.Irrelevant A → (a : A) → recompute a ≡ a
-  recompute-irr≗id irr a = irr (recompute a) a
+  recompute-irrelevant-id : Nullary.Irrelevant A → (a : A) → recompute a ≡ a
+  recompute-irrelevant-id irr a = irr (recompute a) a
 
 
 ------------------------------------------------------------------------

From 345b27fa995e57001becd5b6b317b4b1721556cd Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Jun 2025 12:36:15 +0100
Subject: [PATCH 11/16] fix: lemma names

---
 CHANGELOG.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 195714694f..73008380c0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -352,8 +352,8 @@ Additions to existing modules
   ```agda
   ⊤-dec : Dec {a} ⊤
   ⊥-dec : Dec {a} ⊥
-  recompute-irr≗id : (a? : Decidable A) → Irrelevant A →
-                     (a : A) → recompute a? a ≡ a
+  recompute-irrelevant-id : (a? : Decidable A) → Irrelevant A →
+                            (a : A) → recompute a? a ≡ a
   ```
 
 * In `Relation.Nullary.Negation.Core`:

From fb29ac24378e0f41e734969274b9f9a87d8ed091 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Jun 2025 12:58:07 +0100
Subject: [PATCH 12/16] refactor: lift basic definitions and properties out of
 `Recomputable` into `Core`

---
 CHANGELOG.md                                |  4 +-
 src/Relation/Nullary/Recomputable.agda      | 26 +-----------
 src/Relation/Nullary/Recomputable/Core.agda | 45 +++++++++++++++++++++
 3 files changed, 50 insertions(+), 25 deletions(-)
 create mode 100644 src/Relation/Nullary/Recomputable/Core.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 73008380c0..3529e306d7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -175,6 +175,8 @@ New modules
 
 * `Relation.Binary.Properties.PartialSetoid` to systematise properties of a PER
 
+* `Relation.Nullary.Recomputable.Core`
+
 Additions to existing modules
 -----------------------------
 
@@ -363,7 +365,7 @@ Additions to existing modules
 
 * In `Relation.Nullary.Recomputable`:
   ```agda
-  recompute-irrelevant-id : (recompute : Recomputable A) → Nullary.Irrelevant A →
+  recompute-irrelevant-id : (recompute : Recomputable A) → Irrelevant A →
                             (a : A) → recompute a ≡ a
   ```
 
diff --git a/src/Relation/Nullary/Recomputable.agda b/src/Relation/Nullary/Recomputable.agda
index 095d47a89f..a7671b339c 100644
--- a/src/Relation/Nullary/Recomputable.agda
+++ b/src/Relation/Nullary/Recomputable.agda
@@ -8,13 +8,11 @@
 
 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₂)
 open import Level using (Level)
 open import Relation.Nullary.Negation.Core using (¬_)
-import Relation.Nullary.Irrelevant as Nullary
 
 private
   variable
@@ -23,29 +21,9 @@ 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
-
-------------------------------------------------------------------------
--- Fundamental properties:
--- 'promotion' is a constant function.
--- it is 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
+-- Re-export
 
-  recompute-irrelevant-id : Nullary.Irrelevant A → (a : A) → recompute a ≡ a
-  recompute-irrelevant-id irr a = irr (recompute a) a
+open import Relation.Nullary.Recomputable.Core public
 
 
 ------------------------------------------------------------------------
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
+

From b9a6c873c273000b760509b64bb6cae110ba62a6 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Jun 2025 13:00:53 +0100
Subject: [PATCH 13/16] refactor: propagate `import`s

---
 src/Relation/Nullary/Decidable/Core.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 45bd39fbb7..47b9e55b55 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -23,7 +23,7 @@ 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.Irrelevant using (Irrelevant)
-open import Relation.Nullary.Recomputable as Recomputable
+open import Relation.Nullary.Recomputable.Core as Recomputable
   using (Recomputable)
 open import Relation.Nullary.Reflects as Reflects
   hiding (recompute; recompute-constant)
@@ -85,8 +85,8 @@ 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-irr≗id : (a? : Dec A) → Irrelevant A → (a : A) → recompute a? a ≡ a
-recompute-irr≗id = Recomputable.recompute-irrelevant-id ∘ 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.

From 5851516de2af59783a8c08ddc98312b8b487db00 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Jun 2025 13:05:56 +0100
Subject: [PATCH 14/16] fix: lemma name

---
 src/Relation/Nullary/Decidable.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 70635b59c5..5e6145ec85 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -85,7 +85,7 @@ 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 =
-  trans (dec-yes-recompute a? a) (≡.cong yes (recompute-irr≗id a? irr a))
+  trans (dec-yes-recompute a? a) (≡.cong yes (recompute-irrelevant-id a? irr a))
 
 ⌊⌋-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?))

From 06cbaf24dd8260a17dd514ff256b9b2e0061d95c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Jun 2025 15:08:23 +0100
Subject: [PATCH 15/16] refactor: remove deprecation; fix `CHANGELOG`

---
 CHANGELOG.md                        | 12 ------------
 src/Relation/Nullary/Decidable.agda | 25 ++++++-------------------
 2 files changed, 6 insertions(+), 31 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3529e306d7..9098c29df3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -150,12 +150,6 @@ Deprecated names
   left-inverse ↦ rightInverse
   ```
 
-* In `Relation.Nullary.Decidable`:
-  ```agda
-  dec-yes  ↦ dec-yes-recompute : (a? : Dec A) → .(a : A) → a? ≡ yes (recompute a? a)
-  ```
-  with a more precise type.
-
 New modules
 -----------
 
@@ -363,12 +357,6 @@ Additions to existing modules
   contra-diagonal : (A → ¬ A) → ¬ A
   ```
 
-* In `Relation.Nullary.Recomputable`:
-  ```agda
-  recompute-irrelevant-id : (recompute : Recomputable A) → Irrelevant A →
-                            (a : A) → recompute a ≡ a
-  ```
-
 * In `Relation.Nullary.Reflects`:
   ```agda
   ⊤-reflects : Reflects (⊤ {a}) true
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 5e6145ec85..e9e16a8c88 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -80,13 +80,16 @@ 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-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 =
   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 = _ , 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
+
 ⌊⌋-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?))
 
@@ -96,19 +99,3 @@ does-≡ a? (no ¬a) = dec-false a? ¬a
 
 does-⇔ : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b?
 does-⇔ A⇔B a? = does-≡ (map A⇔B a?)
-
-
-------------------------------------------------------------------------
--- DEPRECATED NAMES
-------------------------------------------------------------------------
--- Please use the new names as continuing support for the old names is
--- not guaranteed.
-
--- Version 2.3
-
-dec-yes : (a? : Dec A) → A → ∃ λ a → a? ≡ yes a
-dec-yes a? a = _ , dec-yes-recompute a? a
-{-# WARNING_ON_USAGE dec-yes
-"Warning: dec-yes was deprecated in v2.3.
-Please use dec-yes-recompute instead, with a sharper type."
-#-}

From 574942620fa50118bd76c456e6da982572bceb08 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 29 Jun 2025 12:11:29 +0100
Subject: [PATCH 16/16] refactor: remove coupling with `Data.Fin.Permutation`

---
 src/Data/Fin/Permutation.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 275594ef96..794b93f76b 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -26,7 +26,7 @@ open import Function.Base using (_∘_)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary using (does; ¬_; yes; no)
-open import Relation.Nullary.Decidable using (dec-yes-recompute; dec-no)
+open import Relation.Nullary.Decidable using (dec-yes; dec-no)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl; sym; trans; subst; cong; cong₂)
@@ -197,7 +197,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
 
   inverseʳ′ : StrictlyInverseʳ _≡_ to from
   inverseʳ′ k with i ≟ k
-  ... | yes i≡k rewrite dec-yes-recompute (j ≟ j) refl = i≡k
+  ... | yes i≡k rewrite proj₂ (dec-yes (j ≟ j) refl) = i≡k
   ... | no  i≢k
     with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym
     rewrite dec-no (j ≟ punchIn j (π ⟨$⟩ʳ punchOut i≢k)) j≢punchInⱼπʳpunchOuti≢k
@@ -210,7 +210,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
 
   inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ k with j ≟ k
-  ... | yes j≡k rewrite dec-yes-recompute (i ≟ i) refl = j≡k
+  ... | yes j≡k rewrite proj₂ (dec-yes (i ≟ i) refl) = j≡k
   ... | no  j≢k
     with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym
     rewrite dec-no (i ≟ punchIn i (π ⟨$⟩ˡ punchOut j≢k)) i≢punchInᵢπˡpunchOutj≢k