From b13a032851a99c0abd9ebc55748ad0cbd1e0060d Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Wed, 5 Jun 2024 16:28:11 +0100
Subject: [PATCH] Adds `Relation.Nullary.Recomputable` plus consequences
 (#2243)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* prototype for fixing #2199

* delegate to `Relation.Nullary.Negation.Core.weak-contradiction`

* refactoring: lift out `Recomputable` in its own right

* forgot to add this module

* refactoring: tweak

* tidying up; added `CHANGELOG`

* more tidying up

* streamlined `import`s

* removed `Recomputable` from `Relation.Nullary`

* fixed multiple definitions in `Relation.Unary`

* reorder `CHANGELOG` entries after merge

* `contradiciton` via `weak-contradiction`

* irrefutable `with`

* use `of`

* only use *irrelevant* `⊥-elim-irr`

* tightened `import`s

* removed `irr-contradiction`

* inspired by #2329

* conjecture: all uses of `contradiction` can be made weak

* second thoughts: reverted last round of chnages

* lazier pattern analysis cf. #2055

* dependencies: uncoupled from `Recomputable`

* moved `⊥` and `¬ A` properties to this one place

* removed `contradictionᵒ` and rephrased everything in terms of `weak-contradiction`

* knock-on consequences; simplified `import`s

* narrow `import`s

* narrow `import`s; irrefutable `with`

* narrow `import`s; `CHANGELOG`

* narrow `import`s

* response to review comments

* irrelevance of `recompute`

* knock-on, plus proof of `UIP` from #2149

* knock-ons from renaming

* knock-on from renaming

* pushed proof `recompute-constant` to `Recomputable`
---
 CHANGELOG.md                              | 78 +++++++++++++++--------
 src/Axiom/UniquenessOfIdentityProofs.agda | 35 +++++-----
 src/Data/Empty.agda                       |  3 +
 src/Relation/Binary/Definitions.agda      |  4 +-
 src/Relation/Nullary.agda                 | 10 +--
 src/Relation/Nullary/Decidable.agda       | 24 +++----
 src/Relation/Nullary/Decidable/Core.agda  | 23 ++++---
 src/Relation/Nullary/Negation.agda        | 11 ++--
 src/Relation/Nullary/Negation/Core.agda   | 15 +++--
 src/Relation/Nullary/Recomputable.agda    | 63 ++++++++++++++++++
 src/Relation/Nullary/Reflects.agda        | 45 ++++++++-----
 src/Relation/Unary.agda                   |  3 +-
 12 files changed, 207 insertions(+), 107 deletions(-)
 create mode 100644 src/Relation/Nullary/Recomputable.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 94a0fd3263..e02ff2dc30 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -118,25 +118,9 @@ New modules
   Algebra.Module.Bundles.Raw
   ```
 
-* Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid):
-  ```
-  Data.List.Relation.Binary.Equality.Setoid.Properties
-  ```
-
-* Refactoring of `Data.List.Base.{scanr|scanl}` and their properties:
-  ```
-  Data.List.Scans.Base
-  Data.List.Scans.Properties
-  ```
-
-* Prime factorisation of natural numbers.
-  ```
-  Data.Nat.Primality.Factorisation
-  ```
-
-* Consequences of 'infinite descent' for (accessible elements of) well-founded relations:
+* Nagata's construction of the "idealization of a module":
   ```agda
-  Induction.InfiniteDescent
+  Algebra.Module.Construct.Idealization
   ```
 
 * The unique morphism from the initial, resp. terminal, algebra:
@@ -145,9 +129,22 @@ New modules
   Algebra.Morphism.Construct.Terminal
   ```
 
-* Nagata's construction of the "idealization of a module":
+* Pointwise and equality relations over indexed containers:
   ```agda
-  Algebra.Module.Construct.Idealization
+  Data.Container.Indexed.Relation.Binary.Pointwise
+  Data.Container.Indexed.Relation.Binary.Pointwise.Properties
+  Data.Container.Indexed.Relation.Binary.Equality.Setoid
+  ```
+
+* Refactoring of `Data.List.Base.{scanr|scanl}` and their properties:
+  ```
+  Data.List.Scans.Base
+  Data.List.Scans.Properties
+  ```
+
+* Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid):
+  ```
+  Data.List.Relation.Binary.Equality.Setoid.Properties
   ```
 
 * `Data.List.Relation.Binary.Sublist.Propositional.Slice`
