From 97ab4e0a332cef6a3282a92a71aea1f696ccab65 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 7 Nov 2023 18:41:29 +0000
Subject: [PATCH 01/35] prototype for fixing #2199

---
 src/Data/Empty.agda                      | 14 ++++++++++++++
 src/Relation/Nullary.agda                |  2 +-
 src/Relation/Nullary/Decidable/Core.agda | 13 ++++++-------
 src/Relation/Nullary/Negation/Core.agda  | 11 ++++++++++-
 src/Relation/Nullary/Reflects.agda       | 10 ++++++++++
 5 files changed, 41 insertions(+), 9 deletions(-)

diff --git a/src/Data/Empty.agda b/src/Data/Empty.agda
index 990a9a1632..3fd27ef91d 100644
--- a/src/Data/Empty.agda
+++ b/src/Data/Empty.agda
@@ -30,8 +30,22 @@ private
 
 {-# DISPLAY Irrelevant Empty = ⊥ #-}
 
+------------------------------------------------------------------------
+-- Recomputable/recompute
+
+Recomputable : ∀ {a} (A : Set a) → Set a
+Recomputable A = .A → A
+
+-- ⊥ is Recomputable
+
+⊥-recompute : Recomputable ⊥
+⊥-recompute ()
+
 ------------------------------------------------------------------------
 -- Functions
 
 ⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
 ⊥-elim ()
+
+⊥-elim-irr : ∀ {w} {Whatever : Set w} → .⊥ → Whatever
+⊥-elim-irr bot = ⊥-elim (⊥-recompute bot)
diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index 0b0f83f77b..96df64bca9 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -16,7 +16,7 @@ open import Agda.Builtin.Equality
 -- Re-exports
 
 open import Relation.Nullary.Negation.Core public
-open import Relation.Nullary.Reflects public
+open import Relation.Nullary.Reflects public hiding (recompute)
 open import Relation.Nullary.Decidable.Core public
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index f77613ea65..6884d1a591 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -14,13 +14,12 @@ module Relation.Nullary.Decidable.Core where
 open import Level using (Level; Lift)
 open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
 open import Data.Unit.Base using (⊤)
-open import Data.Empty using (⊥)
-open import Data.Empty.Irrelevant using (⊥-elim)
+open import Data.Empty using (Recomputable; ⊥-elim-irr)
 open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_∘_; const; _$_; flip)
-open import Relation.Nullary.Reflects
-open import Relation.Nullary.Negation.Core
+open import Relation.Nullary.Reflects hiding (recompute)
+open import Relation.Nullary.Negation.Core as Negation
 
 private
   variable
@@ -69,9 +68,9 @@ module _ {A : Set a} where
 
 -- Given an irrelevant proof of a decidable type, a proof can
 -- be recomputed and subsequently used in relevant contexts.
-recompute : Dec A → .A → A
+recompute : Dec A → Recomputable A
 recompute (yes a) _ = a
-recompute (no ¬a) a = ⊥-elim (¬a a)
+recompute (no ¬a) a = weak-contradiction a ¬a
 
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
@@ -171,7 +170,7 @@ proof (map′ A→B B→A (false because [¬a])) = ofⁿ (invert [¬a] ∘ B→A
 
 decidable-stable : Dec A → Stable A
 decidable-stable (yes a) ¬¬a = a
-decidable-stable (no ¬a) ¬¬a = ⊥-elim (¬¬a ¬a)
+decidable-stable (no ¬a) ¬¬a = ⊥-elim-irr (¬¬a ¬a)
 
 ¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A)
 ¬-drop-Dec ¬¬a? = map′ negated-stable contradiction (¬? ¬¬a?)
diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index cbe9ac6da9..61e4e5ae3a 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -9,7 +9,7 @@
 module Relation.Nullary.Negation.Core where
 
 open import Data.Bool.Base using (not)
-open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Empty using (⊥; ⊥-elim; ⊥-elim-irr; Recomputable)
 open import Data.Sum.Base using (_⊎_; [_,_]; inj₁; inj₂)
 open import Function.Base using (flip; _$_; _∘_; const)
 open import Level
@@ -73,3 +73,12 @@ negated-stable ¬¬¬a a = ¬¬¬a (_$ a)
 private
   note : (A → ¬ B) → B → ¬ A
   note = flip
+
+------------------------------------------------------------------------
+-- recompute: negated propositions are recomputable
+
+¬-recompute : Recomputable (¬ A)
+¬-recompute ¬a a = ⊥-elim-irr (¬a a)
+
+weak-contradiction : .A → ¬ A → Whatever
+weak-contradiction a ¬a = ⊥-elim-irr (¬a a)
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 3b301fdbce..0a81a75bd3 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -52,6 +52,16 @@ invert : ∀ {b} → Reflects A b → if b then A else ¬ A
 invert (ofʸ  a) = a
 invert (ofⁿ ¬a) = ¬a
 
+------------------------------------------------------------------------
+-- recompute
+
+-- Given an irrelevant proof of a reflected type, a proof can
+-- be recomputed and subsequently used in relevant contexts.
+
+recompute : ∀ {b} → Reflects A b → Recomputable A
+recompute (ofʸ  a) _ = a
+recompute (ofⁿ ¬a) a = ⊥-elim-irr (¬a a)
+
 ------------------------------------------------------------------------
 -- Interaction with negation, product, sums etc.
 

From 724ff8595775fffeab499a5e85d663a77ea3ab04 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 17 Nov 2023 06:43:15 +0000
Subject: [PATCH 02/35] delegate to
 `Relation.Nullary.Negation.Core.weak-contradiction`

---
 src/Relation/Nullary/Decidable/Core.agda | 4 ++--
 src/Relation/Nullary/Reflects.agda       | 9 ++++-----
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 6884d1a591..109b806b28 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -14,7 +14,7 @@ module Relation.Nullary.Decidable.Core where
 open import Level using (Level; Lift)
 open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
 open import Data.Unit.Base using (⊤)
-open import Data.Empty using (Recomputable; ⊥-elim-irr)
+open import Data.Empty using (Recomputable)
 open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_∘_; const; _$_; flip)
@@ -170,7 +170,7 @@ proof (map′ A→B B→A (false because [¬a])) = ofⁿ (invert [¬a] ∘ B→A
 
 decidable-stable : Dec A → Stable A
 decidable-stable (yes a) ¬¬a = a
-decidable-stable (no ¬a) ¬¬a = ⊥-elim-irr (¬¬a ¬a)
+decidable-stable (no ¬a) ¬¬a = contradiction ¬a ¬¬a
 
 ¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A)
 ¬-drop-Dec ¬¬a? = map′ negated-stable contradiction (¬? ¬¬a?)
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 0a81a75bd3..aa2bf35b81 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -11,12 +11,11 @@ module Relation.Nullary.Reflects where
 open import Agda.Builtin.Equality
 
 open import Data.Bool.Base
-open import Data.Unit.Base using (⊤)
-open import Data.Empty
+open import Data.Empty using (Recomputable)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Level using (Level)
-open import Function.Base using (_$_; _∘_; const; id)
+open import Function.Base using (_$_; _∘_; const; id; flip)
 
 open import Relation.Nullary.Negation.Core
 
@@ -60,7 +59,7 @@ invert (ofⁿ ¬a) = ¬a
 
 recompute : ∀ {b} → Reflects A b → Recomputable A
 recompute (ofʸ  a) _ = a
-recompute (ofⁿ ¬a) a = ⊥-elim-irr (¬a a)
+recompute (ofⁿ ¬a) a = weak-contradiction a ¬a
 
 ------------------------------------------------------------------------
 -- Interaction with negation, product, sums etc.
@@ -94,7 +93,7 @@ _→-reflects_ : ∀ {a b} → Reflects A a → Reflects B b →
                 Reflects (A → B) (not a ∨ b)
 ofʸ  a →-reflects ofʸ  b = ofʸ (const b)
 ofʸ  a →-reflects ofⁿ ¬b = ofⁿ (¬b ∘ (_$ a))
-ofⁿ ¬a →-reflects _      = ofʸ (⊥-elim ∘ ¬a)
+ofⁿ ¬a →-reflects _      = ofʸ (flip contradiction ¬a)
 
 ------------------------------------------------------------------------
 -- Other lemmas

From 1e9375591fb5eae08864d684785ac9de460e39a3 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 17 Nov 2023 08:10:29 +0000
Subject: [PATCH 03/35] refactoring: lift out `Recomputable` in its own right

---
 src/Data/Empty.agda                      |  6 +-----
 src/Relation/Nullary/Decidable.agda      |  7 +++----
 src/Relation/Nullary/Decidable/Core.agda |  2 +-
 src/Relation/Nullary/Negation.agda       |  7 +++----
 src/Relation/Nullary/Negation/Core.agda  | 10 ++++++----
 src/Relation/Nullary/Reflects.agda       |  2 +-
 6 files changed, 15 insertions(+), 19 deletions(-)

diff --git a/src/Data/Empty.agda b/src/Data/Empty.agda
index 3fd27ef91d..4e554f8368 100644
--- a/src/Data/Empty.agda
+++ b/src/Data/Empty.agda
@@ -9,6 +9,7 @@
 module Data.Empty where
 
 open import Data.Irrelevant using (Irrelevant)
+open import Relation.Nullary.Recomputable using (Recomputable)
 
 ------------------------------------------------------------------------
 -- Definition
@@ -31,11 +32,6 @@ private
 {-# DISPLAY Irrelevant Empty = ⊥ #-}
 
 ------------------------------------------------------------------------
--- Recomputable/recompute
-
-Recomputable : ∀ {a} (A : Set a) → Set a
-Recomputable A = .A → A
-
 -- ⊥ is Recomputable
 
 ⊥-recompute : Recomputable ⊥
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index cb5f72b6e0..24485ab51c 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -10,7 +10,6 @@ module Relation.Nullary.Decidable where
 
 open import Level using (Level)
 open import Data.Bool.Base using (true; false; if_then_else_)
-open import Data.Empty using (⊥-elim)
 open import Data.Product.Base using (∃; _,_)
 open import Function.Base
 open import Function.Bundles using
@@ -52,7 +51,7 @@ via-injection inj _≟_ x y = map′ injective cong (to x ≟ to y)
 
 True-↔ : (a? : Dec A) → Irrelevant A → True a? ↔ A
 True-↔ (true  because [a]) irr = mk↔ₛ′ (λ _ → invert [a]) _ (irr (invert [a])) cong′
-True-↔ (false because ofⁿ ¬a) _ = mk↔ₛ′ (λ ()) (invert (ofⁿ ¬a)) (⊥-elim ∘ ¬a) λ ()
+True-↔ (false because ofⁿ ¬a) _ = mk↔ₛ′ (λ ()) (invert (ofⁿ ¬a)) (λ a → contradiction a ¬a) λ ()
 
 ------------------------------------------------------------------------
 -- Result of decidability
@@ -63,11 +62,11 @@ isYes≗does (false because _) = refl
 
 dec-true : (a? : Dec A) → A → does a? ≡ true
 dec-true (true  because   _ ) a = refl
-dec-true (false because [¬a]) a = ⊥-elim (invert [¬a] a)
+dec-true (false because [¬a]) a = contradiction a (invert [¬a])
 
 dec-false : (a? : Dec A) → ¬ A → does a? ≡ false
 dec-false (false because  _ ) ¬a = refl
-dec-false (true  because [a]) ¬a = ⊥-elim (¬a (invert [a]))
+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 dec-true a? a
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 109b806b28..1dcab259de 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -14,10 +14,10 @@ module Relation.Nullary.Decidable.Core where
 open import Level using (Level; Lift)
 open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
 open import Data.Unit.Base using (⊤)
-open import Data.Empty using (Recomputable)
 open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_∘_; const; _$_; flip)
