From a0db97ca535bf5473eebc499160c939880a17d1f Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 13 Oct 2023 10:16:47 +0100
Subject: [PATCH 01/33] added dependent eliminator; refactored existing
 definitions; added `recompute`

---
 src/Relation/Nullary/Reflects.agda | 67 ++++++++++++++++++++++++------
 1 file changed, 55 insertions(+), 12 deletions(-)

diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 4f97bd8709..9f8ca61b0b 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -11,17 +11,17 @@ module Relation.Nullary.Reflects where
 open import Agda.Builtin.Equality
 
 open import Data.Bool.Base
-open import Data.Empty
+open import Data.Empty.Irrelevant using (⊥-elim)
 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)
+open import Function.Base using (id; _$_; _∘_; const; flip)
 
-open import Relation.Nullary.Negation.Core
+open import Relation.Nullary.Negation.Core using (¬_; contradiction; _¬-⊎_)
 
 private
   variable
-    a : Level
+    a c : Level
     A B : Set a
 
 ------------------------------------------------------------------------
@@ -40,24 +40,57 @@ data Reflects (A : Set a) : Bool → Set a where
 -- These lemmas are intended to be used mostly when `b` is a value, so
 -- that the `if` expressions have already been evaluated away.
 -- In this case, `of` works like the relevant constructor (`ofⁿ` or
--- `ofʸ`), and `invert` strips off the constructor to just give either
+-- `ofʸ`), and `of⁻¹` strips off the constructor to just give either
 -- the proof of `A` or the proof of `¬ A`.
 
+-- NB. not the maximally dependent eliminator, but mostly sufficent
+
+reflects : (C : Bool → Set c) → (A → C true) → (¬ A → C false) →
+           ∀ {b} → Reflects A b → C b
+reflects C t f (ofⁿ ¬a) = f ¬a
+reflects C t f (ofʸ  a) = t a
+
+reflects′ : (A → B) → (¬ A → B) → ∀ {b} → Reflects A b → B
+reflects′ {B = B} = reflects (const B)
+
 of : ∀ {b} → if b then A else ¬ A → Reflects A b
 of {b = false} ¬a = ofⁿ ¬a
 of {b = true }  a = ofʸ a
 
-invert : ∀ {b} → Reflects A b → if b then A else ¬ A
-invert (ofʸ  a) = a
-invert (ofⁿ ¬a) = ¬a
+of⁻¹ : ∀ {b} → Reflects A b → if b then A else ¬ A
+of⁻¹ {A = A} = reflects (λ b → if b then A else ¬ A) id id
+
+invert = of⁻¹ -- against subsequent deprecation
+
+-- in lieu of a distinct `Reflects.Properties` module
+
+of⁻¹∘of≗id : ∀ {b} (r : if b then A else ¬ A) → of⁻¹ (of {b = b} r) ≡ r
+of⁻¹∘of≗id {b = false} _ = refl
+of⁻¹∘of≗id {b = true}  _ = refl
+
+of∘of⁻¹≗id : ∀ {b} (r : Reflects A b) → of (of⁻¹ r) ≡ r
+of∘of⁻¹≗id (ofʸ a)  = refl
+of∘of⁻¹≗id (ofⁿ ¬a) = refl
+
+
+------------------------------------------------------------------------
+-- Recomputable/recompute
+
+Recomputable : (A : Set a) → Set a
+Recomputable A = .A → A
+
+-- 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 {A = A} = reflects (const (.A → A)) (λ a _ → a) (λ ¬a a → ⊥-elim (¬a a))
 
 ------------------------------------------------------------------------
 -- Interaction with negation, product, sums etc.
 
 -- 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 {A = A} = reflects (λ b → Reflects (¬ A) (not b)) (ofⁿ ∘ flip _$_) ofʸ
 
 -- If we can decide A and Q then we can decide their product
 infixr 2 _×-reflects_
@@ -67,7 +100,6 @@ ofʸ  a ×-reflects ofʸ  b = ofʸ (a , b)
 ofʸ  a ×-reflects ofⁿ ¬b = ofⁿ (¬b ∘ proj₂)
 ofⁿ ¬a ×-reflects _      = ofⁿ (¬a ∘ proj₁)
 
-
 infixr 1 _⊎-reflects_
 _⊎-reflects_ : ∀ {a b} → Reflects A a → Reflects B b →
                Reflects (A ⊎ B) (a ∨ b)
@@ -80,7 +112,8 @@ _→-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
@@ -95,3 +128,13 @@ 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ⁿ  _) = refl
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.1
+

From ea024ec4f2dca491eec005928c455d25d5285f1f Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 13 Oct 2023 10:23:18 +0100
Subject: [PATCH 02/33] knock-on changes; refactored `recompute`; made pattern
 synonyms `yes`, `no` lazier

---
 src/Relation/Nullary/Decidable/Core.agda | 74 ++++++++++++------------
 1 file changed, 38 insertions(+), 36 deletions(-)

diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 166b1f264e..55d638e7b9 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -12,19 +12,19 @@
 module Relation.Nullary.Decidable.Core where
 
 open import Level using (Level; Lift)
-open import Data.Bool.Base using (Bool; false; true; not; T; _∧_; _∨_)
+open import Data.Bool.Base
 open import Data.Unit.Base using (⊤)
-open import Data.Empty 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.Reflects as Reflects
+  using (Reflects; ofʸ; ofⁿ; of; of⁻¹; Recomputable)
 open import Relation.Nullary.Negation.Core
+  using (¬_; contradiction; Stable; DoubleNegation; negated-stable)
 
 private
   variable
-    a b : Level
+    a : Level
     A B : Set a
 
 ------------------------------------------------------------------------
@@ -48,8 +48,13 @@ record Dec (A : Set a) : Set a where
 
 open Dec public
 
-pattern yes a =  true because ofʸ  a
-pattern no ¬a = false because ofⁿ ¬a
+-- lazier versions of `yes` and `no`
+pattern yes′ [a] =  true because  [a]
+pattern no′ [¬a] = false because [¬a]
+
+-- now these are derived patterns, but could be re-expressed using `of`
+pattern yes  a  = yes′ (ofʸ a)
+pattern no [¬a] = no′ (ofⁿ [¬a])
 
 ------------------------------------------------------------------------
 -- Flattening
@@ -57,12 +62,10 @@ pattern no ¬a = false because ofⁿ ¬a
 module _ {A : Set a} where
 
   From-yes : Dec A → Set a
-  From-yes (true  because _) = A
-  From-yes (false because _) = Lift a ⊤
+  From-yes a? = if (does a?) then A else Lift a ⊤
 
   From-no : Dec A → Set a
-  From-no (false because _) = ¬ A
-  From-no (true  because _) = Lift a ⊤
+  From-no  a? = if (does a?) then Lift a ⊤ else ¬ A
 
 ------------------------------------------------------------------------
 -- Recompute
@@ -70,8 +73,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 → .A → A
-recompute (yes a) _ = a
-recompute (no ¬a) a = ⊥-elim (¬a a)
+recompute = Reflects.recompute ∘ proof
 
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
@@ -81,19 +83,19 @@ infixr 2 _×-dec_ _→-dec_
 
 ¬? : Dec A → Dec (¬ A)
 does  (¬? a?) = not (does a?)
-proof (¬? a?) = ¬-reflects (proof a?)
+proof (¬? a?) = Reflects.¬-reflects (proof a?)
 
 _×-dec_ : Dec A → Dec B → Dec (A × B)
 does  (a? ×-dec b?) = does a? ∧ does b?
-proof (a? ×-dec b?) = proof a? ×-reflects proof b?
+proof (a? ×-dec b?) = proof a? Reflects.×-reflects proof b?
 
 _⊎-dec_ : Dec A → Dec B → Dec (A ⊎ B)
 does  (a? ⊎-dec b?) = does a? ∨ does b?
-proof (a? ⊎-dec b?) = proof a? ⊎-reflects proof b?
+proof (a? ⊎-dec b?) = proof a? Reflects.⊎-reflects proof b?
 
 _→-dec_ : Dec A → Dec B → Dec (A → B)
 does  (a? →-dec b?) = not (does a?) ∨ does b?
-proof (a? →-dec b?) = proof a? →-reflects proof b?
+proof (a? →-dec b?) = proof a? Reflects.→-reflects proof b?
 
 ------------------------------------------------------------------------
 -- Relationship with booleans