@@ -155,6 +152,12 @@ New modules
   and adding new functions:
   - `⊆-upper-bound-is-cospan` generalising `⊆-disjoint-union-is-cospan` from (*)
   - `⊆-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
@@ -180,6 +183,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
@@ -190,12 +198,11 @@ New modules
   Relation.Binary.Properties.DecSetoid
   ```
 
-* Pointwise and equality relations over indexed containers:
+* Systematise the use of `Recomputable A = .A → A`:
   ```agda
-  Data.Container.Indexed.Relation.Binary.Pointwise
-  Data.Container.Indexed.Relation.Binary.Pointwise.Properties
-  Data.Container.Indexed.Relation.Binary.Equality.Setoid
+  Relation.Nullary.Recomputable
   ```
+  with `Recomputable` exported publicly from `Relation.Nullary`.
 
 * New IO primitives to handle buffering
   ```agda
@@ -372,6 +379,11 @@ Additions to existing modules
   Subtrees o c = (r : Response c) → X (next c r)
   ```
 
+* In `Data.Empty`:
+  ```agda
+  ⊥-elim-irr  : .⊥ → Whatever
+  ```
+
 * In `Data.Fin.Properties`:
   ```agda
   nonZeroIndex : Fin n → ℕ.NonZero n
@@ -674,7 +686,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`:
@@ -690,11 +702,27 @@ Additions to existing modules
   WeaklyDecidable : Set _
   ```
 
+* Added new proof in `Relation.Nullary.Decidable.Core`:
+  ```agda
+  recompute-constant : (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? ⌋
   ```
 
+* Added new definitions in `Relation.Nullary.Negation.Core`:
+  ```agda
+  contradiction-irr : .A → ¬ A → Whatever
+  ```
+
+* Added new definitions in `Relation.Nullary.Reflects`:
+  ```agda
+  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`
   ```
   Stable          : Pred A ℓ → Set _
diff --git a/src/Axiom/UniquenessOfIdentityProofs.agda b/src/Axiom/UniquenessOfIdentityProofs.agda
index 74463fe557..670941afb1 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-constant)
 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,14 @@ 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} (_≟_ : DecidableEquality A)