+open import Relation.Nullary.Recomputable
 open import Relation.Nullary.Reflects hiding (recompute)
 open import Relation.Nullary.Negation.Core as Negation
 
diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda
index 4d9ee54208..d033124714 100644
--- a/src/Relation/Nullary/Negation.agda
+++ b/src/Relation/Nullary/Negation.agda
@@ -10,7 +10,6 @@ module Relation.Nullary.Negation where
 
 open import Effect.Monad using (RawMonad; mkRawMonad)
 open import Data.Bool.Base using (Bool; false; true; if_then_else_; not)
-open import Data.Empty using (⊥-elim)
 open import Data.Product.Base as Prod using (_,_; Σ; Σ-syntax; ∃; curry; uncurry)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
 open import Function.Base using (flip; _∘_; const; _∘′_)
@@ -73,7 +72,7 @@ open import Relation.Nullary.Negation.Core public
 -- ⊥).
 
 call/cc : ((A → Whatever) → DoubleNegation A) → DoubleNegation A
-call/cc hyp ¬a = hyp (λ a → ⊥-elim (¬a a)) ¬a
+call/cc hyp ¬a = hyp (λ a → contradiction a ¬a) ¬a
 
 -- The "independence of premise" rule, in the double-negation monad.
 -- It is assumed that the index set (A) is inhabited.
@@ -83,7 +82,7 @@ independence-of-premise {A = A} {B = B} {P = P} q f = ¬¬-map helper ¬¬-exclu
   where
   helper : Dec B → Σ[ x ∈ A ] (B → P x)
   helper (yes p) = Prod.map₂ const (f p)
-  helper (no ¬p) = (q , ⊥-elim ∘′ ¬p)
+  helper (no ¬p) = (q , flip contradiction ¬p)
 
 -- The independence of premise rule for binary sums.
 
@@ -92,7 +91,7 @@ independence-of-premise-⊎ {A = A} {B = B} {C = C} f = ¬¬-map helper ¬¬-exc
   where
   helper : Dec A → (A → B) ⊎ (A → C)
   helper (yes p) = Sum.map const const (f p)
-  helper (no ¬p) = inj₁ (⊥-elim ∘′ ¬p)
+  helper (no ¬p) = inj₁ (flip contradiction ¬p)
 
 private
 
diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 61e4e5ae3a..7fe6043368 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -9,10 +9,11 @@
 module Relation.Nullary.Negation.Core where
 
 open import Data.Bool.Base using (not)
-open import Data.Empty using (⊥; ⊥-elim; ⊥-elim-irr; Recomputable)
+open import Data.Empty using (⊥; ⊥-elim; ⊥-elim-irr)
 open import Data.Sum.Base using (_⊎_; [_,_]; inj₁; inj₂)
 open import Function.Base using (flip; _$_; _∘_; const)
 open import Level
+open import Relation.Nullary.Recomputable
 
 private
   variable
@@ -58,6 +59,9 @@ contradiction₂ (inj₂ b) ¬a ¬b = contradiction b ¬b
 contraposition : (A → B) → ¬ B → ¬ A
 contraposition f ¬b a = contradiction (f a) ¬b
 
+weak-contradiction : .A → ¬ A → Whatever
+weak-contradiction a ¬a = ⊥-elim-irr (¬a a)
+
 -- Everything is stable in the double-negation monad.
 stable : ¬ ¬ Stable A
 stable ¬[¬¬a→a] = ¬[¬¬a→a] (λ ¬¬a → ⊥-elim (¬¬a (¬[¬¬a→a] ∘ const)))
@@ -75,10 +79,8 @@ private
   note = flip
 
 ------------------------------------------------------------------------
--- recompute: negated propositions are recomputable
+-- recompute: negated propositions are Recomputable
 
 ¬-recompute : Recomputable (¬ A)
 ¬-recompute ¬a a = ⊥-elim-irr (¬a a)
 
-weak-contradiction : .A → ¬ A → Whatever
-weak-contradiction a ¬a = ⊥-elim-irr (¬a a)
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index aa2bf35b81..cd723795e2 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -11,13 +11,13 @@ module Relation.Nullary.Reflects where
 open import Agda.Builtin.Equality
 
 open import Data.Bool.Base
-open import Data.Empty using (Recomputable)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Level using (Level)
 open import Function.Base using (_$_; _∘_; const; id; flip)
 
 open import Relation.Nullary.Negation.Core
+open import Relation.Nullary.Recomputable
 
 private
   variable

From e474789c7af5fe92577b96c6f5a54cabfe113812 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 17 Nov 2023 08:40:15 +0000
Subject: [PATCH 04/35] forgot to add this module

---
 src/Relation/Nullary/Recomputable.agda | 42 ++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 src/Relation/Nullary/Recomputable.agda

diff --git a/src/Relation/Nullary/Recomputable.agda b/src/Relation/Nullary/Recomputable.agda
new file mode 100644
index 0000000000..93c126142e
--- /dev/null
+++ b/src/Relation/Nullary/Recomputable.agda
@@ -0,0 +1,42 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Recomputable types and their algebra as Harrop formulas
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Nullary.Recomputable where
+
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Level using (Level)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+------------------------------------------------------------------------
+-- Definition
+
+Recomputable : (A : Set a) → Set a
+Recomputable A = .A → A
+
+------------------------------------------------------------------------
+-- Algebra
+
+_×-recompute_ : Recomputable A → Recomputable B → Recomputable (A × B)
+(rA ×-recompute rB) p = rA (p .proj₁) , rB (p .proj₂)
+
+_→-recompute_ : (A : Set a) → Recomputable B → Recomputable (A → B)
+(A →-recompute rB) f a = rB (f a)
+
+Π-recompute : (B : A → Set b) → (∀ x → Recomputable (B x)) → Recomputable (∀ x → B x)
+Π-recompute B rB f a = rB a (f a)
+
+∀-recompute : (B : A → Set b) → (∀ {x} → Recomputable (B x)) → Recomputable (∀ {x} → B x)
+∀-recompute B rB f = rB f
+
+
+

From 07660c2dffeb03ffe72d48331d90dea14592d16b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 17 Nov 2023 08:49:31 +0000
Subject: [PATCH 05/35] refactoring: tweak

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

diff --git a/src/Relation/Nullary/Recomputable.agda b/src/Relation/Nullary/Recomputable.agda
index 93c126142e..91c16f89c6 100644
--- a/src/Relation/Nullary/Recomputable.agda
+++ b/src/Relation/Nullary/Recomputable.agda
@@ -24,7 +24,7 @@ Recomputable : (A : Set a) → Set a
 Recomputable A = .A → A
 
 ------------------------------------------------------------------------
--- Algebra
+-- Constructions
 
 _×-recompute_ : Recomputable A → Recomputable B → Recomputable (A × B)
 (rA ×-recompute rB) p = rA (p .proj₁) , rB (p .proj₂)
@@ -37,6 +37,3 @@ _→-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
-
-
-

From 7547ba8e819620e54343ee783c0f1bfa15b4ea2f Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 2 Jan 2024 12:52:38 +0000
Subject: [PATCH 06/35] tidying up; added `CHANGELOG`

---
 CHANGELOG.md                             | 20 ++++++++++++++++++++
 src/Data/Empty.agda                      |  2 +-
 src/Relation/Nullary.agda                |  1 +
 src/Relation/Nullary/Decidable.agda      |  4 ++--
 src/Relation/Nullary/Decidable/Core.agda |  7 +++----
 src/Relation/Nullary/Negation.agda       |  6 +++---
 src/Relation/Nullary/Negation/Core.agda  | 10 ++++++++--
 src/Relation/Unary.agda                  |  5 +++--
 8 files changed, 41 insertions(+), 14 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8be73afc66..b4bb89ac80 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -29,9 +29,21 @@ Deprecated names
 New modules
 -----------
 
+* Systematise the use of `Recomputable A = .A → A`:
+  ```agda
+  Relation.Nullary.Recomputable
+  ```
+  with `Recomputable` exported publicly from `Relation.Nullary`.
+
 Additions to existing modules
 -----------------------------
 