@@ -104,8 +106,8 @@ proof (a? →-dec b?) = proof a? →-reflects proof b?
 -- for proof automation.
 
 isYes : Dec A → Bool
-isYes (true  because _) = true
-isYes (false because _) = false
+isYes (yes′ _) = true
+isYes (no′  _) = false
 
 isNo : Dec A → Bool
 isNo = not ∘ isYes
@@ -124,42 +126,42 @@ False = T ∘ isNo
 
 -- Gives a witness to the "truth".
 toWitness : {a? : Dec A} → True a? → A
-toWitness {a? = true  because [a]} _  = invert [a]
-toWitness {a? = false because  _ } ()
+toWitness {a? = yes′ [a]} _ = of⁻¹ [a]
+toWitness {a? = no′  _ } ()
 
 -- Establishes a "truth", given a witness.
 fromWitness : {a? : Dec A} → A → True a?
-fromWitness {a? = true  because   _ } = const _
-fromWitness {a? = false because [¬a]} = invert [¬a]
+fromWitness {a? = yes′  _ } = const _
+fromWitness {a? = no′ [¬a]} = of⁻¹ [¬a]
 
 -- Variants for False.
 toWitnessFalse : {a? : Dec A} → False a? → ¬ A
-toWitnessFalse {a? = true  because   _ } ()
-toWitnessFalse {a? = false because [¬a]} _  = invert [¬a]
+toWitnessFalse {a? = yes′  _ } ()
+toWitnessFalse {a? = no′ [¬a]} _  = of⁻¹ [¬a]
 
 fromWitnessFalse : {a? : Dec A} → ¬ A → False a?
-fromWitnessFalse {a? = true  because [a]} = flip _$_ (invert [a])
-fromWitnessFalse {a? = false because  _ } = const _
+fromWitnessFalse {a? = yes′ [a]} = flip _$_ (of⁻¹ [a])
+fromWitnessFalse {a? = no′   _ } = const _
 
 -- If a decision procedure returns "yes", then we can extract the
 -- proof using from-yes.
 from-yes : (a? : Dec A) → From-yes a?
-from-yes (true  because [a]) = invert [a]
-from-yes (false because _ ) = _
+from-yes (yes′ [a]) = of⁻¹ [a]
+from-yes (no′   _ ) = _
 
 -- If a decision procedure returns "no", then we can extract the proof
 -- using from-no.
 from-no : (a? : Dec A) → From-no a?
-from-no (false because [¬a]) = invert [¬a]
-from-no (true  because   _ ) = _
+from-no (no′ [¬a]) = of⁻¹ [¬a]
+from-no (yes′  _ ) = _
 
 ------------------------------------------------------------------------
 -- Maps
 
 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)
+does  (map′ A→B B→A a?)        = does a?
+proof (map′ A→B B→A (yes′ [a])) = of (A→B (of⁻¹ [a]))
+proof (map′ A→B B→A (no′ [¬a])) = of (of⁻¹ [¬a] ∘ B→A)
 
 ------------------------------------------------------------------------
 -- Relationship with double-negation
@@ -167,8 +169,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 = ⊥-elim (¬¬a ¬a)
+decidable-stable (yes′ [a]) ¬¬a = of⁻¹ [a]
+decidable-stable (no′ [¬a]) ¬¬a = contradiction (of⁻¹ [¬a]) ¬¬a
 
 ¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A)
 ¬-drop-Dec ¬¬a? = map′ negated-stable contradiction (¬? ¬¬a?)

From 9d92dd55940aa3a75bc55823b014f2ea201ffa2a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 13 Oct 2023 10:30:52 +0100
Subject: [PATCH 03/33] added `of`, `invert`, `Recomputable` to exports from
 `Reflects`

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

diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index b8a4c30470..03bb6d866c 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -21,7 +21,7 @@ open import Relation.Nullary.Negation.Core public using
   )
 
 open import Relation.Nullary.Reflects public using
-  ( Reflects; ofʸ; ofⁿ
+  ( Reflects; ofʸ; ofⁿ; of; invert; Recomputable
   ; _×-reflects_; _⊎-reflects_; _→-reflects_
   )
 

From 3c41be8e516c85bde5ac0f34989f42d3d4592266 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 13 Oct 2023 10:41:00 +0100
Subject: [PATCH 04/33] retained use of `invert`

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

diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 55d638e7b9..f30e668b54 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.Reflects as Reflects
-  using (Reflects; ofʸ; ofⁿ; of; of⁻¹; Recomputable)
+  using (Reflects; ofʸ; ofⁿ; of; invert; Recomputable)
 open import Relation.Nullary.Negation.Core
   using (¬_; contradiction; Stable; DoubleNegation; negated-stable)
 
@@ -126,33 +126,33 @@ False = T ∘ isNo
 
 -- Gives a witness to the "truth".
 toWitness : {a? : Dec A} → True a? → A
-toWitness {a? = yes′ [a]} _ = of⁻¹ [a]
+toWitness {a? = yes′ [a]} _ = invert [a]
 toWitness {a? = no′  _ } ()
 
 -- Establishes a "truth", given a witness.
 fromWitness : {a? : Dec A} → A → True a?
 fromWitness {a? = yes′  _ } = const _
-fromWitness {a? = no′ [¬a]} = of⁻¹ [¬a]
+fromWitness {a? = no′ [¬a]} = invert [¬a]
 
 -- Variants for False.
 toWitnessFalse : {a? : Dec A} → False a? → ¬ A
 toWitnessFalse {a? = yes′  _ } ()
-toWitnessFalse {a? = no′ [¬a]} _  = of⁻¹ [¬a]
+toWitnessFalse {a? = no′ [¬a]} _  = invert [¬a]
 
 fromWitnessFalse : {a? : Dec A} → ¬ A → False a?
-fromWitnessFalse {a? = yes′ [a]} = flip _$_ (of⁻¹ [a])
+fromWitnessFalse {a? = yes′ [a]} = flip _$_ (invert [a])
 fromWitnessFalse {a? = no′   _ } = const _
 
 -- If a decision procedure returns "yes", then we can extract the
 -- proof using from-yes.
 from-yes : (a? : Dec A) → From-yes a?
-from-yes (yes′ [a]) = of⁻¹ [a]
+from-yes (yes′ [a]) = invert [a]
 from-yes (no′   _ ) = _
 
 -- If a decision procedure returns "no", then we can extract the proof
 -- using from-no.
 from-no : (a? : Dec A) → From-no a?
-from-no (no′ [¬a]) = of⁻¹ [¬a]
+from-no (no′ [¬a]) = invert [¬a]
 from-no (yes′  _ ) = _
 
 ------------------------------------------------------------------------
@@ -160,8 +160,8 @@ from-no (yes′  _ ) = _
 
 map′ : (A → B) → (B → A) → Dec A → Dec B
 does  (map′ A→B B→A a?)        = does a?
-proof (map′ A→B B→A (yes′ [a])) = of (A→B (of⁻¹ [a]))
-proof (map′ A→B B→A (no′ [¬a])) = of (of⁻¹ [¬a] ∘ B→A)
+proof (map′ A→B B→A (yes′ [a])) = of (A→B (invert [a]))
+proof (map′ A→B B→A (no′ [¬a])) = of (invert [¬a] ∘ B→A)
 
 ------------------------------------------------------------------------
 -- Relationship with double-negation
@@ -169,8 +169,8 @@ proof (map′ A→B B→A (no′ [¬a])) = of (of⁻¹ [¬a] ∘ B→A)
 -- Decidable predicates are stable.
 
 decidable-stable : Dec A → Stable A
-decidable-stable (yes′ [a]) ¬¬a = of⁻¹ [a]
-decidable-stable (no′ [¬a]) ¬¬a = contradiction (of⁻¹ [¬a]) ¬¬a
+decidable-stable (yes′ [a]) ¬¬a = invert [a]
+decidable-stable (no′ [¬a]) ¬¬a = contradiction (invert [¬a]) ¬¬a
 
 ¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A)
 ¬-drop-Dec ¬¬a? = map′ negated-stable contradiction (¬? ¬¬a?)

From 9df29e6690ee7af39b30d2da240d35fd6becb1c1 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 13 Oct 2023 10:42:26 +0100
Subject: [PATCH 05/33] knock-on consequences; tightened `imports`

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

diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index cb5f72b6e0..bf197da15c 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -9,16 +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.Reflects using (invert)
+open import Relation.Nullary using (invert; ¬_; contradiction; Irrelevant)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong′)
 
 private
@@ -51,23 +49,23 @@ 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-↔ (yes′ [a]) irr = let  a = invert  [a] in mk↔ₛ′ (λ _ → a) _ (irr a) cong′
+True-↔ (no′ [¬a]) _   = let ¬a = invert [¬a] in mk↔ₛ′ (λ ()) ¬a (λ a → contradiction a ¬a) λ ()
 
 ------------------------------------------------------------------------
 -- Result of decidability
 
 isYes≗does : (a? : Dec A) → isYes a? ≡ does a?
-isYes≗does (true  because _) = refl
-isYes≗does (false because _) = refl
+isYes≗does (yes′ _) = refl
+isYes≗does (no′  _) = 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 (yes′  _ ) a = refl
+dec-true (no′ [¬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 (no′   _ ) ¬a = refl
+dec-false (yes′ [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

From 259e966486f399b754e8b01ebf647dfd8cbf314f Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 13 Oct 2023 10:58:37 +0100
Subject: [PATCH 06/33] =?UTF-8?q?added=20`reflects`,=20`reflects=E2=80=B2`?=
 =?UTF-8?q?,=20`yes=E2=80=B2`,=20`no=E2=80=B2`=20to=20exports=20from=20`Re?=
 =?UTF-8?q?flects`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index 03bb6d866c..bc3ffeaf26 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -21,12 +21,12 @@ open import Relation.Nullary.Negation.Core public using
   )
 
 open import Relation.Nullary.Reflects public using
-  ( Reflects; ofʸ; ofⁿ; of; invert; Recomputable
+  ( Reflects; ofʸ; ofⁿ; reflects; reflects′; of; invert; Recomputable
   ; _×-reflects_; _⊎-reflects_; _→-reflects_
   )
 
 open import Relation.Nullary.Decidable.Core public using
-  ( Dec; does; proof; yes; no; _because_; recompute
+  ( Dec; _because_; does; proof; yes′; no′; yes; no; recompute
   ; ¬?; _×-dec_; _⊎-dec_; _→-dec_
   )
 

From 35bb7099af1430fcc073369d165f2946e714fc8c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 13 Oct 2023 12:38:07 +0100
Subject: [PATCH 07/33] exemplary refactoring

---
 src/Axiom/UniquenessOfIdentityProofs.agda | 34 +++++++++++------------
 1 file changed, 16 insertions(+), 18 deletions(-)

diff --git a/src/Axiom/UniquenessOfIdentityProofs.agda b/src/Axiom/UniquenessOfIdentityProofs.agda
index 1cefc1a6a1..f708eff986 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 Function.Base using (id; const; flip)
+open import Level using (Level)
+open import Relation.Nullary using (contradiction; reflects′; proof)
 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
+
 ------------------------------------------------------------------------
 -- 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} _≡_
 
 ------------------------------------------------------------------------
@@ -38,12 +42,11 @@ UIP A = Irrelevant {A = A} _≡_
 -- proof to its image via this function which we then know is equal to
 -- 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)
+module Constant⇒UIP (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 : ∀ {x y} (p : x ≡ y) → trans (sym (f refl)) (f p) ≡ p
   ≡-canonical refl = trans-symˡ (f refl)
 
   ≡-irrelevant : UIP A
@@ -59,19 +62,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} (_≟_ : 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 {a} {b} a≡b = reflects′ id (contradiction a≡b) (proof (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-constant {a} {b} a≡b _
+    = reflects′ (λ _ → refl) (contradiction a≡b) (proof (a ≟ b))
 
   ≡-irrelevant : UIP A
   ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant

From a68ab46a7ee561671355a62b694e6fbefa389c2e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 14 Oct 2023 17:33:30 +0100
Subject: [PATCH 08/33] corrected reference to `README.Design.Decidability`

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

diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index f30e668b54..9836669955 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -35,8 +35,8 @@ private
 -- reflects the boolean result. This definition allows the boolean
 -- part of the decision procedure to compute independently from the
 -- proof. This leads to better computational behaviour when we only care
--- about the result and not the proof. See README.Decidability for
--- further details.
+-- about the result and not the proof. See README.Design.Decidability
+-- for further details.
 
 infix 2 _because_
 

From 8fba6746176ecf41e6acb1d8f4051cb4ceaa7482 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 14 Oct 2023 17:42:33 +0100
Subject: [PATCH 09/33] uniformity of `of`

---
 README/Design/Decidability.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/README/Design/Decidability.agda b/README/Design/Decidability.agda
index c6f086424f..d290197de4 100644
--- a/README/Design/Decidability.agda
+++ b/README/Design/Decidability.agda
@@ -31,14 +31,14 @@ infix 4 _≟₀_ _≟₁_ _≟₂_
 -- a proof of `Reflects P false` amounts to a refutation of `P`.
 
 ex₀ : (n : ℕ) → Reflects (n ≡ n) true
-ex₀ n = ofʸ refl
+ex₀ n = of refl
 
 ex₁ : (n : ℕ) → Reflects (zero ≡ suc n) false
-ex₁ n = ofⁿ λ ()
+ex₁ n = of λ ()
 
 ex₂ : (b : Bool) → Reflects (T b) b
-ex₂ false = ofⁿ id
-ex₂ true  = ofʸ tt
+ex₂ false = of id
+ex₂ true  = of tt
 
 ------------------------------------------------------------------------
 -- Dec

From d8fe7138ed462537ec6d6cadf8279402e2759dca Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 18 Oct 2023 13:50:10 +0100
Subject: [PATCH 10/33] further uniformity wrt `of`

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

diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 9f8ca61b0b..6044490a09 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -90,37 +90,37 @@ recompute {A = A} = reflects (const (.A → A)) (λ a _ → a) (λ ¬a a → ⊥
 
 -- If we can decide A, then we can decide its negation.
 ¬-reflects : ∀ {b} → Reflects A b → Reflects (¬ A) (not b)
-¬-reflects {A = A} = reflects (λ b → Reflects (¬ A) (not b)) (ofⁿ ∘ flip _$_) ofʸ
+¬-reflects {A = A} = reflects (λ b → Reflects (¬ A) (not b)) (of ∘ flip _$_) of
 
 -- If we can decide A and Q then we can decide their product
 infixr 2 _×-reflects_
 _×-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₁)
 
 infixr 1 _⊎-reflects_
 _⊎-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)
 
 infixr 2 _→-reflects_
 _→-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 (flip 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 856d8d3a9f149c46a6bfcbc093c7703b10b362a0 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 19 Oct 2023 18:47:39 +0100
Subject: [PATCH 11/33] uniformity of `of`

---
 README/Design/Decidability.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README/Design/Decidability.agda b/README/Design/Decidability.agda
index d290197de4..d38bcfba4a 100644
--- a/README/Design/Decidability.agda
+++ b/README/Design/Decidability.agda
@@ -85,8 +85,8 @@ zero  ≟₁ suc n = no λ ()
 suc m ≟₁ zero  = no λ ()
 does  (suc m ≟₁ suc n) = does (m ≟₁ n)
 proof (suc m ≟₁ suc n) with m ≟₁ n
-... | yes p = ofʸ (cong suc p)
-... | no ¬p = ofⁿ (¬p ∘ suc-injective)
+... | yes p = of (cong suc p)
+... | no ¬p = of (¬p ∘ suc-injective)
 
 -- We now get definitional equalities such as the following.
 

From af83f0ae1ebc75879d42957b70f2693022f36345 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Oct 2023 08:51:29 +0100
Subject: [PATCH 12/33] tightened `recompute`; moved `invert` towards
 deprecation

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

diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 6044490a09..44c14654df 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -60,8 +60,6 @@ of {b = true }  a = ofʸ a
 of⁻¹ : ∀ {b} → Reflects A b → if b then A else ¬ A
 of⁻¹ {A = A} = reflects (λ b → if b then A else ¬ A) id id
 
-invert = of⁻¹ -- against subsequent deprecation
-
 -- in lieu of a distinct `Reflects.Properties` module
 
 of⁻¹∘of≗id : ∀ {b} (r : if b then A else ¬ A) → of⁻¹ (of {b = b} r) ≡ r
@@ -83,7 +81,7 @@ Recomputable A = .A → A
 -- be recomputed and subsequently used in relevant contexts.
 
 recompute : ∀ {b} → Reflects A b → Recomputable A
-recompute {A = A} = reflects (const (.A → A)) (λ a _ → a) (λ ¬a a → ⊥-elim (¬a a))
+recompute {A = A} = reflects′ {B = Recomputable A} (λ a _ → a) (λ ¬a a → ⊥-elim (¬a a))
 
 ------------------------------------------------------------------------
 -- Interaction with negation, product, sums etc.
@@ -138,3 +136,5 @@ det (ofⁿ ¬a) (ofⁿ  _) = refl
 
 -- Version 2.1
 
+invert = of⁻¹ -- against subsequent deprecation; no warning issued yet
+

From 964b973a70a8baaf4ccd7280b36ad7c57935d9ca Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 4 Nov 2023 02:59:34 +0000
Subject: [PATCH 13/33] fixed buggy merge conflict

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

diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 93a31df8e0..d47de19b3e 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -53,9 +53,11 @@ reflects C t f (ofʸ  a) = t a
 reflects′ : (A → B) → (¬ A → B) → ∀ {b} → Reflects A b → B
 reflects′ {B = B} = reflects (const B)
 
+-- a 'computed constructor' and its inverse
+
 of : ∀ {b} → if b then A else ¬ A → Reflects A b
-of {b = false} ¬a = ofⁿ ¬a
-of {b = true }  a = ofʸ a
+of {b = false} = ofⁿ
+of {b = true } = ofʸ
 
 of⁻¹ : ∀ {b} → Reflects A b → if b then A else ¬ A
 of⁻¹ {A = A} = reflects (λ b → if b then A else ¬ A) id id

From 2410d81d5f9b00c6cd590cf15730c1a10eff5c5a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 4 Nov 2023 03:06:18 +0000
Subject: [PATCH 14/33] fixed buggy merge conflict

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

diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 679891f7ea..cd089be403 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -12,7 +12,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.Bool.Base
 open import Data.Unit.Base using (⊤)
 open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
@@ -82,7 +82,7 @@ infixr 1 _⊎-dec_
 infixr 2 _×-dec_ _→-dec_
 
 T? : ∀ x → Dec (T x)
-T? x = x because T-reflects x
+T? x = x because Reflects.T-reflects x
 
 ¬? : Dec A → Dec (¬ A)
 does  (¬? a?) = not (does a?)

From 1308e1d5702117473c76e209991768f5b2b1d650 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 4 Nov 2023 03:17:01 +0000
Subject: [PATCH 15/33] fixed buggy merge conflict: hides `Reflects.recompute`

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

diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index 0b0f83f77b..b3015f8983 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -17,6 +17,7 @@ open import Agda.Builtin.Equality
 
 open import Relation.Nullary.Negation.Core public
 open import Relation.Nullary.Reflects public
+  hiding (recompute)
 open import Relation.Nullary.Decidable.Core public
 
 ------------------------------------------------------------------------

From 507d3b116b1bda389dfaa7e20418cfd59eb1e10f Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 4 Nov 2023 03:54:42 +0000
Subject: [PATCH 16/33] tightened up

---
 src/Relation/Nullary/Reflects.agda | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index d47de19b3e..b93ec089e7 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -38,10 +38,7 @@ data Reflects (A : Set a) : Bool → Set a where
 -- Constructors and destructors
 
 -- These lemmas are intended to be used mostly when `b` is a value, so
--- that the `if` expressions have already been evaluated away.
--- In this case, `of` works like the relevant constructor (`ofⁿ` or
--- `ofʸ`), and `of⁻¹` strips off the constructor to just give either
--- the proof of `A` or the proof of `¬ A`.
+-- that the conditional expressions have already been evaluated away.
 
 -- NB. not the maximally dependent eliminator, but mostly sufficent
 
@@ -53,14 +50,16 @@ reflects C t f (ofʸ  a) = t a
 reflects′ : (A → B) → (¬ A → B) → ∀ {b} → Reflects A b → B
 reflects′ {B = B} = reflects (const B)
 
--- a 'computed constructor' and its inverse
+-- In this case, `of` works like the relevant 'computed constructor'
+-- (`ofⁿ` or `ofʸ`), and its inverse `of⁻¹` strips off the constructor
+-- to just give either the proof of `A` or the proof of `¬ A`.
 
 of : ∀ {b} → if b then A else ¬ A → Reflects A b
 of {b = false} = ofⁿ
 of {b = true } = ofʸ
 
 of⁻¹ : ∀ {b} → Reflects A b → if b then A else ¬ A
-of⁻¹ {A = A} = reflects (λ b → if b then A else ¬ A) id id
+of⁻¹ {A = A} = reflects (if_then A else ¬ A) id id
 
 -- in lieu of a distinct `Reflects.Properties` module
 
@@ -97,9 +96,9 @@ 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 {A = A} = reflects (λ b → Reflects (¬ A) (not b)) (of ∘ flip _$_) of
+¬-reflects {A = A} = reflects (Reflects (¬ A) ∘ not) (of ∘ flip _$_) of
 
--- If we can decide A and Q then we can decide their product
+-- If we can decide A and B then we can decide their product, sum and implication
 _×-reflects_ : ∀ {a b} → Reflects A a → Reflects B b →
                Reflects (A × B) (a ∧ b)
 ofʸ  a ×-reflects ofʸ  b = of (a , b)
@@ -113,7 +112,7 @@ 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)
+               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)

From 7512da6fd3a930007dc42f79414675a9bb95acb1 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 4 Nov 2023 04:28:53 +0000
Subject: [PATCH 17/33] tightened up; added characterisation lemmas

---
 src/Relation/Nullary/Decidable/Core.agda | 88 +++++++++++++++---------
 1 file changed, 57 insertions(+), 31 deletions(-)

diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index cd089be403..2fa85769a6 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -16,9 +16,9 @@ open import Data.Bool.Base
 open import Data.Unit.Base using (⊤)
 open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
-open import Function.Base using (_∘_; const; _$_; flip)
+open import Function.Base using (id; _∘_; const; _$_; flip)
 open import Relation.Nullary.Reflects as Reflects
-  using (Reflects; ofʸ; ofⁿ; of; invert; Recomputable)
+  using (Reflects; of; invert; Recomputable)
 open import Relation.Nullary.Negation.Core
   using (¬_; contradiction; Stable; DoubleNegation; negated-stable)
 
@@ -48,13 +48,39 @@ record Dec (A : Set a) : Set a where
 
 open Dec public
 
--- lazier versions of `yes` and `no`
-pattern yes′ [a] =  true because  [a]
-pattern no′ [¬a] = false because [¬a]
+-- lazier 'pattern' _ᵖ versions of `yes` and `no`
+pattern yesᵖ [a] =  true because  [a]
+pattern noᵖ [¬a] = false because [¬a]
 
--- now these are derived patterns, but could be re-expressed using `of`
-pattern yes  a  = yes′ (ofʸ a)
-pattern no [¬a] = no′ (ofⁿ [¬a])
+-- now these original forms are derived patterns
+pattern yes a = yesᵖ (Reflects.ofʸ a)
+pattern no ¬a = noᵖ (Reflects.ofⁿ ¬a)
+
+-- but can be re-expressed as term constructions _ᵗ using `of`
+yesᵗ : A → Dec A
+yesᵗ a = yesᵖ (of a)
+
+noᵗ : ¬ A → Dec A
+noᵗ ¬a = noᵖ (of ¬a)
+
+------------------------------------------------------------------------
+-- Characterisation : Dec A iff there is a Bool b reflecting it via T
+
+-- forwards direction: use `does`
+
+does-complete : ∀ (A? : Dec A) → A → T (does A?)
+does-complete (yesᵖ  _ ) _ = _
+does-complete (noᵖ [¬a]) a = contradiction a (invert [¬a])
+
+does-sound : ∀ (A? : Dec A) → T (does A?) → A
+does-sound (yesᵖ [a]) _ = invert [a]
+does-sound (noᵖ   _ ) ()
+
+-- backwards direction: inherit from `Reflects`
+
+fromEquivalence : ∀ {b} → (T b → A) → (A → T b) → Dec A
+fromEquivalence {b = b} sound complete
+  = b because (Reflects.fromEquivalence sound complete)
 
 ------------------------------------------------------------------------
 -- Flattening
@@ -72,7 +98,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 → .A → A
+recompute : Dec A → Recomputable A
 recompute = Reflects.recompute ∘ proof
 
 ------------------------------------------------------------------------
@@ -81,8 +107,8 @@ recompute = Reflects.recompute ∘ proof
 infixr 1 _⊎-dec_
 infixr 2 _×-dec_ _→-dec_
 
-T? : ∀ x → Dec (T x)
-T? x = x because Reflects.T-reflects x
+T? : ∀ b → Dec (T b)
+T? b = b because Reflects.T-reflects b -- ≗ fromEquivalence id id
 
 ¬? : Dec A → Dec (¬ A)
 does  (¬? a?) = not (does a?)
@@ -109,8 +135,8 @@ proof (a? →-dec b?) = proof a? Reflects.→-reflects proof b?
 -- for proof automation.
 
 isYes : Dec A → Bool
-isYes (yes′ _) = true
-isYes (no′  _) = false
+isYes (yesᵖ _) = true
+isYes (noᵖ  _) = false
 
 isNo : Dec A → Bool
 isNo = not ∘ isYes
@@ -129,42 +155,42 @@ False = T ∘ isNo
 
 -- Gives a witness to the "truth".
 toWitness : {a? : Dec A} → True a? → A
-toWitness {a? = yes′ [a]} _ = invert [a]
-toWitness {a? = no′  _ } ()
+toWitness {a? = yesᵖ [a]} _ = invert [a]
+toWitness {a? = noᵖ  _ } ()
 
 -- Establishes a "truth", given a witness.
 fromWitness : {a? : Dec A} → A → True a?
-fromWitness {a? = yes′  _ } = const _
-fromWitness {a? = no′ [¬a]} = invert [¬a]
+fromWitness {a? = yesᵖ  _ } = const _
+fromWitness {a? = noᵖ [¬a]} = invert [¬a]
 
 -- Variants for False.
 toWitnessFalse : {a? : Dec A} → False a? → ¬ A
-toWitnessFalse {a? = yes′  _ } ()
-toWitnessFalse {a? = no′ [¬a]} _  = invert [¬a]
+toWitnessFalse {a? = yesᵖ  _ } ()
+toWitnessFalse {a? = noᵖ [¬a]} _  = invert [¬a]
 
 fromWitnessFalse : {a? : Dec A} → ¬ A → False a?
-fromWitnessFalse {a? = yes′ [a]} = flip _$_ (invert [a])
-fromWitnessFalse {a? = no′   _ } = const _
+fromWitnessFalse {a? = yesᵖ [a]} = flip _$_ (invert [a])
+fromWitnessFalse {a? = noᵖ   _ } = const _
 
 -- If a decision procedure returns "yes", then we can extract the
 -- proof using from-yes.
 from-yes : (a? : Dec A) → From-yes a?
-from-yes (yes′ [a]) = invert [a]
-from-yes (no′   _ ) = _
+from-yes (yesᵖ [a]) = invert [a]
+from-yes (noᵖ   _ ) = _
 
 -- If a decision procedure returns "no", then we can extract the proof
 -- using from-no.
 from-no : (a? : Dec A) → From-no a?
-from-no (no′ [¬a]) = invert [¬a]
-from-no (yes′  _ ) = _
+from-no (noᵖ [¬a]) = invert [¬a]
+from-no (yesᵖ  _ ) = _
 
 ------------------------------------------------------------------------
 -- Maps
 
 map′ : (A → B) → (B → A) → Dec A → Dec B
-does  (map′ A→B B→A a?)        = does a?
-proof (map′ A→B B→A (yes′ [a])) = of (A→B (invert [a]))
-proof (map′ A→B B→A (no′ [¬a])) = of (invert [¬a] ∘ B→A)
+does  (map′ A→B B→A a?)         = does a?
+proof (map′ A→B B→A (yesᵖ [a])) = of (A→B (invert [a]))
+proof (map′ A→B B→A (noᵖ [¬a])) = of (invert [¬a] ∘ B→A)
 
 ------------------------------------------------------------------------
 -- Relationship with double-negation
@@ -172,8 +198,8 @@ proof (map′ A→B B→A (no′ [¬a])) = of (invert [¬a] ∘ B→A)
 -- Decidable predicates are stable.
 
 decidable-stable : Dec A → Stable A
-decidable-stable (yes′ [a]) ¬¬a = invert [a]
-decidable-stable (no′ [¬a]) ¬¬a = contradiction (invert [¬a]) ¬¬a
+decidable-stable (yesᵖ [a]) ¬¬a = invert [a]
+decidable-stable (noᵖ [¬a]) ¬¬a = contradiction (invert [¬a]) ¬¬a
 
 ¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A)
 ¬-drop-Dec ¬¬a? = map′ negated-stable contradiction (¬? ¬¬a?)
@@ -182,7 +208,7 @@ decidable-stable (no′ [¬a]) ¬¬a = contradiction (invert [¬a]) ¬¬a
 -- nullary relation is decidable in the double-negation monad).
 
 ¬¬-excluded-middle : DoubleNegation (Dec A)
-¬¬-excluded-middle ¬?a = ¬?a (no (λ a → ¬?a (yes a)))
+¬¬-excluded-middle ¬?a = ¬?a (noᵗ (λ a → ¬?a (yesᵗ a)))
 
 
 ------------------------------------------------------------------------

From 13f196a94e7d1a6785435001c4dfac50f4b4bcaf Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 4 Nov 2023 04:29:25 +0000
Subject: [PATCH 18/33] hides `Reflects.fromEquivalence`

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

diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index b3015f8983..9a8e8fce1f 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -17,7 +17,7 @@ open import Agda.Builtin.Equality
 
 open import Relation.Nullary.Negation.Core public
 open import Relation.Nullary.Reflects public
-  hiding (recompute)
+  hiding (recompute; fromEquivalence)
 open import Relation.Nullary.Decidable.Core public
 
 ------------------------------------------------------------------------

From edc184adb48b64acae8605a05548b081cb1943fd Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 4 Nov 2023 05:12:38 +0000
Subject: [PATCH 19/33] added characterisation lemmas

---
 src/Relation/Nullary/Decidable.agda | 42 +++++++++++++++++++++--------
 1 file changed, 31 insertions(+), 11 deletions(-)

diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index bf197da15c..de61ecffd0 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -9,11 +9,11 @@
 module Relation.Nullary.Decidable where
 
 open import Level using (Level)
-open import Data.Bool.Base using (true; false)
-open import Data.Product.Base using (∃; _,_)
+open import Data.Bool.Base using (true; false; T)
+open import Data.Product.Base using (∃; ∃-syntax; _,_)
 open import Function.Base
 open import Function.Bundles using
-  (Injection; module Injection; module Equivalence; _⇔_; _↔_; mk↔ₛ′)
+  (Injection; module Injection; module Equivalence; _⇔_; mk⇔; _↔_; mk↔ₛ′)
 open import Relation.Binary.Bundles using (Setoid; module Setoid)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary using (invert; ¬_; contradiction; Irrelevant)
@@ -29,6 +29,26 @@ private
 
 open import Relation.Nullary.Decidable.Core public
 
+------------------------------------------------------------------------
+-- Characterisation : Dec A ⇔ there exists a Bool b st A ⇔ T b 
+
+-- forwards direction: use `does`
+
+dec⇔T∘does : (A? : Dec A) → A ⇔ T (does A?)
+dec⇔T∘does A? = mk⇔ (does-complete A?) (does-sound A?)
+
+dec⇒∃⇔T : (A? : Dec A) → ∃[ b ] A ⇔ T b
+dec⇒∃⇔T A? = does A? , dec⇔T∘does A?
+
+-- backwards direction: inherit from `Decidable.Core`
+∃⇔T⇒dec : (∃[ b ] A ⇔ T b) → Dec A
+∃⇔T⇒dec (b , A⇔Tb) = fromEquivalence from to
+  where open Equivalence A⇔Tb
+
+-- finally
+dec⇔∃⇔T : Dec A ⇔ (∃[ b ] A ⇔ T b)
+dec⇔∃⇔T = mk⇔ dec⇒∃⇔T ∃⇔T⇒dec
+
 ------------------------------------------------------------------------
 -- Maps
 
@@ -49,23 +69,23 @@ 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-↔ (yes′ [a]) irr = let  a = invert  [a] in mk↔ₛ′ (λ _ → a) _ (irr a) cong′
-True-↔ (no′ [¬a]) _   = let ¬a = invert [¬a] in mk↔ₛ′ (λ ()) ¬a (λ a → contradiction a ¬a) λ ()
+True-↔ (yesᵖ [a]) irr = let  a = invert  [a] in mk↔ₛ′ (λ _ → a) _ (irr a) cong′
+True-↔ (noᵖ [¬a]) _   = let ¬a = invert [¬a] in mk↔ₛ′ (λ ()) ¬a (λ a → contradiction a ¬a) λ ()
 
 ------------------------------------------------------------------------
 -- Result of decidability
 
 isYes≗does : (a? : Dec A) → isYes a? ≡ does a?
-isYes≗does (yes′ _) = refl
-isYes≗does (no′  _) = refl
+isYes≗does (yesᵖ _) = refl
+isYes≗does (noᵖ  _) = refl
 
 dec-true : (a? : Dec A) → A → does a? ≡ true
-dec-true (yes′  _ ) a = refl
-dec-true (no′ [¬a]) a = contradiction a (invert [¬a])
+dec-true (yesᵖ  _ ) a = refl
+dec-true (noᵖ [¬a]) a = contradiction a (invert [¬a])
 
 dec-false : (a? : Dec A) → ¬ A → does a? ≡ false
-dec-false (no′   _ ) ¬a = refl
-dec-false (yes′ [a]) ¬a = contradiction (invert [a]) ¬a
+dec-false (noᵖ   _ ) ¬a = refl
+dec-false (yesᵖ [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

From f5329db586a7d6a4e0f8c1c5fca454c9e54e3721 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 4 Nov 2023 05:32:01 +0000
Subject: [PATCH 20/33] knock-on consequences for `import`s

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

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 37b1f33ee0..3b01f6155c 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -38,7 +38,7 @@ open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Decidable using (True; via-injection; map′)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
-open import Relation.Nullary.Reflects using (fromEquivalence)
+open import Relation.Nullary.Reflects as Reflects using (Reflects)
 
 open import Algebra.Definitions {A = ℕ} _≡_
   hiding (LeftCancellative; RightCancellative; Cancellative)
@@ -126,7 +126,7 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 <⇒<ᵇ (s<s m<n@(s≤s _)) = <⇒<ᵇ m<n
 
 <ᵇ-reflects-< : ∀ m n → Reflects (m < n) (m <ᵇ n)
-<ᵇ-reflects-< m n = fromEquivalence (<ᵇ⇒< m n) <⇒<ᵇ
+<ᵇ-reflects-< m n = Reflects.fromEquivalence (<ᵇ⇒< m n) <⇒<ᵇ
 
 ------------------------------------------------------------------------
 -- Properties of _≤ᵇ_
@@ -141,7 +141,7 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 ≤⇒≤ᵇ m≤n@(s≤s _) = <⇒<ᵇ m≤n
 
 ≤ᵇ-reflects-≤ : ∀ m n → Reflects (m ≤ n) (m ≤ᵇ n)
-≤ᵇ-reflects-≤ m n = fromEquivalence (≤ᵇ⇒≤ m n) ≤⇒≤ᵇ
+≤ᵇ-reflects-≤ m n = Reflects.fromEquivalence (≤ᵇ⇒≤ m n) ≤⇒≤ᵇ
 
 ------------------------------------------------------------------------
 -- Properties of _≤_

From d1ee5149b9fd9adb0b712d371e427f5b6fdcce3e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 4 Nov 2023 05:44:15 +0000
Subject: [PATCH 21/33] knock-on consequences for `import`s

---
 src/Data/Nat/Properties.agda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 3b01f6155c..96eb3968be 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -20,7 +20,6 @@ import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
 import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
 import Algebra.Properties.CommutativeSemigroup as CommSemigroupProperties
 open import Data.Bool.Base using (Bool; false; true; T)
-open import Data.Bool.Properties using (T?)
 open import Data.Nat.Base
 open import Data.Product.Base using (∃; _×_; _,_)
 open import Data.Sum.Base as Sum
@@ -36,7 +35,7 @@ open import Relation.Binary
 open import Relation.Binary.Consequences using (flip-Connex)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary hiding (Irrelevant)
-open import Relation.Nullary.Decidable using (True; via-injection; map′)
+open import Relation.Nullary.Decidable using (T?; True; via-injection; map′)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects as Reflects using (Reflects)
 

From 40558fe8e09593ee148b6df70f0c5ea4714e4470 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 4 Nov 2023 09:24:10 +0000
Subject: [PATCH 22/33] narrower `import`s

---
 src/Data/Nat/Properties.agda | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 96eb3968be..6a520b23bf 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -34,8 +34,9 @@ open import Relation.Binary.Core
 open import Relation.Binary
 open import Relation.Binary.Consequences using (flip-Connex)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary hiding (Irrelevant)
-open import Relation.Nullary.Decidable using (T?; True; via-injection; map′)
+--open import Relation.Nullary hiding (Irrelevant)
+open import Relation.Nullary.Decidable
+  using (Dec; yes; no; T?; True; via-injection; map′)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects as Reflects using (Reflects)
 

From a9b8c24b89898d85cb20d714491ce00d3cfc0501 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 4 Nov 2023 10:22:25 +0000
Subject: [PATCH 23/33] final tweaks

---
 src/Data/Nat/Properties.agda | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 6a520b23bf..4543642e8c 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -34,7 +34,6 @@ open import Relation.Binary.Core
 open import Relation.Binary
 open import Relation.Binary.Consequences using (flip-Connex)
 open import Relation.Binary.PropositionalEquality
---open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Decidable
   using (Dec; yes; no; T?; True; via-injection; map′)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)

From 66dbe56b5e5837853803310882c4a9133dbac285 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 7 Nov 2023 09:11:31 +0000
Subject: [PATCH 24/33] recitfy variable names

---
 src/Axiom/UniquenessOfIdentityProofs.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Axiom/UniquenessOfIdentityProofs.agda b/src/Axiom/UniquenessOfIdentityProofs.agda
index f708eff986..7290f76190 100644
--- a/src/Axiom/UniquenessOfIdentityProofs.agda
+++ b/src/Axiom/UniquenessOfIdentityProofs.agda
@@ -65,11 +65,11 @@ module Constant⇒UIP (f : _≡_ {A = A} ⇒ _≡_)
 module Decidable⇒UIP (_≟_ : Decidable {A = A} _≡_) where
 
   ≡-normalise : _≡_ {A = A} ⇒ _≡_
-  ≡-normalise {a} {b} a≡b = reflects′ id (contradiction a≡b) (proof (a ≟ b))
+  ≡-normalise {x} {y} x≡y = reflects′ id (contradiction x≡y) (proof (x ≟ y))
 
-  ≡-normalise-constant : ∀ {a b} (p q : a ≡ b) → ≡-normalise p ≡ ≡-normalise q
-  ≡-normalise-constant {a} {b} a≡b _
-    = reflects′ (λ _ → refl) (contradiction a≡b) (proof (a ≟ b))
+  ≡-normalise-constant : ∀ {x y} (p q : x ≡ y) → ≡-normalise p ≡ ≡-normalise q
+  ≡-normalise-constant {x} {y} x≡y _
+    = reflects′ (λ _ → refl) (contradiction x≡y) (proof (x ≟ y))
 
   ≡-irrelevant : UIP A
   ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant

From 3e174d64e5e9ac69b0b3f2ad59ead95c1db69f54 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 7 Nov 2023 09:21:01 +0000
Subject: [PATCH 25/33] refactoring: names

---
 src/Relation/Nullary/Reflects.agda | 71 ++++++++++++++++--------------
 1 file changed, 37 insertions(+), 34 deletions(-)

diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index b93ec089e7..97254266d7 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -42,34 +42,35 @@ data Reflects (A : Set a) : Bool → Set a where
 
 -- NB. not the maximally dependent eliminator, but mostly sufficent
 
-reflects : (C : Bool → Set c) → (A → C true) → (¬ A → C false) →
-           ∀ {b} → Reflects A b → C b
-reflects C t f (ofⁿ ¬a) = f ¬a
-reflects C t f (ofʸ  a) = t a
+reflects⁻ : (C : Bool → Set c) → (A → C true) → (¬ A → C false) →
+            ∀ {b} → Reflects A b → C b
+reflects⁻ C t f (ofⁿ ¬a) = f ¬a
+reflects⁻ C t f (ofʸ  a) = t a
 
-reflects′ : (A → B) → (¬ A → B) → ∀ {b} → Reflects A b → B
-reflects′ {B = B} = reflects (const B)
+reflects′ : ∀ (C : Set c) → (A → C) → (¬ A → C) → ∀ {b} → Reflects A b → C
+reflects′ C = reflects⁻ (const C)
 
 -- In this case, `of` works like the relevant 'computed constructor'
--- (`ofⁿ` or `ofʸ`), and its inverse `of⁻¹` strips off the constructor
+-- (`ofⁿ` or `ofʸ`), and its inverse `reflects⁻¹` strips off the constructor
 -- to just give either the proof of `A` or the proof of `¬ A`.
 
-of : ∀ {b} → if b then A else ¬ A → Reflects A b
-of {b = false} = ofⁿ
-of {b = true } = ofʸ
+reflects : ∀ {b} → if b then A else ¬ A → Reflects A b
+reflects {b = false} = ofⁿ
+reflects {b = true } = ofʸ
 
-of⁻¹ : ∀ {b} → Reflects A b → if b then A else ¬ A
-of⁻¹ {A = A} = reflects (if_then A else ¬ A) id id
+reflects⁻¹ : ∀ {b} → Reflects A b → if b then A else ¬ A
+reflects⁻¹ {A = A} = reflects⁻ (if_then A else ¬ A) id id
 
 -- in lieu of a distinct `Reflects.Properties` module
 
-of⁻¹∘of≗id : ∀ {b} (r : if b then A else ¬ A) → of⁻¹ (of {b = b} r) ≡ r
-of⁻¹∘of≗id {b = false} _ = refl
-of⁻¹∘of≗id {b = true}  _ = refl
+reflects⁻¹∘reflects≗id : ∀ {b} (r : if b then A else ¬ A) →
+                         reflects⁻¹ (reflects {b = b} r) ≡ r
+reflects⁻¹∘reflects≗id {b = false} _ = refl
+reflects⁻¹∘reflects≗id {b = true}  _ = refl
 
-of∘of⁻¹≗id : ∀ {b} (r : Reflects A b) → of (of⁻¹ r) ≡ r
-of∘of⁻¹≗id (ofʸ a)  = refl
-of∘of⁻¹≗id (ofⁿ ¬a) = refl
+reflects∘reflects⁻¹≗id : ∀ {b} (r : Reflects A b) → reflects (reflects⁻¹ r) ≡ r
+reflects∘reflects⁻¹≗id (ofʸ a)  = refl
+reflects∘reflects⁻¹≗id (ofⁿ ¬a) = refl
 
 
 ------------------------------------------------------------------------
@@ -82,7 +83,7 @@ Recomputable A = .A → A
 -- be recomputed and subsequently used in relevant contexts.
 
 recompute : ∀ {b} → Reflects A b → Recomputable A
-recompute {A = A} = reflects′ {B = Recomputable A} (λ a _ → a) (λ ¬a a → ⊥-elim (¬a a))
+recompute {A = A} = reflects′ (Recomputable A) (λ a _ → a) (λ ¬a a → ⊥-elim (¬a a))
 
 ------------------------------------------------------------------------
 -- Interaction with negation, product, sums etc.
@@ -91,39 +92,39 @@ infixr 1 _⊎-reflects_
 infixr 2 _×-reflects_ _→-reflects_
 
 T-reflects : ∀ b → Reflects (T b) b
-T-reflects true  = of _
-T-reflects false = of id
+T-reflects true  = reflects _
+T-reflects false = reflects id
 
 -- If we can decide A, then we can decide its negation.
 ¬-reflects : ∀ {b} → Reflects A b → Reflects (¬ A) (not b)
-¬-reflects {A = A} = reflects (Reflects (¬ A) ∘ not) (of ∘ flip _$_) of
+¬-reflects {A = A} = reflects⁻ (Reflects (¬ A) ∘ not) (reflects ∘ flip _$_) reflects
 
 -- If we can decide A and B then we can decide their product, sum and implication
 _×-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 = reflects (a , b)
+ofʸ  a ×-reflects ofⁿ ¬b = reflects (¬b ∘ proj₂)
+ofⁿ ¬a ×-reflects _      = reflects (¬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      _ = reflects (inj₁ a)
+ofⁿ ¬a ⊎-reflects ofʸ  b = reflects (inj₂ b)
+ofⁿ ¬a ⊎-reflects ofⁿ ¬b = reflects (¬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 = reflects (const b)
+ofʸ  a →-reflects ofⁿ ¬b = reflects (¬b ∘ (_$ a))
+ofⁿ ¬a →-reflects _      = reflects (flip 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 = reflects (sound _)
+fromEquivalence {b = false} sound complete = reflects complete
 
 -- `Reflects` is deterministic.
 det : ∀ {b b′} → Reflects A b → Reflects A b′ → b ≡ b′
@@ -144,4 +145,6 @@ T-reflects-elim {a} r = det r (T-reflects a)
 
 -- Version 2.1
 
-invert = of⁻¹ -- against subsequent deprecation; no warning issued yet
+-- against subsequent deprecation; no warnings issued yet
+invert = reflects⁻¹
+of = reflects

From 9ec839900e52ab7175e28b8d2c88597acdf0944a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 7 Nov 2023 09:26:23 +0000
Subject: [PATCH 26/33] knock-on consequences: implicit to explicit

---
 src/Axiom/UniquenessOfIdentityProofs.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Axiom/UniquenessOfIdentityProofs.agda b/src/Axiom/UniquenessOfIdentityProofs.agda
index 7290f76190..8f52653c18 100644
--- a/src/Axiom/UniquenessOfIdentityProofs.agda
+++ b/src/Axiom/UniquenessOfIdentityProofs.agda
@@ -65,11 +65,11 @@ module Constant⇒UIP (f : _≡_ {A = A} ⇒ _≡_)
 module Decidable⇒UIP (_≟_ : Decidable {A = A} _≡_) where
 
   ≡-normalise : _≡_ {A = A} ⇒ _≡_
-  ≡-normalise {x} {y} x≡y = reflects′ id (contradiction x≡y) (proof (x ≟ y))
+  ≡-normalise {x} {y} x≡y = reflects′ (x ≡ y) id (contradiction x≡y) (proof (x ≟ y))
 
   ≡-normalise-constant : ∀ {x y} (p q : x ≡ y) → ≡-normalise p ≡ ≡-normalise q
   ≡-normalise-constant {x} {y} x≡y _
-    = reflects′ (λ _ → refl) (contradiction x≡y) (proof (x ≟ y))
+    = reflects′ _ (λ _ → refl) (contradiction x≡y) (proof (x ≟ y))
 
   ≡-irrelevant : UIP A
   ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant

From ec880fb3f145cdc95f735896c17f13abba0d779a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 8 Mar 2024 09:07:31 +0000
Subject: [PATCH 27/33] reverted changes to `README.Design.Decidability` in an
 effort to resolve merge conflict

---
 README/Design/Decidability.agda | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/README/Design/Decidability.agda b/README/Design/Decidability.agda
index d38bcfba4a..c6f086424f 100644
--- a/README/Design/Decidability.agda
+++ b/README/Design/Decidability.agda
@@ -31,14 +31,14 @@ infix 4 _≟₀_ _≟₁_ _≟₂_
 -- a proof of `Reflects P false` amounts to a refutation of `P`.
 
 ex₀ : (n : ℕ) → Reflects (n ≡ n) true
-ex₀ n = of refl
+ex₀ n = ofʸ refl
 
 ex₁ : (n : ℕ) → Reflects (zero ≡ suc n) false
-ex₁ n = of λ ()
+ex₁ n = ofⁿ λ ()
 
 ex₂ : (b : Bool) → Reflects (T b) b
-ex₂ false = of id
-ex₂ true  = of tt
+ex₂ false = ofⁿ id
+ex₂ true  = ofʸ tt
 
 ------------------------------------------------------------------------
 -- Dec
@@ -85,8 +85,8 @@ zero  ≟₁ suc n = no λ ()
 suc m ≟₁ zero  = no λ ()
 does  (suc m ≟₁ suc n) = does (m ≟₁ n)
 proof (suc m ≟₁ suc n) with m ≟₁ n
-... | yes p = of (cong suc p)
-... | no ¬p = of (¬p ∘ suc-injective)
+... | yes p = ofʸ (cong suc p)
+... | no ¬p = ofⁿ (¬p ∘ suc-injective)
 
 -- We now get definitional equalities such as the following.
 

From 6d473aadbc93e1ab1503e4c3de4a90818f74e167 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 8 Mar 2024 09:13:32 +0000
Subject: [PATCH 28/33] restored changes to `README.Design.Decidability` after
 resolving merge conflict

---
 doc/README/Design/Decidability.agda | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/doc/README/Design/Decidability.agda b/doc/README/Design/Decidability.agda
index c6f086424f..d38bcfba4a 100644
--- a/doc/README/Design/Decidability.agda
+++ b/doc/README/Design/Decidability.agda
@@ -31,14 +31,14 @@ infix 4 _≟₀_ _≟₁_ _≟₂_
 -- a proof of `Reflects P false` amounts to a refutation of `P`.
 
 ex₀ : (n : ℕ) → Reflects (n ≡ n) true
-ex₀ n = ofʸ refl
+ex₀ n = of refl
 
 ex₁ : (n : ℕ) → Reflects (zero ≡ suc n) false
-ex₁ n = ofⁿ λ ()
+ex₁ n = of λ ()
 
 ex₂ : (b : Bool) → Reflects (T b) b
-ex₂ false = ofⁿ id
-ex₂ true  = ofʸ tt
+ex₂ false = of id
+ex₂ true  = of tt
 
 ------------------------------------------------------------------------
 -- Dec
@@ -85,8 +85,8 @@ zero  ≟₁ suc n = no λ ()
 suc m ≟₁ zero  = no λ ()
 does  (suc m ≟₁ suc n) = does (m ≟₁ n)
 proof (suc m ≟₁ suc n) with m ≟₁ n
-... | yes p = ofʸ (cong suc p)
-... | no ¬p = ofⁿ (¬p ∘ suc-injective)
+... | yes p = of (cong suc p)
+... | no ¬p = of (¬p ∘ suc-injective)
 
 -- We now get definitional equalities such as the following.
 

From cb52c089a11c6a927c9ef1160c8d1270c420c762 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 8 Mar 2024 09:19:40 +0000
Subject: [PATCH 29/33] fix imports

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

diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index c339ef0aac..588bdaa6a8 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -17,7 +17,8 @@ open import Function.Bundles using
 open import Relation.Binary.Bundles using (Setoid; module Setoid)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary using (invert; ¬_; contradiction; Irrelevant)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong′)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; refl; sym; trans; cong′)
 
 private
   variable

From 27234f7dce32e2d5ff501f716a0ca3ae81d21452 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 8 Mar 2024 09:19:48 +0000
Subject: [PATCH 30/33] temporary fix to resolve multiple definitions

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

diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index 07471c7e4a..c56eb2766d 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -36,11 +36,11 @@ Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
 
 ------------------------------------------------------------------------
 -- Recomputability - we can rebuild a relevant proof given an
--- irrelevant one.
-
+-- irrelevant one. NOW moved to Relation.Nullary.Reflects
+{-
 Recomputable : Set p → Set p
 Recomputable P = .P → P
-
+-}
 ------------------------------------------------------------------------
 -- Weak decidability
 -- `nothing` is 'don't know'/'give up'; `just` is `yes`/`definitely`

From b6abf30fe1785a627165810c99f5192279c641ca Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 27 Mar 2024 10:43:21 +0000
Subject: [PATCH 31/33] `fix-whitespace`

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

diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 588bdaa6a8..b9565cf0dc 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -31,7 +31,7 @@ private
 open import Relation.Nullary.Decidable.Core public
 
 ------------------------------------------------------------------------
--- Characterisation : Dec A ⇔ there exists a Bool b st A ⇔ T b 
+-- Characterisation : Dec A ⇔ there exists a Bool b st A ⇔ T b
 
 -- forwards direction: use `does`
 

From 2a8b773d25f64ddd3a91e0251e82bc3196b4873a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 8 Apr 2024 09:01:54 +0100
Subject: [PATCH 32/33] use `recompute` directly

---
 src/Axiom/UniquenessOfIdentityProofs.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Axiom/UniquenessOfIdentityProofs.agda b/src/Axiom/UniquenessOfIdentityProofs.agda
index 8f52653c18..793ea9173b 100644
--- a/src/Axiom/UniquenessOfIdentityProofs.agda
+++ b/src/Axiom/UniquenessOfIdentityProofs.agda
@@ -10,7 +10,7 @@ module Axiom.UniquenessOfIdentityProofs where
 
 open import Function.Base using (id; const; flip)
 open import Level using (Level)
-open import Relation.Nullary using (contradiction; reflects′; proof)
+open import Relation.Nullary using (contradiction; reflects′; recompute; proof)
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality.Core
@@ -65,7 +65,7 @@ module Constant⇒UIP (f : _≡_ {A = A} ⇒ _≡_)
 module Decidable⇒UIP (_≟_ : Decidable {A = A} _≡_) where
 
   ≡-normalise : _≡_ {A = A} ⇒ _≡_
-  ≡-normalise {x} {y} x≡y = reflects′ (x ≡ y) id (contradiction x≡y) (proof (x ≟ y))
+  ≡-normalise {x} {y} x≡y = recompute (x ≟ y) x≡y
 
   ≡-normalise-constant : ∀ {x y} (p q : x ≡ y) → ≡-normalise p ≡ ≡-normalise q
   ≡-normalise-constant {x} {y} x≡y _

From 16776b5b350191eb18deda20afd9f32680bcfc53 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 8 Apr 2024 11:26:36 +0100
Subject: [PATCH 33/33] `UIP` in terms of `recompute`

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

diff --git a/src/Axiom/UniquenessOfIdentityProofs.agda b/src/Axiom/UniquenessOfIdentityProofs.agda
index 793ea9173b..6975481cdb 100644
--- a/src/Axiom/UniquenessOfIdentityProofs.agda
+++ b/src/Axiom/UniquenessOfIdentityProofs.agda
@@ -10,7 +10,7 @@ module Axiom.UniquenessOfIdentityProofs where
 
 open import Function.Base using (id; const; flip)
 open import Level using (Level)
-open import Relation.Nullary using (contradiction; reflects′; recompute; proof)
+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
@@ -68,8 +68,7 @@ module Decidable⇒UIP (_≟_ : Decidable {A = A} _≡_) where
   ≡-normalise {x} {y} x≡y = recompute (x ≟ y) x≡y
 
   ≡-normalise-constant : ∀ {x y} (p q : x ≡ y) → ≡-normalise p ≡ ≡-normalise q
-  ≡-normalise-constant {x} {y} x≡y _
-    = reflects′ _ (λ _ → refl) (contradiction x≡y) (proof (x ≟ y))
+  ≡-normalise-constant {x} {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 c56eb2766d..79bb2e9334 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -25,7 +25,7 @@ private
 
 open import Relation.Nullary.Negation.Core public
 open import Relation.Nullary.Reflects public
-  hiding (recompute; fromEquivalence)
+  hiding (recompute; recompute-irr; fromEquivalence)
 open import Relation.Nullary.Decidable.Core public
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index c0108e30d5..6ec4166a6d 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 (id; _∘_; const; _$_; flip)
 open import Relation.Nullary.Reflects as Reflects
-  using (Reflects; of; invert; Recomputable)
+  using (Reflects; of; invert; reflects′; Recomputable)
 open import Relation.Nullary.Negation.Core
   using (¬_; contradiction; Stable; DoubleNegation; negated-stable)
+open import Agda.Builtin.Equality using (_≡_)
 
 private
   variable
@@ -103,6 +104,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 97254266d7..5e0ba46478 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -85,6 +85,9 @@ Recomputable A = .A → A
 recompute : ∀ {b} → Reflects A b → Recomputable A
 recompute {A = A} = reflects′ (Recomputable A) (λ a _ → a) (λ ¬a a → ⊥-elim (¬a a))
 
+recompute-irr : ∀ {b} (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
+recompute-irr {A = A} r p q = refl
+
 ------------------------------------------------------------------------
 -- Interaction with negation, product, sums etc.