+module Decidable⇒UIP (_≟_ : DecidableEquality 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-constant (x ≟ y)
 
   ≡-irrelevant : UIP A
   ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant
diff --git a/src/Data/Empty.agda b/src/Data/Empty.agda
index 19754e8c7d..d2647a1f18 100644
--- a/src/Data/Empty.agda
+++ b/src/Data/Empty.agda
@@ -35,3 +35,6 @@ private
 
 ⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
 ⊥-elim ()
+
+⊥-elim-irr : ∀ {w} {Whatever : Set w} → .⊥ → Whatever
+⊥-elim-irr ()
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.
 
diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index 92e0607f4d..5ea302fd98 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -23,8 +23,9 @@ private
 ------------------------------------------------------------------------
 -- Re-exports
 
+open import Relation.Nullary.Recomputable public using (Recomputable)
 open import Relation.Nullary.Negation.Core public
-open import Relation.Nullary.Reflects public
+open import Relation.Nullary.Reflects public hiding (recompute; recompute-constant)
 open import Relation.Nullary.Decidable.Core public
 
 ------------------------------------------------------------------------
@@ -33,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`
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 4335a5df5a..4b28ed43f1 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -9,15 +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.Empty using (⊥-elim)
+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′)
@@ -52,8 +51,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)) (⊥-elim ∘ ¬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
@@ -64,23 +63,20 @@ 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
-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 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?))
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 83da26e51b..9af6cc0078 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -11,17 +11,19 @@
 
 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.Empty.Irrelevant using (⊥-elim)
 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.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)
 
+
 private
   variable
     a b : Level
@@ -69,9 +71,12 @@ 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 (yes a) _ = a
-recompute (no ¬a) a = ⊥-elim (¬a a)
+
+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 = Recomputable.recompute-constant ∘ recompute
 
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
@@ -161,8 +166,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
@@ -170,8 +175,8 @@ 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 contradiction (¬? ¬¬a?)
diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda
index b9116504ec..5372ac5f5e 100644
--- a/src/Relation/Nullary/Negation.agda
+++ b/src/Relation/Nullary/Negation.agda
@@ -8,11 +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.Empty using (⊥-elim)
+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)
@@ -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 (flip contradiction ¬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) = Product.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 cbe9ac6da9..702fb16353 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -8,10 +8,9 @@
 
 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-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
 
 private
@@ -48,8 +47,11 @@ _¬-⊎_ = [_,_]
 ------------------------------------------------------------------------
 -- Uses of negation
 
+contradiction-irr : .A → ¬ A → Whatever
+contradiction-irr a ¬a = ⊥-elim-irr (¬a a)
+
 contradiction : A → ¬ A → Whatever
-contradiction a ¬a = ⊥-elim (¬a a)
+contradiction a = contradiction-irr a
 
 contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
 contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a
@@ -60,11 +62,11 @@ 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] (contradiction (¬[¬¬a→a] ∘ const))
 
 -- Negated predicates are stable.
 negated-stable : Stable (¬ A)
-negated-stable ¬¬¬a a = ¬¬¬a (_$ a)
+negated-stable ¬¬¬a a = ¬¬¬a (contradiction a)
 
 ¬¬-map : (A → B) → ¬ ¬ A → ¬ ¬ B
 ¬¬-map f = contraposition (contraposition f)
@@ -73,3 +75,4 @@ negated-stable ¬¬¬a a = ¬¬¬a (_$ a)
 private
   note : (A → ¬ B) → B → ¬ A
   note = flip
+
diff --git a/src/Relation/Nullary/Recomputable.agda b/src/Relation/Nullary/Recomputable.agda
new file mode 100644
index 0000000000..cd0b83f113
--- /dev/null
+++ b/src/Relation/Nullary/Recomputable.agda
@@ -0,0 +1,63 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Recomputable types and their algebra as Harrop formulas
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+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)
+open import Relation.Nullary.Negation.Core using (¬_)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    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 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
+
+⊥-recompute : Recomputable ⊥
+⊥-recompute ()
+
+_×-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
+
+-- corollary: negated propositions are Recomputable
+
+¬-recompute : Recomputable (¬ A)
+¬-recompute {A = A} = A →-recompute ⊥-recompute
+
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 3b301fdbce..00cee309a7 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -11,14 +11,13 @@ 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.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 (¬_; contradiction-irr; contradiction; _¬-⊎_)
+open import Relation.Nullary.Recomputable as Recomputable using (Recomputable)
 
 private
   variable
@@ -52,6 +51,20 @@ 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 = contradiction-irr a ¬a
+
+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.
 
@@ -64,34 +77,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ʸ (⊥-elim ∘ ¬a)
+ofʸ  a →-reflects ofʸ  b = of (const b)
+ofʸ  a →-reflects ofⁿ ¬b = of (¬b ∘ (_$ a))
+ofⁿ ¬a →-reflects _      = of (λ a → contradiction a ¬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′
diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 0f8a7534fd..3abc070ace 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -14,9 +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 as Nullary using (¬_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Nullary as Nullary using (¬_; Dec; True)
 
 private
   variable