+* In `Data.Empty`:
+  ```agda
+  ⊥-recompute : Recomputable ⊥
+  ⊥-elim-irr : ∀ {w} {Whatever : Set w} → .⊥ → Whatever
+  ```
+
 * In `Data.Fin.Properties`:
   ```agda
   nonZeroIndex : Fin n → ℕ.NonZero n
@@ -88,3 +100,11 @@ Additions to existing modules
 
 * In `Function.Bundles`, added `_➙_` as a synonym for `Func` that can
   be used infix.
+
+* Added new definitions in `Relation.Nullary.Negation.Core`:
+  ```agda
+  contradictionᵒ     : ¬ A → A → Whatever
+  weak-contradiction : .A → ¬ A → Whatever
+  irr-contradiction  : .A → .(¬ A) → Whatever
+  ¬-recompute        : Recomputable (¬ A)
+  ```
diff --git a/src/Data/Empty.agda b/src/Data/Empty.agda
index 4e554f8368..5bbd897d92 100644
--- a/src/Data/Empty.agda
+++ b/src/Data/Empty.agda
@@ -44,4 +44,4 @@ private
 ⊥-elim ()
 
 ⊥-elim-irr : ∀ {w} {Whatever : Set w} → .⊥ → Whatever
-⊥-elim-irr bot = ⊥-elim (⊥-recompute bot)
+⊥-elim-irr ()
diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index 96df64bca9..ff583fb317 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -15,6 +15,7 @@ open import Agda.Builtin.Equality
 ------------------------------------------------------------------------
 -- Re-exports
 
+open import Relation.Nullary.Recomputable public using (Recomputable)
 open import Relation.Nullary.Negation.Core public
 open import Relation.Nullary.Reflects public hiding (recompute)
 open import Relation.Nullary.Decidable.Core public
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 24485ab51c..12b1409a02 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -50,8 +50,8 @@ via-injection inj _≟_ x y = map′ injective cong (to x ≟ to y)
 -- A lemma relating True and Dec
 
 True-↔ : (a? : Dec A) → Irrelevant A → True a? ↔ A
-True-↔ (true  because [a]) irr = mk↔ₛ′ (λ _ → invert [a]) _ (irr (invert [a])) cong′
-True-↔ (false because ofⁿ ¬a) _ = mk↔ₛ′ (λ ()) (invert (ofⁿ ¬a)) (λ a → contradiction a ¬a) λ ()
+True-↔ (true  because [a]) irr = let a = invert [a] in mk↔ₛ′ (λ _ → a) _ (irr a) cong′
+True-↔ (false because [¬a]) _  = let ¬a = invert [¬a] in mk↔ₛ′ (λ ()) ¬a (λ a → contradiction a ¬a) λ ()
 
 ------------------------------------------------------------------------
 -- Result of decidability
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 1dcab259de..d8cfd7c0b6 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -18,8 +18,8 @@ open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_∘_; const; _$_; flip)
 open import Relation.Nullary.Recomputable
-open import Relation.Nullary.Reflects hiding (recompute)
-open import Relation.Nullary.Negation.Core as Negation
+open import Relation.Nullary.Reflects as Reflects hiding (recompute)
+open import Relation.Nullary.Negation.Core
 
 private
   variable
@@ -69,8 +69,7 @@ module _ {A : Set a} where
 -- Given an irrelevant proof of a decidable type, a proof can
 -- be recomputed and subsequently used in relevant contexts.
 recompute : Dec A → Recomputable A
-recompute (yes a) _ = a
-recompute (no ¬a) a = weak-contradiction a ¬a
+recompute = Reflects.recompute ∘ proof
 
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda
index d033124714..e52fa021a5 100644
--- a/src/Relation/Nullary/Negation.agda
+++ b/src/Relation/Nullary/Negation.agda
@@ -72,7 +72,7 @@ open import Relation.Nullary.Negation.Core public
 -- ⊥).
 
 call/cc : ((A → Whatever) → DoubleNegation A) → DoubleNegation A
-call/cc hyp ¬a = hyp (λ a → contradiction a ¬a) ¬a
+call/cc hyp ¬a = hyp (contradictionᵒ ¬a) ¬a
 
 -- The "independence of premise" rule, in the double-negation monad.
 -- It is assumed that the index set (A) is inhabited.
@@ -82,7 +82,7 @@ independence-of-premise {A = A} {B = B} {P = P} q f = ¬¬-map helper ¬¬-exclu
   where
   helper : Dec B → Σ[ x ∈ A ] (B → P x)
   helper (yes p) = Prod.map₂ const (f p)
-  helper (no ¬p) = (q , flip contradiction ¬p)
+  helper (no ¬p) = (q , contradictionᵒ ¬p)
 
 -- The independence of premise rule for binary sums.
 
@@ -91,7 +91,7 @@ independence-of-premise-⊎ {A = A} {B = B} {C = C} f = ¬¬-map helper ¬¬-exc
   where
   helper : Dec A → (A → B) ⊎ (A → C)
   helper (yes p) = Sum.map const const (f p)
-  helper (no ¬p) = inj₁ (flip contradiction ¬p)
+  helper (no ¬p) = inj₁ (contradictionᵒ ¬p)
 
 private
 
diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 7fe6043368..befebd26ea 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -9,7 +9,7 @@
 module Relation.Nullary.Negation.Core where
 
 open import Data.Bool.Base using (not)
-open import Data.Empty using (⊥; ⊥-elim; ⊥-elim-irr)
+open import Data.Empty using (⊥; ⊥-elim; ⊥-recompute; ⊥-elim-irr)
 open import Data.Sum.Base using (_⊎_; [_,_]; inj₁; inj₂)
 open import Function.Base using (flip; _$_; _∘_; const)
 open import Level
@@ -52,6 +52,9 @@ _¬-⊎_ = [_,_]
 contradiction : A → ¬ A → Whatever
 contradiction a ¬a = ⊥-elim (¬a a)
 
+contradictionᵒ : ¬ A → A → Whatever
+contradictionᵒ = flip contradiction
+
 contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
 contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a
 contradiction₂ (inj₂ b) ¬a ¬b = contradiction b ¬b
@@ -62,6 +65,9 @@ contraposition f ¬b a = contradiction (f a) ¬b
 weak-contradiction : .A → ¬ A → Whatever
 weak-contradiction a ¬a = ⊥-elim-irr (¬a a)
 
+irr-contradiction : .A → .(¬ A) → Whatever
+irr-contradiction a ¬a = ⊥-elim-irr (¬a a)
+
 -- Everything is stable in the double-negation monad.
 stable : ¬ ¬ Stable A
 stable ¬[¬¬a→a] = ¬[¬¬a→a] (λ ¬¬a → ⊥-elim (¬¬a (¬[¬¬a→a] ∘ const)))
@@ -82,5 +88,5 @@ private
 -- recompute: negated propositions are Recomputable
 
 ¬-recompute : Recomputable (¬ A)
-¬-recompute ¬a a = ⊥-elim-irr (¬a a)
+¬-recompute {A = A} = A →-recompute ⊥-recompute
 
diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index f6d7cb13b0..97fae5fe1b 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -16,6 +16,7 @@ open import Function.Base using (_∘_; _|>_)
 open import Level using (Level; _⊔_; 0ℓ; suc; Lift)
 open import Relation.Nullary.Decidable.Core using (Dec; True)
 open import Relation.Nullary.Negation.Core using (¬_)
+import Relation.Nullary as Nullary
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 private
@@ -178,13 +179,13 @@ Decidable P = ∀ x → Dec (P x)
 -- indistinguishable.
 
 Irrelevant : Pred A ℓ → Set _
-Irrelevant P = ∀ {x} (a : P x) (b : P x) → a ≡ b
+Irrelevant P = ∀ {x} → Nullary.Irrelevant (P x)
 
 -- Recomputability - we can rebuild a relevant proof given an
 -- irrelevant one.
 
 Recomputable : Pred A ℓ → Set _
-Recomputable P = ∀ {x} → .(P x) → P x
+Recomputable P = ∀ {x} → Nullary.Recomputable (P x)
 
 ------------------------------------------------------------------------
 -- Operations on sets

From a5762427131cce9a047210f74c89b04e60059368 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 2 Jan 2024 12:59:22 +0000
Subject: [PATCH 07/35] more tidying up

---
 CHANGELOG.md                       |  2 +-
 src/Relation/Nullary/Reflects.agda | 27 +++++++++++++--------------
 2 files changed, 14 insertions(+), 15 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b4bb89ac80..947a994c95 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -41,7 +41,7 @@ Additions to existing modules
 * In `Data.Empty`:
   ```agda
   ⊥-recompute : Recomputable ⊥
-  ⊥-elim-irr : ∀ {w} {Whatever : Set w} → .⊥ → Whatever
+  ⊥-elim-irr  : .⊥ → Whatever
   ```
 
 * In `Data.Fin.Properties`:
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index cd723795e2..36d58726c7 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -15,7 +15,6 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Level using (Level)
 open import Function.Base using (_$_; _∘_; const; id; flip)
-
 open import Relation.Nullary.Negation.Core
 open import Relation.Nullary.Recomputable
 
@@ -73,34 +72,34 @@ T-reflects false = of id
 
 -- If we can decide A, then we can decide its negation.
 ¬-reflects : ∀ {b} → Reflects A b → Reflects (¬ A) (not b)
-¬-reflects (ofʸ  a) = ofⁿ (_$ a)
-¬-reflects (ofⁿ ¬a) = ofʸ ¬a
+¬-reflects (ofʸ  a) = of (_$ a)
+¬-reflects (ofⁿ ¬a) = of ¬a
 
 -- If we can decide A and Q then we can decide their product
 _×-reflects_ : ∀ {a b} → Reflects A a → Reflects B b →
                Reflects (A × B) (a ∧ b)
-ofʸ  a ×-reflects ofʸ  b = ofʸ (a , b)
-ofʸ  a ×-reflects ofⁿ ¬b = ofⁿ (¬b ∘ proj₂)
-ofⁿ ¬a ×-reflects _      = ofⁿ (¬a ∘ proj₁)
+ofʸ  a ×-reflects ofʸ  b = of (a , b)
+ofʸ  a ×-reflects ofⁿ ¬b = of (¬b ∘ proj₂)
+ofⁿ ¬a ×-reflects _      = of (¬a ∘ proj₁)
 
 _⊎-reflects_ : ∀ {a b} → Reflects A a → Reflects B b →
                Reflects (A ⊎ B) (a ∨ b)
-ofʸ  a ⊎-reflects      _ = ofʸ (inj₁ a)
-ofⁿ ¬a ⊎-reflects ofʸ  b = ofʸ (inj₂ b)
-ofⁿ ¬a ⊎-reflects ofⁿ ¬b = ofⁿ (¬a ¬-⊎ ¬b)
+ofʸ  a ⊎-reflects      _ = of (inj₁ a)
+ofⁿ ¬a ⊎-reflects ofʸ  b = of (inj₂ b)
+ofⁿ ¬a ⊎-reflects ofⁿ ¬b = of (¬a ¬-⊎ ¬b)
 
 _→-reflects_ : ∀ {a b} → Reflects A a → Reflects B b →
                 Reflects (A → B) (not a ∨ b)
-ofʸ  a →-reflects ofʸ  b = ofʸ (const b)
-ofʸ  a →-reflects ofⁿ ¬b = ofⁿ (¬b ∘ (_$ a))
-ofⁿ ¬a →-reflects _      = ofʸ (flip contradiction ¬a)
+ofʸ  a →-reflects ofʸ  b = of (const b)
+ofʸ  a →-reflects ofⁿ ¬b = of (¬b ∘ (_$ a))
+ofⁿ ¬a →-reflects _      = of (contradictionᵒ ¬a)
 
 ------------------------------------------------------------------------
 -- Other lemmas
 
 fromEquivalence : ∀ {b} → (T b → A) → (A → T b) → Reflects A b
-fromEquivalence {b = true}  sound complete = ofʸ (sound _)
-fromEquivalence {b = false} sound complete = ofⁿ complete
+fromEquivalence {b = true}  sound complete = of (sound _)
+fromEquivalence {b = false} sound complete = of complete
 
 -- `Reflects` is deterministic.
 det : ∀ {b b′} → Reflects A b → Reflects A b′ → b ≡ b′

From f853c32ff2a86b210d0e5868503a855b512697ad Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 2 Jan 2024 13:03:29 +0000
Subject: [PATCH 08/35] streamlined `import`s

---
 src/Relation/Unary.agda | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 97fae5fe1b..c9c0b4c8e7 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -14,10 +14,8 @@ open import Data.Product.Base using (_×_; _,_; Σ-syntax; ∃; uncurry; swap)
 open import Data.Sum.Base using (_⊎_; [_,_])
 open import Function.Base using (_∘_; _|>_)
 open import Level using (Level; _⊔_; 0ℓ; suc; Lift)
-open import Relation.Nullary.Decidable.Core using (Dec; True)
-open import Relation.Nullary.Negation.Core using (¬_)
-import Relation.Nullary as Nullary
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Nullary as Nullary using (¬_; Dec; True)
 
 private
   variable

From 3f76aff96288edfe221d3a4f3eb9d992ed915864 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 8 Mar 2024 10:31:18 +0000
Subject: [PATCH 09/35] removed `Recomputable` from `Relation.Nullary`

---
 src/Relation/Nullary.agda | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index 6bb15386e5..6b5fe5c120 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -34,13 +34,6 @@ open import Relation.Nullary.Decidable.Core public
 Irrelevant : Set p → Set p
 Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
 
-------------------------------------------------------------------------
--- Recomputability - we can rebuild a relevant proof given an
--- irrelevant one.
-
-Recomputable : Set p → Set p
-Recomputable P = .P → P
-
 ------------------------------------------------------------------------
 -- Weak decidability
 -- `nothing` is 'don't know'/'give up'; `just` is `yes`/`definitely`

From f786cf05be8f1155a47eff37da5ba7c027f24b6b Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 8 Mar 2024 10:36:08 +0000
Subject: [PATCH 10/35] fixed multiple definitions in `Relation.Unary`

---
 src/Relation/Unary.agda | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 8bafce15c2..29ac237fcb 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -195,18 +195,6 @@ Decidable P = ∀ x → Dec (P x)
 ⌊_⌋ : {P : Pred A ℓ} → Decidable P → Pred A ℓ
 ⌊ P? ⌋ a = Lift _ (True (P? a))
 
--- Irrelevance - any two proofs that an element satifies P are
--- indistinguishable.
-
-Irrelevant : Pred A ℓ → Set _
-Irrelevant P = ∀ {x} → Nullary.Irrelevant (P x)
-
--- Recomputability - we can rebuild a relevant proof given an
--- irrelevant one.
-
-Recomputable : Pred A ℓ → Set _
-Recomputable P = ∀ {x} → Nullary.Recomputable (P x)
-
 ------------------------------------------------------------------------
 -- Operations on sets
 

From 2f31e75d2e67450609b278d74a60e59ebab6afe0 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 25 Mar 2024 18:20:59 +0000
Subject: [PATCH 11/35] reorder `CHANGELOG` entries after merge

---
 CHANGELOG.md | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c303018348..53b1170191 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -62,16 +62,6 @@ New modules
   Algebra.Module.Bundles.Raw
   ```
 
