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.
 
diff --git a/src/Axiom/UniquenessOfIdentityProofs.agda b/src/Axiom/UniquenessOfIdentityProofs.agda
index 1cefc1a6a1..6975481cdb 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.Decidable.Core using (recompute; recompute-irr)
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
 
+private
+  variable
+    a : Level
+    A : Set a
+
 ------------------------------------------------------------------------
 -- 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,13 @@ module Constant⇒UIP
 -- function over proofs of equality which is constant: it returns the
 -- proof produced by the decision procedure.
 
-module Decidable⇒UIP
-  {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
-  where
+module Decidable⇒UIP (_≟_ : Decidable {A = A} _≡_) where
 
   ≡-normalise : _≡_ {A = A} ⇒ _≡_
-  ≡-normalise {a} {b} a≡b with a ≟ b
-  ... | true  because  [p] = invert [p]
-  ... | false because [¬p] = ⊥-elim (invert [¬p] a≡b)
-
-  ≡-normalise-constant : ∀ {a b} (p q : a ≡ b) → ≡-normalise p ≡ ≡-normalise q
-  ≡-normalise-constant {a} {b} p q with a ≟ b
-  ... | true  because   _  = refl
-  ... | false because [¬p] = ⊥-elim (invert [¬p] p)
+  ≡-normalise {x} {y} x≡y = recompute (x ≟ y) x≡y
+
+  ≡-normalise-constant : ∀ {x y} (p q : x ≡ y) → ≡-normalise p ≡ ≡-normalise q
+  ≡-normalise-constant {x} {y} = recompute-irr (x ≟ y)
 
   ≡-irrelevant : UIP A
   ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index b09b46db7d..9499d5685b 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
@@ -35,10 +34,10 @@ 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 (True; via-injection; map′)
+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 using (fromEquivalence)
+open import Relation.Nullary.Reflects as Reflects using (Reflects)
 
 open import Algebra.Definitions {A = ℕ} _≡_
   hiding (LeftCancellative; RightCancellative; Cancellative)
@@ -135,7 +134,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 _≤ᵇ_
@@ -150,7 +149,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 _≤_
diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index 92e0607f4d..79bb2e9334 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -25,6 +25,7 @@ private
 
 open import Relation.Nullary.Negation.Core public
 open import Relation.Nullary.Reflects public
+  hiding (recompute; recompute-irr; fromEquivalence)
 open import Relation.Nullary.Decidable.Core public
 
 ------------------------------------------------------------------------
@@ -35,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`
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 4335a5df5a..b9565cf0dc 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.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
-open import Relation.Nullary.Reflects using (invert)
+open import Relation.Nullary using (invert; ¬_; contradiction; Irrelevant)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; sym; trans; cong′)
 
@@ -32,6 +30,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
 
@@ -52,23 +70,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
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 83da26e51b..6ec4166a6d 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -14,17 +14,18 @@ module Relation.Nullary.Decidable.Core where
 open import Level using (Level; Lift)
 open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
 open import Data.Unit.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 Function.Base using (id; _∘_; const; _$_; flip)
+open import Relation.Nullary.Reflects as Reflects
+  using (Reflects; of; invert; reflects′; Recomputable)
 open import Relation.Nullary.Negation.Core
-  using (¬_; Stable; negated-stable; contradiction; DoubleNegation)
+  using (¬_; contradiction; Stable; DoubleNegation; negated-stable)
+open import Agda.Builtin.Equality using (_≡_)
 
 private
   variable
-    a b : Level
+    a : Level
     A B : Set a
 
 ------------------------------------------------------------------------
@@ -48,8 +49,39 @@ 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 'pattern' _ᵖ versions of `yes` and `no`
+pattern yesᵖ [a] =  true because  [a]
+pattern noᵖ [¬a] = false because [¬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
@@ -69,9 +101,11 @@ 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-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.
@@ -79,24 +113,24 @@ recompute (no ¬a) a = ⊥-elim (¬a a)
 infixr 1 _⊎-dec_
 infixr 2 _×-dec_ _→-dec_
 
-T? : ∀ x → Dec (T x)
-T? x = x because 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?)
-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
@@ -107,8 +141,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
@@ -127,42 +161,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]} _ = invert [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]} = invert [¬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]} _  = invert [¬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 _$_ (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 (true  because [a]) = invert [a]
-from-yes (false because _ ) = _
+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 (false because [¬a]) = invert [¬a]
-from-no (true  because   _ ) = _
+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 (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 (invert [a]))
+proof (map′ A→B B→A (noᵖ [¬a])) = of (invert [¬a] ∘ B→A)
 
 ------------------------------------------------------------------------
 -- Relationship with double-negation
@@ -170,8 +204,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 (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?)
@@ -180,7 +214,7 @@ decidable-stable (no ¬a) ¬¬a = contradiction ¬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)))
 
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 3b301fdbce..5e0ba46478 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -11,18 +11,17 @@ module Relation.Nullary.Reflects where
 open import Agda.Builtin.Equality
 
 open import Data.Bool.Base
-open import Data.Unit.Base using (⊤)
-open import Data.Empty
+open import Data.Empty.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; id)
+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
 
 ------------------------------------------------------------------------
@@ -39,18 +38,55 @@ 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 `invert` 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.
 
-of : ∀ {b} → if b then A else ¬ A → Reflects A b
-of {b = false} ¬a = ofⁿ ¬a
-of {b = true }  a = 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′ : ∀ (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 `reflects⁻¹` strips off the constructor
+-- to just give either the proof of `A` or the proof of `¬ A`.
+
+reflects : ∀ {b} → if b then A else ¬ A → Reflects A b
+reflects {b = false} = ofⁿ
+reflects {b = true } = ofʸ
+
+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
+
+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
+
+reflects∘reflects⁻¹≗id : ∀ {b} (r : Reflects A b) → reflects (reflects⁻¹ r) ≡ r
+reflects∘reflects⁻¹≗id (ofʸ a)  = refl
+reflects∘reflects⁻¹≗id (ofⁿ ¬a) = refl
 
-invert : ∀ {b} → Reflects A b → if b then A else ¬ A
-invert (ofʸ  a) = a
-invert (ofⁿ ¬a) = ¬a
+
+------------------------------------------------------------------------
+-- 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′ (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.
@@ -59,39 +95,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 (ofʸ  a) = ofⁿ (_$ a)
-¬-reflects (ofⁿ ¬a) = ofʸ ¬a
+¬-reflects {A = A} = reflects⁻ (Reflects (¬ A) ∘ not) (reflects ∘ flip _$_) reflects
 
--- 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)
-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ʸ (⊥-elim ∘ ¬a)
+               Reflects (A → B) (not a ∨ b)
+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′
@@ -102,3 +138,16 @@ det (ofⁿ ¬a) (ofⁿ  _) = refl
 
 T-reflects-elim : ∀ {a b} → Reflects (T a) b → b ≡ a
 T-reflects-elim {a} r = det r (T-reflects a)
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.1
+
+-- against subsequent deprecation; no warnings issued yet
+invert = reflects⁻¹
+of = reflects