-* Prime factorisation of natural numbers.
-  ```
-  Data.Nat.Primality.Factorisation
-  ```
-
-* Consequences of 'infinite descent' for (accessible elements of) well-founded relations:
-  ```agda
-  Induction.InfiniteDescent
-  ```
-
 * The unique morphism from the initial, resp. terminal, algebra:
   ```agda
   Algebra.Morphism.Construct.Initial
@@ -97,6 +87,11 @@ New modules
   - `⊆-upper-bound-cospan` generalising `⊆-disjoint-union-cospan` from (*)
   ```
 
+* Prime factorisation of natural numbers.
+  ```
+  Data.Nat.Primality.Factorisation
+  ```
+
 * `Data.Vec.Functional.Relation.Binary.Permutation`, defining:
   ```agda
   _↭_ : IRel (Vector A) _
@@ -121,6 +116,11 @@ New modules
   _⇨_ = setoid
   ```
 
+* Consequences of 'infinite descent' for (accessible elements of) well-founded relations:
+  ```agda
+  Induction.InfiniteDescent
+  ```
+
 * Symmetric interior of a binary relation
   ```
   Relation.Binary.Construct.Interior.Symmetric

From 47d7a2ae4bec00fee97ac4f7b41672ffdc251146 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 25 Mar 2024 18:33:37 +0000
Subject: [PATCH 12/35] `contradiciton` via `weak-contradiction`

---
 src/Relation/Nullary/Negation/Core.agda | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index befebd26ea..09d3494254 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -49,8 +49,11 @@ _¬-⊎_ = [_,_]
 ------------------------------------------------------------------------
 -- Uses of negation
 
+weak-contradiction : .A → ¬ A → Whatever
+weak-contradiction a ¬a = ⊥-elim-irr (¬a a)
+
 contradiction : A → ¬ A → Whatever
-contradiction a ¬a = ⊥-elim (¬a a)
+contradiction a = weak-contradiction a
 
 contradictionᵒ : ¬ A → A → Whatever
 contradictionᵒ = flip contradiction
@@ -62,15 +65,9 @@ contradiction₂ (inj₂ b) ¬a ¬b = contradiction b ¬b
 contraposition : (A → B) → ¬ B → ¬ A
 contraposition f ¬b a = contradiction (f a) ¬b
 
-weak-contradiction : .A → ¬ A → Whatever
-weak-contradiction a ¬a = ⊥-elim-irr (¬a a)
-
-irr-contradiction : .A → .(¬ A) → Whatever
-irr-contradiction a ¬a = ⊥-elim-irr (¬a a)
-
 -- Everything is stable in the double-negation monad.
 stable : ¬ ¬ Stable A
-stable ¬[¬¬a→a] = ¬[¬¬a→a] (λ ¬¬a → ⊥-elim (¬¬a (¬[¬¬a→a] ∘ const)))
+stable ¬[¬¬a→a] = ¬[¬¬a→a] λ ¬¬a → {!⊥-elim (¬¬a (¬[¬¬a→a] ∘ const))!}
 
 -- Negated predicates are stable.
 negated-stable : Stable (¬ A)

From bc665c77c9ef1cdf8f14584c94c96a41c4eb446b Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 25 Mar 2024 18:51:27 +0000
Subject: [PATCH 13/35] irrefutable `with`

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

diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 3d4e6e6a6a..8bf333e86b 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -78,8 +78,7 @@ dec-no a? ¬a with dec-false a? ¬a
 dec-no (no _) _ | refl = refl
 
 dec-yes-irr : (a? : Dec A) → Irrelevant A → (a : A) → a? ≡ yes a
-dec-yes-irr a? irr a with dec-yes a? a
-... | a′ , eq rewrite irr a a′ = eq
+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?))

From 323931f4cb3ec483e00dfb338969c49fe7d18179 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 25 Mar 2024 18:52:20 +0000
Subject: [PATCH 14/35] use `of`

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

diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index d8cfd7c0b6..32047d4f6d 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -68,6 +68,7 @@ module _ {A : Set a} where
 
 -- Given an irrelevant proof of a decidable type, a proof can
 -- be recomputed and subsequently used in relevant contexts.
+
 recompute : Dec A → Recomputable A
 recompute = Reflects.recompute ∘ proof
 
@@ -159,8 +160,8 @@ from-no (true  because   _ ) = _
 
 map′ : (A → B) → (B → A) → Dec A → Dec B
 does  (map′ A→B B→A a?)                   = does a?
-proof (map′ A→B B→A (true  because  [a])) = ofʸ (A→B (invert [a]))
-proof (map′ A→B B→A (false because [¬a])) = ofⁿ (invert [¬a] ∘ B→A)
+proof (map′ A→B B→A (true  because  [a])) = of (A→B (invert [a]))
+proof (map′ A→B B→A (false because [¬a])) = of (invert [¬a] ∘ B→A)
 
 ------------------------------------------------------------------------
 -- Relationship with double-negation

From 47c4f8194d77cb93d470ae3d1ac666b939b98147 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 25 Mar 2024 18:54:28 +0000
Subject: [PATCH 15/35] =?UTF-8?q?only=20use=20*irrelevant*=20`=E2=8A=A5-el?=
 =?UTF-8?q?im-irr`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Relation/Nullary/Negation/Core.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 09d3494254..0eee307d07 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -9,7 +9,7 @@
 module Relation.Nullary.Negation.Core where
 
 open import Data.Bool.Base using (not)
-open import Data.Empty using (⊥; ⊥-elim; ⊥-recompute; ⊥-elim-irr)
+open import Data.Empty using (⊥; ⊥-recompute; ⊥-elim-irr)
 open import Data.Sum.Base using (_⊎_; [_,_]; inj₁; inj₂)
 open import Function.Base using (flip; _$_; _∘_; const)
 open import Level
@@ -67,7 +67,7 @@ contraposition f ¬b a = contradiction (f a) ¬b
 
 -- Everything is stable in the double-negation monad.
 stable : ¬ ¬ Stable A
-stable ¬[¬¬a→a] = ¬[¬¬a→a] λ ¬¬a → {!⊥-elim (¬¬a (¬[¬¬a→a] ∘ const))!}
+stable ¬[¬¬a→a] = ¬[¬¬a→a] λ ¬¬a → ⊥-elim-irr (¬¬a (¬[¬¬a→a] ∘ const))
 
 -- Negated predicates are stable.
 negated-stable : Stable (¬ A)

From 3d5f18d74e265051d7cdd9006291546758c5ea1e Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 25 Mar 2024 19:01:39 +0000
Subject: [PATCH 16/35] tightened `import`s

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

diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda
index 453f76cc96..280a9e1833 100644
--- a/src/Relation/Nullary/Negation.agda
+++ b/src/Relation/Nullary/Negation.agda
@@ -8,10 +8,10 @@
 
 module Relation.Nullary.Negation where
 
-open import Effect.Monad using (RawMonad; mkRawMonad)
-open import Data.Bool.Base using (Bool; false; true; if_then_else_; not)
+open import Data.Bool.Base using (Bool; false; true; if_then_else_)
 open import Data.Product.Base as Product using (_,_; Σ; Σ-syntax; ∃; curry; uncurry)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
+open import Effect.Monad using (RawMonad; mkRawMonad)
 open import Function.Base using (flip; _∘_; const; _∘′_)
 open import Level using (Level)
 open import Relation.Nullary.Decidable.Core using (Dec; yes; no; ¬¬-excluded-middle)

From c09da6d4481782894ce43bf0d621fb0dae676894 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 25 Mar 2024 19:04:26 +0000
Subject: [PATCH 17/35] removed `irr-contradiction`

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 53b1170191..49c5cf4eb3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -410,9 +410,8 @@ Additions to existing modules
 
 * Added new definitions in `Relation.Nullary.Negation.Core`:
   ```agda
-  contradictionᵒ     : ¬ A → A → Whatever
   weak-contradiction : .A → ¬ A → Whatever
-  irr-contradiction  : .A → .(¬ A) → Whatever
+  contradictionᵒ     : ¬ A → A → Whatever
   ¬-recompute        : Recomputable (¬ A)
   ```
 
@@ -434,4 +433,4 @@ Additions to existing modules
   ```
 
 * `Tactic.Cong` now provides a marker function, `⌞_⌟`, for user-guided
-  anti-unification. See README.Tactic.Cong for details.
+  anti-unification. See `README.Tactic.Cong` for details.

From 2ca46f0539b2f1770233a94660cd0dddf5d29742 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 26 Mar 2024 17:35:06 +0000
Subject: [PATCH 18/35] inspired by #2329

---
 src/Relation/Nullary/Negation/Core.agda | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 0eee307d07..47526f8d49 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -55,15 +55,15 @@ weak-contradiction a ¬a = ⊥-elim-irr (¬a a)
 contradiction : A → ¬ A → Whatever
 contradiction a = weak-contradiction a
 
-contradictionᵒ : ¬ A → A → Whatever
-contradictionᵒ = flip contradiction
+contradictionᵒ : ¬ A → .A → Whatever
+contradictionᵒ ¬a a = weak-contradiction a ¬a
 
 contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
-contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a
-contradiction₂ (inj₂ b) ¬a ¬b = contradiction b ¬b
+contradiction₂ (inj₁ a) ¬a ¬b = weak-contradiction a ¬a
+contradiction₂ (inj₂ b) ¬a ¬b = weak-contradiction b ¬b
 
 contraposition : (A → B) → ¬ B → ¬ A
-contraposition f ¬b a = contradiction (f a) ¬b
+contraposition f ¬b a = weak-contradiction (f a) ¬b
 
 -- Everything is stable in the double-negation monad.
 stable : ¬ ¬ Stable A

From 2ac735362df70450023c838c6e1b3aebf5e880be Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 26 Mar 2024 17:45:01 +0000
Subject: [PATCH 19/35] conjecture: all uses of `contradiction` can be made
 weak

---
 CHANGELOG.md                             | 1 -
 src/Relation/Nullary/Decidable.agda      | 2 +-
 src/Relation/Nullary/Decidable/Core.agda | 4 ++--
 src/Relation/Nullary/Negation.agda       | 6 +++---
 src/Relation/Nullary/Negation/Core.agda  | 3 ---
 src/Relation/Nullary/Reflects.agda       | 6 +++---
 6 files changed, 9 insertions(+), 13 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 49c5cf4eb3..1ed6974557 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -411,7 +411,6 @@ Additions to existing modules
 * Added new definitions in `Relation.Nullary.Negation.Core`:
   ```agda
   weak-contradiction : .A → ¬ A → Whatever
-  contradictionᵒ     : ¬ A → A → Whatever
   ¬-recompute        : Recomputable (¬ A)
   ```
 
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 8bf333e86b..b7f9d88e9f 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -52,7 +52,7 @@ via-injection inj _≟_ x y = map′ injective cong (to x ≟ to y)
 
 True-↔ : (a? : Dec A) → Irrelevant A → True a? ↔ A
 True-↔ (true  because [a]) irr = let a = invert [a] in mk↔ₛ′ (λ _ → a) _ (irr a) cong′
-True-↔ (false because [¬a]) _  = let ¬a = invert [¬a] in mk↔ₛ′ (λ ()) ¬a (λ a → contradiction a ¬a) λ ()
+True-↔ (false because [¬a]) _  = let ¬a = invert [¬a] in mk↔ₛ′ (λ ()) ¬a (λ a → weak-contradiction a ¬a) λ ()
 
 ------------------------------------------------------------------------
 -- Result of decidability
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 32047d4f6d..21b2e5fc19 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -170,10 +170,10 @@ proof (map′ A→B B→A (false because [¬a])) = of (invert [¬a] ∘ B→A)
 
 decidable-stable : Dec A → Stable A
 decidable-stable (yes a) ¬¬a = a
-decidable-stable (no ¬a) ¬¬a = contradiction ¬a ¬¬a
+decidable-stable (no ¬a) ¬¬a = weak-contradiction ¬a ¬¬a
 
 ¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A)
-¬-drop-Dec ¬¬a? = map′ negated-stable contradiction (¬? ¬¬a?)
+¬-drop-Dec ¬¬a? = map′ negated-stable (λ ¬a ¬¬a → weak-contradiction ¬a ¬¬a) (¬? ¬¬a?)
 
 -- A double-negation-translated variant of excluded middle (or: every
 -- nullary relation is decidable in the double-negation monad).
diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda
index 280a9e1833..8703a85ffa 100644
--- a/src/Relation/Nullary/Negation.agda
+++ b/src/Relation/Nullary/Negation.agda
@@ -72,7 +72,7 @@ open import Relation.Nullary.Negation.Core public
 -- ⊥).
 
 call/cc : ((A → Whatever) → DoubleNegation A) → DoubleNegation A
-call/cc hyp ¬a = hyp (contradictionᵒ ¬a) ¬a
+call/cc hyp ¬a = hyp (λ a → weak-contradiction a ¬a) ¬a
 
 -- The "independence of premise" rule, in the double-negation monad.
 -- It is assumed that the index set (A) is inhabited.
@@ -82,7 +82,7 @@ independence-of-premise {A = A} {B = B} {P = P} q f = ¬¬-map helper ¬¬-exclu
   where
   helper : Dec B → Σ[ x ∈ A ] (B → P x)
   helper (yes p) = Product.map₂ const (f p)
-  helper (no ¬p) = (q , contradictionᵒ ¬p)
+  helper (no ¬p) = (q , λ p → weak-contradiction p ¬p)
 
 -- The independence of premise rule for binary sums.
 
@@ -91,7 +91,7 @@ independence-of-premise-⊎ {A = A} {B = B} {C = C} f = ¬¬-map helper ¬¬-exc
   where
   helper : Dec A → (A → B) ⊎ (A → C)
   helper (yes p) = Sum.map const const (f p)
-  helper (no ¬p) = inj₁ (contradictionᵒ ¬p)
+  helper (no ¬p) = inj₁ (λ p → weak-contradiction p ¬p)
 
 private
 
diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 47526f8d49..09296da751 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -55,9 +55,6 @@ weak-contradiction a ¬a = ⊥-elim-irr (¬a a)
 contradiction : A → ¬ A → Whatever
 contradiction a = weak-contradiction a
 
-contradictionᵒ : ¬ A → .A → Whatever
-contradictionᵒ ¬a a = weak-contradiction a ¬a
-
 contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
 contradiction₂ (inj₁ a) ¬a ¬b = weak-contradiction a ¬a
 contradiction₂ (inj₂ b) ¬a ¬b = weak-contradiction b ¬b
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 36d58726c7..b7ca4a0b6e 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -92,7 +92,7 @@ _→-reflects_ : ∀ {a b} → Reflects A a → Reflects B b →
                 Reflects (A → B) (not a ∨ b)
 ofʸ  a →-reflects ofʸ  b = of (const b)
 ofʸ  a →-reflects ofⁿ ¬b = of (¬b ∘ (_$ a))
-ofⁿ ¬a →-reflects _      = of (contradictionᵒ ¬a)
+ofⁿ ¬a →-reflects _      = of (λ a → weak-contradiction a ¬a)
 
 ------------------------------------------------------------------------
 -- Other lemmas
@@ -104,8 +104,8 @@ fromEquivalence {b = false} sound complete = of complete
 -- `Reflects` is deterministic.
 det : ∀ {b b′} → Reflects A b → Reflects A b′ → b ≡ b′
 det (ofʸ  a) (ofʸ  _) = refl
-det (ofʸ  a) (ofⁿ ¬a) = contradiction a ¬a
-det (ofⁿ ¬a) (ofʸ  a) = contradiction a ¬a
+det (ofʸ  a) (ofⁿ ¬a) = weak-contradiction a ¬a
+det (ofⁿ ¬a) (ofʸ  a) = weak-contradiction a ¬a
 det (ofⁿ ¬a) (ofⁿ  _) = refl
 
 T-reflects-elim : ∀ {a b} → Reflects (T a) b → b ≡ a

From d90b68bff873cdf7e15b6b6537f0bbb88cd4f315 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 27 Mar 2024 07:11:21 +0000
Subject: [PATCH 20/35] second thoughts: reverted last round of chnages

---
 CHANGELOG.md                            | 1 +
 src/Relation/Nullary/Decidable.agda     | 2 +-
 src/Relation/Nullary/Negation.agda      | 6 +++---
 src/Relation/Nullary/Negation/Core.agda | 3 +++
 4 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1ed6974557..49c5cf4eb3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -411,6 +411,7 @@ Additions to existing modules
 * Added new definitions in `Relation.Nullary.Negation.Core`:
   ```agda
   weak-contradiction : .A → ¬ A → Whatever
+  contradictionᵒ     : ¬ A → A → Whatever
   ¬-recompute        : Recomputable (¬ A)
   ```
 
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index b7f9d88e9f..8bf333e86b 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -52,7 +52,7 @@ via-injection inj _≟_ x y = map′ injective cong (to x ≟ to y)
 
 True-↔ : (a? : Dec A) → Irrelevant A → True a? ↔ A
 True-↔ (true  because [a]) irr = let a = invert [a] in mk↔ₛ′ (λ _ → a) _ (irr a) cong′
-True-↔ (false because [¬a]) _  = let ¬a = invert [¬a] in mk↔ₛ′ (λ ()) ¬a (λ a → weak-contradiction a ¬a) λ ()
+True-↔ (false because [¬a]) _  = let ¬a = invert [¬a] in mk↔ₛ′ (λ ()) ¬a (λ a → contradiction a ¬a) λ ()
 
 ------------------------------------------------------------------------
 -- Result of decidability
diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda
index 8703a85ffa..280a9e1833 100644
--- a/src/Relation/Nullary/Negation.agda
+++ b/src/Relation/Nullary/Negation.agda
@@ -72,7 +72,7 @@ open import Relation.Nullary.Negation.Core public
 -- ⊥).
 
 call/cc : ((A → Whatever) → DoubleNegation A) → DoubleNegation A
-call/cc hyp ¬a = hyp (λ a → weak-contradiction a ¬a) ¬a
+call/cc hyp ¬a = hyp (contradictionᵒ ¬a) ¬a
 
 -- The "independence of premise" rule, in the double-negation monad.
 -- It is assumed that the index set (A) is inhabited.
@@ -82,7 +82,7 @@ independence-of-premise {A = A} {B = B} {P = P} q f = ¬¬-map helper ¬¬-exclu
   where
   helper : Dec B → Σ[ x ∈ A ] (B → P x)
   helper (yes p) = Product.map₂ const (f p)
-  helper (no ¬p) = (q , λ p → weak-contradiction p ¬p)
+  helper (no ¬p) = (q , contradictionᵒ ¬p)
 
 -- The independence of premise rule for binary sums.
 
@@ -91,7 +91,7 @@ independence-of-premise-⊎ {A = A} {B = B} {C = C} f = ¬¬-map helper ¬¬-exc
   where
   helper : Dec A → (A → B) ⊎ (A → C)
   helper (yes p) = Sum.map const const (f p)
-  helper (no ¬p) = inj₁ (λ p → weak-contradiction p ¬p)
+  helper (no ¬p) = inj₁ (contradictionᵒ ¬p)
 
 private
 
diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 09296da751..16c43a0875 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -55,6 +55,9 @@ weak-contradiction a ¬a = ⊥-elim-irr (¬a a)
 contradiction : A → ¬ A → Whatever
 contradiction a = weak-contradiction a
 
+contradictionᵒ : ¬ A → A → Whatever
+contradictionᵒ = flip contradiction
+
 contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
 contradiction₂ (inj₁ a) ¬a ¬b = weak-contradiction a ¬a
 contradiction₂ (inj₂ b) ¬a ¬b = weak-contradiction b ¬b

From 2f8c01220c227e717756a89acd255b4822db5ab2 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 27 Mar 2024 10:25:26 +0000
Subject: [PATCH 21/35] lazier pattern analysis cf. #2055

---
 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 35676dfc85..3f8016d0b5 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -170,11 +170,11 @@ proof (map′ A→B B→A (false because [¬a])) = of (invert [¬a] ∘ B→A)
 -- Decidable predicates are stable.
 
 decidable-stable : Dec A → Stable A
-decidable-stable (yes a) ¬¬a = a
-decidable-stable (no ¬a) ¬¬a = contradiction ¬a ¬¬a
+decidable-stable (true  because  [a]) ¬¬a = invert [a]
+decidable-stable (false because [¬a]) ¬¬a = contradiction (invert [¬a]) ¬¬a
 
 ¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A)
-¬-drop-Dec ¬¬a? = map′ negated-stable (λ ¬a ¬¬a → contradiction ¬a ¬¬a) (¬? ¬¬a?)
+¬-drop-Dec ¬¬a? = map′ negated-stable contradiction (¬? ¬¬a?)
 
 -- A double-negation-translated variant of excluded middle (or: every
 -- nullary relation is decidable in the double-negation monad).

From 13d4d4c334d10921dcc0252589c6b54dd6b3f6f0 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 29 Mar 2024 17:21:23 +0000
Subject: [PATCH 22/35] dependencies: uncoupled from `Recomputable`

---
 src/Data/Empty.agda | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/src/Data/Empty.agda b/src/Data/Empty.agda
index 5bbd897d92..49b8450819 100644
--- a/src/Data/Empty.agda
+++ b/src/Data/Empty.agda
@@ -9,7 +9,6 @@
 module Data.Empty where
 
 open import Data.Irrelevant using (Irrelevant)
-open import Relation.Nullary.Recomputable using (Recomputable)
 
 ------------------------------------------------------------------------
 -- Definition
@@ -31,12 +30,6 @@ private
 
 {-# DISPLAY Irrelevant Empty = ⊥ #-}
 
-------------------------------------------------------------------------
--- ⊥ is Recomputable
-
-⊥-recompute : Recomputable ⊥
-⊥-recompute ()
-
 ------------------------------------------------------------------------
 -- Functions
 

From c07a16788e748407dbd2f0604ff8afc60d34a775 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 29 Mar 2024 17:22:46 +0000
Subject: [PATCH 23/35] =?UTF-8?q?moved=20`=E2=8A=A5`=20and=20`=C2=AC=20A`?=
 =?UTF-8?q?=20properties=20to=20this=20one=20place?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/src/Relation/Nullary/Recomputable.agda b/src/Relation/Nullary/Recomputable.agda
index 91c16f89c6..485010df8a 100644
--- a/src/Relation/Nullary/Recomputable.agda
+++ b/src/Relation/Nullary/Recomputable.agda
@@ -8,8 +8,10 @@
 
 module Relation.Nullary.Recomputable where
 
+open import Data.Empty using (⊥)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Level using (Level)
+open import Relation.Nullary.Negation.Core using (¬_)
 
 private
   variable
@@ -26,6 +28,12 @@ Recomputable A = .A → A
 ------------------------------------------------------------------------
 -- Constructions
 
+------------------------------------------------------------------------
+-- Recomputable types are Harrop
+
+⊥-recompute : Recomputable ⊥
+⊥-recompute ()
+
 _×-recompute_ : Recomputable A → Recomputable B → Recomputable (A × B)
 (rA ×-recompute rB) p = rA (p .proj₁) , rB (p .proj₂)
 
@@ -37,3 +45,9 @@ _→-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: negated propositions are Recomputable
+
+¬-recompute : Recomputable (¬ A)
+¬-recompute {A = A} = A →-recompute ⊥-recompute
+

From f3dc80af9006fb457bfa88831d056916f1e9a1ab Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 29 Mar 2024 17:24:32 +0000
Subject: [PATCH 24/35] =?UTF-8?q?removed=20`contradiction=E1=B5=92`=20and?=
 =?UTF-8?q?=20rephrased=20everything=20in=20terms=20of=20`weak-contradicti?=
 =?UTF-8?q?on`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Relation/Nullary/Negation/Core.agda | 19 ++++---------------
 1 file changed, 4 insertions(+), 15 deletions(-)

diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 16c43a0875..eeb9bc073e 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -8,12 +8,10 @@
 
 module Relation.Nullary.Negation.Core where
 
-open import Data.Bool.Base using (not)
-open import Data.Empty using (⊥; ⊥-recompute; ⊥-elim-irr)
+open import Data.Empty using (⊥; ⊥-elim-irr)
 open import Data.Sum.Base using (_⊎_; [_,_]; inj₁; inj₂)
-open import Function.Base using (flip; _$_; _∘_; const)
+open import Function.Base using (flip; _∘_; const)
 open import Level
-open import Relation.Nullary.Recomputable
 
 private
   variable
@@ -55,9 +53,6 @@ weak-contradiction a ¬a = ⊥-elim-irr (¬a a)
 contradiction : A → ¬ A → Whatever
 contradiction a = weak-contradiction a
 
-contradictionᵒ : ¬ A → A → Whatever
-contradictionᵒ = flip contradiction
-
 contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
 contradiction₂ (inj₁ a) ¬a ¬b = weak-contradiction a ¬a
 contradiction₂ (inj₂ b) ¬a ¬b = weak-contradiction b ¬b
@@ -67,11 +62,11 @@ contraposition f ¬b a = weak-contradiction (f a) ¬b
 
 -- Everything is stable in the double-negation monad.
 stable : ¬ ¬ Stable A
-stable ¬[¬¬a→a] = ¬[¬¬a→a] λ ¬¬a → ⊥-elim-irr (¬¬a (¬[¬¬a→a] ∘ const))
+stable ¬[¬¬a→a] = ¬[¬¬a→a] (weak-contradiction (¬[¬¬a→a] ∘ const))
 
 -- Negated predicates are stable.
 negated-stable : Stable (¬ A)
-negated-stable ¬¬¬a a = ¬¬¬a (_$ a)
+negated-stable ¬¬¬a a = ¬¬¬a (weak-contradiction a)
 
 ¬¬-map : (A → B) → ¬ ¬ A → ¬ ¬ B
 ¬¬-map f = contraposition (contraposition f)
@@ -81,9 +76,3 @@ private
   note : (A → ¬ B) → B → ¬ A
   note = flip
 
-------------------------------------------------------------------------
--- recompute: negated propositions are Recomputable
-
-¬-recompute : Recomputable (¬ A)
-¬-recompute {A = A} = A →-recompute ⊥-recompute
-

From b3ce1a6d9bfffe31ad6eeecbbe7dd885d7c04934 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 29 Mar 2024 17:26:12 +0000
Subject: [PATCH 25/35] knock-on consequences; simplified `import`s

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

diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda
index 280a9e1833..5372ac5f5e 100644
--- a/src/Relation/Nullary/Negation.agda
+++ b/src/Relation/Nullary/Negation.agda
@@ -72,7 +72,7 @@ open import Relation.Nullary.Negation.Core public
 -- ⊥).
 
 call/cc : ((A → Whatever) → DoubleNegation A) → DoubleNegation A
-call/cc hyp ¬a = hyp (contradictionᵒ ¬a) ¬a
+call/cc hyp ¬a = hyp (flip contradiction ¬a) ¬a
 
 -- The "independence of premise" rule, in the double-negation monad.
 -- It is assumed that the index set (A) is inhabited.
@@ -82,7 +82,7 @@ independence-of-premise {A = A} {B = B} {P = P} q f = ¬¬-map helper ¬¬-exclu
   where
   helper : Dec B → Σ[ x ∈ A ] (B → P x)
   helper (yes p) = Product.map₂ const (f p)
-  helper (no ¬p) = (q , contradictionᵒ ¬p)
+  helper (no ¬p) = (q , flip contradiction ¬p)
 
 -- The independence of premise rule for binary sums.
 
@@ -91,7 +91,7 @@ independence-of-premise-⊎ {A = A} {B = B} {C = C} f = ¬¬-map helper ¬¬-exc
   where
   helper : Dec A → (A → B) ⊎ (A → C)
   helper (yes p) = Sum.map const const (f p)
-  helper (no ¬p) = inj₁ (contradictionᵒ ¬p)
+  helper (no ¬p) = inj₁ (flip contradiction ¬p)
 
 private
 

From 43bde69e53162ca32333fbdd263707ccbb95d2e6 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 29 Mar 2024 17:32:59 +0000
Subject: [PATCH 26/35] narrow `import`s

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

diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index b7ca4a0b6e..4f0865cd0a 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -15,8 +15,8 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Level using (Level)
 open import Function.Base using (_$_; _∘_; const; id; flip)
-open import Relation.Nullary.Negation.Core
-open import Relation.Nullary.Recomputable
+open import Relation.Nullary.Negation.Core using (¬_; weak-contradiction; _¬-⊎_)
+open import Relation.Nullary.Recomputable using (Recomputable)
 
 private
   variable

From 21a8dbf9007d03b1506deb13b0cabc1765e2acaa Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 29 Mar 2024 17:35:28 +0000
Subject: [PATCH 27/35] narrow `import`s; irrefutable `with`

---
 src/Relation/Nullary/Decidable.agda | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 8bf333e86b..4b28ed43f1 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -9,14 +9,14 @@
 module Relation.Nullary.Decidable where
 
 open import Level using (Level)
-open import Data.Bool.Base using (true; false; if_then_else_)
+open import Data.Bool.Base using (true; false)
 open import Data.Product.Base using (∃; _,_)
-open import Function.Base
 open import Function.Bundles using
   (Injection; module Injection; module Equivalence; _⇔_; _↔_; mk↔ₛ′)
 open import Relation.Binary.Bundles using (Setoid; module Setoid)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary
+open import Relation.Nullary using (Irrelevant)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; sym; trans; cong′)
@@ -70,12 +70,10 @@ 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 dec-true a? a
-dec-yes (yes a′) a | refl = a′ , refl
+dec-yes a? a with yes a′ ← a? | refl ← dec-true a? a = a′ , refl
 
 dec-no : (a? : Dec A) (¬a : ¬ A) → a? ≡ no ¬a
-dec-no a? ¬a with dec-false a? ¬a
-dec-no (no _) _ | refl = refl
+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

From df742519371fb73dd3b1e8f201188dfd8d246654 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 29 Mar 2024 17:40:18 +0000
Subject: [PATCH 28/35] narrow `import`s; `CHANGELOG`

---
 CHANGELOG.md                         | 5 +----
 src/Relation/Binary/Definitions.agda | 4 +---
 2 files changed, 2 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 49c5cf4eb3..b54ae6de92 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -243,7 +243,6 @@ Additions to existing modules
 
 * In `Data.Empty`:
   ```agda
-  ⊥-recompute : Recomputable ⊥
   ⊥-elim-irr  : .⊥ → Whatever
   ```
 
@@ -393,7 +392,7 @@ Additions to existing modules
 * Added new definitions in `Relation.Binary.Definitions`
   ```
   Stable _∼_ = ∀ x y → Nullary.Stable (x ∼ y)
-  Empty  _∼_ = ∀ {x y} → x ∼ y → ⊥
+  Empty  _∼_ = ∀ {x y} → ¬ (x ∼ y)
   ```
 
 * Added new proofs in `Relation.Binary.Properties.Setoid`:
@@ -411,8 +410,6 @@ Additions to existing modules
 * Added new definitions in `Relation.Nullary.Negation.Core`:
   ```agda
   weak-contradiction : .A → ¬ A → Whatever
-  contradictionᵒ     : ¬ A → A → Whatever
-  ¬-recompute        : Recomputable (¬ A)
   ```
 
 * Added new proof in `Relation.Nullary.Decidable`:
diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda
index 0e3f09e443..167b63a8cb 100644
--- a/src/Relation/Binary/Definitions.agda
+++ b/src/Relation/Binary/Definitions.agda
@@ -12,8 +12,6 @@ module Relation.Binary.Definitions where
 
 open import Agda.Builtin.Equality using (_≡_)
 
-open import Data.Empty using (⊥)
-open import Data.Maybe.Base using (Maybe)
 open import Data.Product.Base using (_×_; ∃-syntax)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_on_; flip)
@@ -248,7 +246,7 @@ Universal _∼_ = ∀ x y → x ∼ y
 -- Empty - no elements are related
 
 Empty : REL A B ℓ → Set _
-Empty _∼_ = ∀ {x y} → x ∼ y → ⊥
+Empty _∼_ = ∀ {x y} → ¬ (x ∼ y)
 
 -- Non-emptiness - at least one pair of elements are related.
 

From d8f1e47c80bbf91cfe11433027cf1ad914fc5b09 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 29 Mar 2024 17:45:47 +0000
Subject: [PATCH 29/35] narrow `import`s

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

diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 4f0865cd0a..daac474add 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -14,7 +14,7 @@ open import Data.Bool.Base
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Level using (Level)
-open import Function.Base using (_$_; _∘_; const; id; flip)
+open import Function.Base using (_$_; _∘_; const; id)
 open import Relation.Nullary.Negation.Core using (¬_; weak-contradiction; _¬-⊎_)
 open import Relation.Nullary.Recomputable using (Recomputable)
 

From 77a4e32f0aa34672650d576f90dc3cac750d3adf Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 6 Apr 2024 20:31:27 +0100
Subject: [PATCH 30/35] response to review comments

---
 CHANGELOG.md                            | 11 ++++++++---
 src/Relation/Nullary/Negation/Core.agda | 16 ++++++++--------
 src/Relation/Nullary/Recomputable.agda  |  9 ++++++---
 src/Relation/Nullary/Reflects.agda      | 11 ++++++-----
 4 files changed, 28 insertions(+), 19 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b54ae6de92..b283f5673b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -407,14 +407,19 @@ Additions to existing modules
   WeaklyDecidable : Set _
   ```
 
+* Added new proof in `Relation.Nullary.Decidable`:
+  ```agda
+  ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
+  ```
+
 * Added new definitions in `Relation.Nullary.Negation.Core`:
   ```agda
-  weak-contradiction : .A → ¬ A → Whatever
+  contradiction-irr : .A → ¬ A → Whatever
   ```
 
-* Added new proof in `Relation.Nullary.Decidable`:
+* Added new definitions in `Relation.Nullary.Reflects`:
   ```agda
-  ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
+  recompute : Reflects A b → Recomputable A
   ```
 
 * Added new definitions in `Relation.Unary`
diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index eeb9bc073e..702fb16353 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -47,26 +47,26 @@ _¬-⊎_ = [_,_]
 ------------------------------------------------------------------------
 -- Uses of negation
 
-weak-contradiction : .A → ¬ A → Whatever
-weak-contradiction a ¬a = ⊥-elim-irr (¬a a)
+contradiction-irr : .A → ¬ A → Whatever
+contradiction-irr a ¬a = ⊥-elim-irr (¬a a)
 
 contradiction : A → ¬ A → Whatever
-contradiction a = weak-contradiction a
+contradiction a = contradiction-irr a
 
 contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
-contradiction₂ (inj₁ a) ¬a ¬b = weak-contradiction a ¬a
-contradiction₂ (inj₂ b) ¬a ¬b = weak-contradiction b ¬b
+contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a
+contradiction₂ (inj₂ b) ¬a ¬b = contradiction b ¬b
 
 contraposition : (A → B) → ¬ B → ¬ A
-contraposition f ¬b a = weak-contradiction (f a) ¬b
+contraposition f ¬b a = contradiction (f a) ¬b
 
 -- Everything is stable in the double-negation monad.
 stable : ¬ ¬ Stable A
-stable ¬[¬¬a→a] = ¬[¬¬a→a] (weak-contradiction (¬[¬¬a→a] ∘ const))
+stable ¬[¬¬a→a] = ¬[¬¬a→a] (contradiction (¬[¬¬a→a] ∘ const))
 
 -- Negated predicates are stable.
 negated-stable : Stable (¬ A)
-negated-stable ¬¬¬a a = ¬¬¬a (weak-contradiction a)
+negated-stable ¬¬¬a a = ¬¬¬a (contradiction a)
 
 ¬¬-map : (A → B) → ¬ ¬ A → ¬ ¬ B
 ¬¬-map f = contraposition (contraposition f)
diff --git a/src/Relation/Nullary/Recomputable.agda b/src/Relation/Nullary/Recomputable.agda
index 485010df8a..59a8538909 100644
--- a/src/Relation/Nullary/Recomputable.agda
+++ b/src/Relation/Nullary/Recomputable.agda
@@ -21,6 +21,12 @@ private
 
 ------------------------------------------------------------------------
 -- 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
@@ -28,9 +34,6 @@ Recomputable A = .A → A
 ------------------------------------------------------------------------
 -- Constructions
 
-------------------------------------------------------------------------
--- Recomputable types are Harrop
-
 ⊥-recompute : Recomputable ⊥
 ⊥-recompute ()
 
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index daac474add..581a7dfd21 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -15,7 +15,8 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Level using (Level)
 open import Function.Base using (_$_; _∘_; const; id)
-open import Relation.Nullary.Negation.Core using (¬_; weak-contradiction; _¬-⊎_)
+open import Relation.Nullary.Negation.Core
+  using (¬_; contradiction-irr; contradiction; _¬-⊎_)
 open import Relation.Nullary.Recomputable using (Recomputable)
 
 private
@@ -58,7 +59,7 @@ invert (ofⁿ ¬a) = ¬a
 
 recompute : ∀ {b} → Reflects A b → Recomputable A
 recompute (ofʸ  a) _ = a
-recompute (ofⁿ ¬a) a = weak-contradiction a ¬a
+recompute (ofⁿ ¬a) a = contradiction-irr a ¬a
 
 ------------------------------------------------------------------------
 -- Interaction with negation, product, sums etc.
@@ -92,7 +93,7 @@ _→-reflects_ : ∀ {a b} → Reflects A a → Reflects B b →
                 Reflects (A → B) (not a ∨ b)
 ofʸ  a →-reflects ofʸ  b = of (const b)
 ofʸ  a →-reflects ofⁿ ¬b = of (¬b ∘ (_$ a))
-ofⁿ ¬a →-reflects _      = of (λ a → weak-contradiction a ¬a)
+ofⁿ ¬a →-reflects _      = of (λ a → contradiction a ¬a)
 
 ------------------------------------------------------------------------
 -- Other lemmas
@@ -104,8 +105,8 @@ fromEquivalence {b = false} sound complete = of complete
 -- `Reflects` is deterministic.
 det : ∀ {b b′} → Reflects A b → Reflects A b′ → b ≡ b′
 det (ofʸ  a) (ofʸ  _) = refl
-det (ofʸ  a) (ofⁿ ¬a) = weak-contradiction a ¬a
-det (ofⁿ ¬a) (ofʸ  a) = weak-contradiction a ¬a
+det (ofʸ  a) (ofⁿ ¬a) = contradiction a ¬a
+det (ofⁿ ¬a) (ofʸ  a) = contradiction a ¬a
 det (ofⁿ ¬a) (ofⁿ  _) = refl
 
 T-reflects-elim : ∀ {a b} → Reflects (T a) b → b ≡ a

From 50a89f436b04049460d66248653230672ca96dce Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 8 Apr 2024 11:57:05 +0100
Subject: [PATCH 31/35] irrelevance of `recompute`

---
 CHANGELOG.md                             | 14 +++++++-------
 src/Relation/Nullary/Decidable/Core.agda |  6 +++++-
 src/Relation/Nullary/Reflects.agda       |  3 +++
 3 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b283f5673b..c19d0d327e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -407,6 +407,11 @@ Additions to existing modules
   WeaklyDecidable : Set _
   ```
 
+* Added new proof in `Relation.Nullary.Decidable.Core`:
+  ```agda
+  recompute-irr : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
+  ```
+
 * Added new proof in `Relation.Nullary.Decidable`:
   ```agda
   ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
@@ -419,13 +424,8 @@ Additions to existing modules
 
 * Added new definitions in `Relation.Nullary.Reflects`:
   ```agda
-  recompute : Reflects A b → Recomputable A
-  ```
-
-* Added new definitions in `Relation.Unary`
-  ```
-  Stable          : Pred A ℓ → Set _
-  WeaklyDecidable : Pred A ℓ → Set _
+  recompute     : Reflects A b → Recomputable A
+  recompute-irr : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
   ```
 
 * Added new definitions in `Relation.Unary`
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 3f8016d0b5..24037b6dc2 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -18,9 +18,10 @@ open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_∘_; const; _$_; flip)
 open import Relation.Nullary.Recomputable
-open import Relation.Nullary.Reflects as Reflects hiding (recompute)
+open import Relation.Nullary.Reflects as Reflects hiding (recompute; recompute-irr)
 open import Relation.Nullary.Negation.Core
   using (¬_; Stable; negated-stable; contradiction; DoubleNegation)
+open import Agda.Builtin.Equality using (_≡_)
 
 private
   variable
@@ -73,6 +74,9 @@ module _ {A : Set a} where
 recompute : Dec A → Recomputable A
 recompute = Reflects.recompute ∘ proof
 
+recompute-irr : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
+recompute-irr = Reflects.recompute-irr ∘ proof
+
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
 
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 581a7dfd21..ad244bdc51 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -61,6 +61,9 @@ recompute : ∀ {b} → Reflects A b → Recomputable A
 recompute (ofʸ  a) _ = a
 recompute (ofⁿ ¬a) a = contradiction-irr a ¬a
 
+recompute-irr : ∀ {b} (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
+recompute-irr r p q = refl
+
 ------------------------------------------------------------------------
 -- Interaction with negation, product, sums etc.
 

From 8f6987fde4e826cd6ee5e2153798b8a73f1db2ae Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 8 Apr 2024 12:13:08 +0100
Subject: [PATCH 32/35] knock-on, plus proof of `UIP` from #2149

---
 CHANGELOG.md                              |  6 ++--
 src/Axiom/UniquenessOfIdentityProofs.agda | 36 +++++++++++------------
 src/Relation/Nullary.agda                 |  2 +-
 src/Relation/Nullary/Decidable/Core.agda  |  4 +--
 src/Relation/Nullary/Reflects.agda        |  4 +--
 5 files changed, 25 insertions(+), 27 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c19d0d327e..990474185b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -409,7 +409,7 @@ Additions to existing modules
 
 * Added new proof in `Relation.Nullary.Decidable.Core`:
   ```agda
-  recompute-irr : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
+  recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
   ```
 
 * Added new proof in `Relation.Nullary.Decidable`:
@@ -424,8 +424,8 @@ Additions to existing modules
 
 * Added new definitions in `Relation.Nullary.Reflects`:
   ```agda
-  recompute     : Reflects A b → Recomputable A
-  recompute-irr : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
+  recompute          : Reflects A b → Recomputable A
+  recompute-constant : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
   ```
 
 * Added new definitions in `Relation.Unary`
diff --git a/src/Axiom/UniquenessOfIdentityProofs.agda b/src/Axiom/UniquenessOfIdentityProofs.agda
index 1cefc1a6a1..f64a700ae0 100644
--- a/src/Axiom/UniquenessOfIdentityProofs.agda
+++ b/src/Axiom/UniquenessOfIdentityProofs.agda
@@ -8,15 +8,19 @@
 
 module Axiom.UniquenessOfIdentityProofs where
 
-open import Data.Bool.Base using (true; false)
-open import Data.Empty
-open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary hiding (Irrelevant)
+open import Level using (Level)
+open import Relation.Nullary.Decidable.Core using (recompute; recompute-irr)
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
 
+private
+  variable
+    a : Level
+    A : Set a
+    x y : A
+
 ------------------------------------------------------------------------
 -- Definition
 --
@@ -24,7 +28,7 @@ open import Relation.Binary.PropositionalEquality.Properties
 -- equality are themselves equal. In other words, the equality relation
 -- is irrelevant. Here we define UIP relative to a given type.
 
-UIP : ∀ {a} (A : Set a) → Set a
+UIP : (A : Set a) → Set a
 UIP A = Irrelevant {A = A} _≡_
 
 ------------------------------------------------------------------------
@@ -39,11 +43,11 @@ UIP A = Irrelevant {A = A} _≡_
 -- the image of any other proof.
 
 module Constant⇒UIP
-  {a} {A : Set a} (f : _≡_ {A = A} ⇒ _≡_)
-  (f-constant : ∀ {a b} (p q : a ≡ b) → f p ≡ f q)
+  (f : _≡_ {A = A} ⇒ _≡_)
+  (f-constant : ∀ {x y} (p q : x ≡ y) → f p ≡ f q)
   where
 
-  ≡-canonical : ∀ {a b} (p : a ≡ b) → trans (sym (f refl)) (f p) ≡ p
+  ≡-canonical : (p : x ≡ y) → trans (sym (f refl)) (f p) ≡ p
   ≡-canonical refl = trans-symˡ (f refl)
 
   ≡-irrelevant : UIP A
@@ -59,19 +63,13 @@ module Constant⇒UIP
 -- function over proofs of equality which is constant: it returns the
 -- proof produced by the decision procedure.
 
-module Decidable⇒UIP
-  {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
-  where
+module Decidable⇒UIP (_≟_ : Decidable {A = A} _≡_) where
 
   ≡-normalise : _≡_ {A = A} ⇒ _≡_
-  ≡-normalise {a} {b} a≡b with a ≟ b
-  ... | true  because  [p] = invert [p]
-  ... | false because [¬p] = ⊥-elim (invert [¬p] a≡b)
-
-  ≡-normalise-constant : ∀ {a b} (p q : a ≡ b) → ≡-normalise p ≡ ≡-normalise q
-  ≡-normalise-constant {a} {b} p q with a ≟ b
-  ... | true  because   _  = refl
-  ... | false because [¬p] = ⊥-elim (invert [¬p] p)
+  ≡-normalise {x} {y} x≡y = recompute (x ≟ y) x≡y
+
+  ≡-normalise-constant : (p q : x ≡ y) → ≡-normalise p ≡ ≡-normalise q
+  ≡-normalise-constant {x = x} {y = y} = recompute-irr (x ≟ y)
 
   ≡-irrelevant : UIP A
   ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant
diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index 6b5fe5c120..698fafc879 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -25,7 +25,7 @@ private
 
 open import Relation.Nullary.Recomputable public using (Recomputable)
 open import Relation.Nullary.Negation.Core public
-open import Relation.Nullary.Reflects public hiding (recompute)
+open import Relation.Nullary.Reflects public hiding (recompute; recompute-irr)
 open import Relation.Nullary.Decidable.Core public
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 24037b6dc2..0e4d487b1b 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -74,8 +74,8 @@ module _ {A : Set a} where
 recompute : Dec A → Recomputable A
 recompute = Reflects.recompute ∘ proof
 
-recompute-irr : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
-recompute-irr = Reflects.recompute-irr ∘ proof
+recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
+recompute-constant = Reflects.recompute-constant ∘ proof
 
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index ad244bdc51..830b9d780c 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -61,8 +61,8 @@ recompute : ∀ {b} → Reflects A b → Recomputable A
 recompute (ofʸ  a) _ = a
 recompute (ofⁿ ¬a) a = contradiction-irr a ¬a
 
-recompute-irr : ∀ {b} (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
-recompute-irr r p q = refl
+recompute-constant : ∀ {b} (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
+recompute-constant r p q = refl
 
 ------------------------------------------------------------------------
 -- Interaction with negation, product, sums etc.

From 190a3c78ea4d2fc57a00cd2db492116906f442d9 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 8 Apr 2024 12:15:37 +0100
Subject: [PATCH 33/35] knock-ons from renaming

---
 src/Axiom/UniquenessOfIdentityProofs.agda | 2 +-
 src/Relation/Nullary.agda                 | 2 +-
 src/Relation/Nullary/Decidable/Core.agda  | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Axiom/UniquenessOfIdentityProofs.agda b/src/Axiom/UniquenessOfIdentityProofs.agda
index f64a700ae0..e9dcce745e 100644
--- a/src/Axiom/UniquenessOfIdentityProofs.agda
+++ b/src/Axiom/UniquenessOfIdentityProofs.agda
@@ -9,7 +9,7 @@
 module Axiom.UniquenessOfIdentityProofs where
 
 open import Level using (Level)
-open import Relation.Nullary.Decidable.Core using (recompute; recompute-irr)
+open import Relation.Nullary.Decidable.Core using (recompute; recompute-constant)
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality.Core
diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index 698fafc879..5ea302fd98 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -25,7 +25,7 @@ private
 
 open import Relation.Nullary.Recomputable public using (Recomputable)
 open import Relation.Nullary.Negation.Core public
-open import Relation.Nullary.Reflects public hiding (recompute; recompute-irr)
+open import Relation.Nullary.Reflects public hiding (recompute; recompute-constant)
 open import Relation.Nullary.Decidable.Core public
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 0e4d487b1b..4a633d0cae 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -18,7 +18,7 @@ open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_∘_; const; _$_; flip)
 open import Relation.Nullary.Recomputable
-open import Relation.Nullary.Reflects as Reflects hiding (recompute; recompute-irr)
+open import Relation.Nullary.Reflects as Reflects hiding (recompute; recompute-constant)
 open import Relation.Nullary.Negation.Core
   using (¬_; Stable; negated-stable; contradiction; DoubleNegation)
 open import Agda.Builtin.Equality using (_≡_)

From 7c31399ba6ee577944f83fc28a5d479d10c98c6b Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 8 Apr 2024 12:18:30 +0100
Subject: [PATCH 34/35] knock-on from renaming

---
 src/Axiom/UniquenessOfIdentityProofs.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Axiom/UniquenessOfIdentityProofs.agda b/src/Axiom/UniquenessOfIdentityProofs.agda
index e9dcce745e..89d062766e 100644
--- a/src/Axiom/UniquenessOfIdentityProofs.agda
+++ b/src/Axiom/UniquenessOfIdentityProofs.agda
@@ -69,7 +69,7 @@ module Decidable⇒UIP (_≟_ : Decidable {A = A} _≡_) where
   ≡-normalise {x} {y} x≡y = recompute (x ≟ y) x≡y
 
   ≡-normalise-constant : (p q : x ≡ y) → ≡-normalise p ≡ ≡-normalise q
-  ≡-normalise-constant {x = x} {y = y} = recompute-irr (x ≟ y)
+  ≡-normalise-constant {x = x} {y = y} = recompute-constant (x ≟ y)
 
   ≡-irrelevant : UIP A
   ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant

From 82044bcdadfcf4ffe2e3e7f8ed25bbbd5f37d7cb Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 9 Apr 2024 07:35:45 +0100
Subject: [PATCH 35/35] pushed proof `recompute-constant` to `Recomputable`

---
 src/Relation/Nullary/Decidable/Core.agda | 7 ++++---
 src/Relation/Nullary/Recomputable.agda   | 7 +++++++
 src/Relation/Nullary/Reflects.agda       | 7 ++++---
 3 files changed, 15 insertions(+), 6 deletions(-)

diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 4a633d0cae..9af6cc0078 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -11,17 +11,18 @@
 
 module Relation.Nullary.Decidable.Core where
 
+open import Agda.Builtin.Equality using (_≡_)
 open import Level using (Level; Lift)
 open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
 open import Data.Unit.Polymorphic.Base using (⊤)
 open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_∘_; const; _$_; flip)
-open import Relation.Nullary.Recomputable
+open import Relation.Nullary.Recomputable as Recomputable hiding (recompute-constant)
 open import Relation.Nullary.Reflects as Reflects hiding (recompute; recompute-constant)
 open import Relation.Nullary.Negation.Core
   using (¬_; Stable; negated-stable; contradiction; DoubleNegation)
-open import Agda.Builtin.Equality using (_≡_)
+
 
 private
   variable
@@ -75,7 +76,7 @@ recompute : Dec A → Recomputable A
 recompute = Reflects.recompute ∘ proof
 
 recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
-recompute-constant = Reflects.recompute-constant ∘ proof
+recompute-constant = Recomputable.recompute-constant ∘ recompute
 
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
diff --git a/src/Relation/Nullary/Recomputable.agda b/src/Relation/Nullary/Recomputable.agda
index 59a8538909..cd0b83f113 100644
--- a/src/Relation/Nullary/Recomputable.agda
+++ b/src/Relation/Nullary/Recomputable.agda
@@ -8,6 +8,7 @@
 
 module Relation.Nullary.Recomputable where
 
+open import Agda.Builtin.Equality using (_≡_; refl)
 open import Data.Empty using (⊥)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Level using (Level)
@@ -31,6 +32,12 @@ private
 Recomputable : (A : Set a) → Set a
 Recomputable A = .A → A
 
+------------------------------------------------------------------------
+-- Fundamental property: 'promotion' is a constant function
+
+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/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 830b9d780c..00cee309a7 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -17,7 +17,7 @@ open import Level using (Level)
 open import Function.Base using (_$_; _∘_; const; id)
 open import Relation.Nullary.Negation.Core
   using (¬_; contradiction-irr; contradiction; _¬-⊎_)
-open import Relation.Nullary.Recomputable using (Recomputable)
+open import Relation.Nullary.Recomputable as Recomputable using (Recomputable)
 
 private
   variable
@@ -61,8 +61,9 @@ recompute : ∀ {b} → Reflects A b → Recomputable A
 recompute (ofʸ  a) _ = a
 recompute (ofⁿ ¬a) a = contradiction-irr a ¬a
 
-recompute-constant : ∀ {b} (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
-recompute-constant r p q = refl
+recompute-constant : ∀ {b} (r : Reflects A b) (p q : A) →
+                     recompute r p ≡ recompute r q
+recompute-constant = Recomputable.recompute-constant ∘ recompute
 
 ------------------------------------------------------------------------
 -- Interaction with negation, product, sums etc.