From e3a3ad0d9072e3587fd248715638578d23632b11 Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Tue, 31 Oct 2023 15:53:46 +0900
Subject: [PATCH 1/5] Move `T?` to `Relation.Nullary.Decidable.Core`

---
 CHANGELOG.md                             |  8 +++++
 notes/style-guide.md                     |  2 +-
 src/Data/Bool.agda                       |  3 --
 src/Data/Bool/Base.agda                  | 18 +++++-----
 src/Data/Bool/Properties.agda            | 42 +++++++++++++-----------
 src/Relation/Nullary.agda                | 17 ++--------
 src/Relation/Nullary/Decidable/Core.agda |  6 +++-
 src/Relation/Nullary/Reflects.agda       | 42 +++++++++++++-----------
 8 files changed, 72 insertions(+), 66 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9d9f403d64..36cf98fb1b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -838,6 +838,9 @@ Non-backwards compatible changes
 
   4. The modules `Relation.Nullary.(Product/Sum/Implication)` have been deprecated
          and their contents moved to `Relation.Nullary.(Negation/Reflects/Decidable)`.
+		 
+  5. The proof `T?` has been moved from `Data.Bool.Properties` to `Relation.Nullary.Decidable.Core`
+	 (but is still re-exported by the former).
 
   as well as the following breaking changes:
 
@@ -3563,6 +3566,11 @@ Additions to existing modules
   poset          : Set a → Poset _ _ _
   ```
 
+* Added new proof in `Relation.Nullary.Reflects`:
+  ```agda
+  T-reflects : Reflects (T b) b
+  ```
+
 * Added new operations in `System.Exit`:
   ```
   isSuccess : ExitCode → Bool
diff --git a/notes/style-guide.md b/notes/style-guide.md
index d6201abe88..c79d8ca2e3 100644
--- a/notes/style-guide.md
+++ b/notes/style-guide.md
@@ -402,7 +402,7 @@ word within a compound word is capitalized except for the first word.
 
 * Rational variables are named `p`, `q`, `r`, ... (default `p`)
 
-* All other variables tend to be named `x`, `y`, `z`.
+* All other variables, including `Bool`, should be named `x`, `y`, `z`.
 
 * Collections of elements are usually indicated by appending an `s`
   (e.g. if you are naming your variables `x` and `y` then lists
diff --git a/src/Data/Bool.agda b/src/Data/Bool.agda
index 1270125254..55ed146e2c 100644
--- a/src/Data/Bool.agda
+++ b/src/Data/Bool.agda
@@ -8,9 +8,6 @@
 
 module Data.Bool where
 
-open import Relation.Nullary
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
-
 ------------------------------------------------------------------------
 -- The boolean type and some operations
 
diff --git a/src/Data/Bool/Base.agda b/src/Data/Bool/Base.agda
index bc2e67644b..ea99ee880d 100644
--- a/src/Data/Bool/Base.agda
+++ b/src/Data/Bool/Base.agda
@@ -57,17 +57,19 @@ true  xor b = not b
 false xor b = b
 
 ------------------------------------------------------------------------
--- Other operations
-
-infix  0 if_then_else_
-
-if_then_else_ : Bool → A → A → A
-if true  then t else f = t
-if false then t else f = f
+-- Conversion to Set
 
 -- A function mapping true to an inhabited type and false to an empty
 -- type.
-
 T : Bool → Set
 T true  = ⊤
 T false = ⊥
+
+------------------------------------------------------------------------
+-- Other operations
+
+infix 0 if_then_else_
+
+if_then_else_ : Bool → A → A → A
+if true  then t else f = t
+if false then t else f = f
diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index e911390366..70afaa07ba 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -29,7 +29,7 @@ open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
 open import Relation.Nullary.Reflects using (ofʸ; ofⁿ)
-open import Relation.Nullary.Decidable.Core using (True; does; proof; yes; no)
+open import Relation.Nullary.Decidable.Core using (True; does; proof; yes; no; fromWitness)
 import Relation.Unary as U
 
 open import Algebra.Definitions {A = Bool} _≡_
@@ -726,15 +726,17 @@ xor-∧-commutativeRing = ⊕-∧-commutativeRing
   open XorRing _xor_ xor-is-ok
 
 ------------------------------------------------------------------------
--- Miscellaneous other properties
+-- Properties of if_then_else_
 
-⇔→≡ : {x y z : Bool} → x ≡ z ⇔ y ≡ z → x ≡ y
-⇔→≡ {true } {true }         hyp = refl
-⇔→≡ {true } {false} {true } hyp = sym (Equivalence.to hyp refl)
-⇔→≡ {true } {false} {false} hyp = Equivalence.from hyp refl
-⇔→≡ {false} {true } {true } hyp = Equivalence.from hyp refl
-⇔→≡ {false} {true } {false} hyp = sym (Equivalence.to hyp refl)
-⇔→≡ {false} {false}         hyp = refl
+if-float : ∀ (f : A → B) b {x y} →
+           f (if b then x else y) ≡ (if b then f x else f y)
+if-float _ true  = refl
+if-float _ false = refl
+
+------------------------------------------------------------------------
+-- Properties of T
+
+open Relation.Nullary.Decidable.Core public using (T?)
 
 T-≡ : ∀ {x} → T x ⇔ x ≡ true
 T-≡ {false} = mk⇔ (λ ())       (λ ())
@@ -757,18 +759,20 @@ T-∨ {false} {false} = mk⇔ inj₁ [ id , id ]
 T-irrelevant : U.Irrelevant T
 T-irrelevant {true}  _  _  = refl
 
-T? : U.Decidable T
-does  (T? b) = b
-proof (T? true ) = ofʸ _
-proof (T? false) = ofⁿ λ()
-
 T?-diag : ∀ b → T b → True (T? b)
-T?-diag true  _ = _
+T?-diag b = fromWitness
+
+------------------------------------------------------------------------
+-- Miscellaneous other properties
+
+⇔→≡ : {x y z : Bool} → x ≡ z ⇔ y ≡ z → x ≡ y
+⇔→≡ {true } {true }         hyp = refl
+⇔→≡ {true } {false} {true } hyp = sym (Equivalence.to hyp refl)
+⇔→≡ {true } {false} {false} hyp = Equivalence.from hyp refl
+⇔→≡ {false} {true } {true } hyp = Equivalence.from hyp refl
+⇔→≡ {false} {true } {false} hyp = sym (Equivalence.to hyp refl)
+⇔→≡ {false} {false}         hyp = refl
 
-if-float : ∀ (f : A → B) b {x y} →
-           f (if b then x else y) ≡ (if b then f x else f y)
-if-float _ true  = refl
-if-float _ false = refl
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index b8a4c30470..0b0f83f77b 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -15,20 +15,9 @@ open import Agda.Builtin.Equality
 ------------------------------------------------------------------------
 -- Re-exports
 
-open import Relation.Nullary.Negation.Core public using
-  ( ¬_; _¬-⊎_
-  ; contradiction; contradiction₂; contraposition
-  )
-
-open import Relation.Nullary.Reflects public using
-  ( Reflects; ofʸ; ofⁿ
-  ; _×-reflects_; _⊎-reflects_; _→-reflects_
-  )
-
-open import Relation.Nullary.Decidable.Core public using
-  ( Dec; does; proof; yes; no; _because_; recompute
-  ; ¬?; _×-dec_; _⊎-dec_; _→-dec_
-  )
+open import Relation.Nullary.Negation.Core public
+open import Relation.Nullary.Reflects public
+open import Relation.Nullary.Decidable.Core public
 
 ------------------------------------------------------------------------
 -- Irrelevant types
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 166b1f264e..3b4f9e8cbc 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; false; true; not; T; _∧_; _∨_)
+open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
 open import Data.Unit.Base using (⊤)
 open import Data.Empty using (⊥)
 open import Data.Empty.Irrelevant using (⊥-elim)
@@ -79,6 +79,10 @@ recompute (no ¬a) a = ⊥-elim (¬a a)
 infixr 1 _⊎-dec_
 infixr 2 _×-dec_ _→-dec_
 
+T? : ∀ b → Dec (T b)
+does  (T? b) = b
+proof (T? b) = T-reflects b
+
 ¬? : Dec A → Dec (¬ A)
 does  (¬? a?) = not (does a?)
 proof (¬? a?) = ¬-reflects (proof a?)
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 4f97bd8709..eae738262a 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -11,11 +11,12 @@ module Relation.Nullary.Reflects where
 open import Agda.Builtin.Equality
 
 open import Data.Bool.Base
+open import Data.Unit.Base using (⊤)
 open import Data.Empty
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Level using (Level)
-open import Function.Base using (_$_; _∘_; const)
+open import Function.Base using (_$_; _∘_; const; id)
 
 open import Relation.Nullary.Negation.Core
 
@@ -23,6 +24,7 @@ private
   variable
     a : Level
     A B : Set a
+    x y : Bool
 
 ------------------------------------------------------------------------
 -- `Reflects` idiom.
@@ -43,41 +45,41 @@ data Reflects (A : Set a) : Bool → Set a where
 -- `ofʸ`), and `invert` 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} ¬a = ofⁿ ¬a
-of {b = true }  a = ofʸ a
+of : if x then A else ¬ A → Reflects A x
+of {x = false} ¬a = ofⁿ ¬a
+of {x = true }  a = ofʸ a
 
-invert : ∀ {b} → Reflects A b → if b then A else ¬ A
+invert : Reflects A x → if x then A else ¬ A
 invert (ofʸ  a) = a
 invert (ofⁿ ¬a) = ¬a
 
 ------------------------------------------------------------------------
 -- Interaction with negation, product, sums etc.
 
+infixr 1 _⊎-reflects_
+infixr 2 _×-reflects_ _→-reflects_
+
+T-reflects : ∀ x → Reflects (T x) x
+T-reflects true  = of _
+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 : Reflects A x → Reflects (¬ A) (not x)
 ¬-reflects (ofʸ  a) = ofⁿ (_$ a)
 ¬-reflects (ofⁿ ¬a) = ofʸ ¬a
 
 -- 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)
+_×-reflects_ : Reflects A x → Reflects B y → Reflects (A × B) (x ∧ y)
 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)
+_⊎-reflects_ : Reflects A x → Reflects B y → Reflects (A ⊎ B) (x ∨ y)
 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)
+_→-reflects_ : Reflects A x → Reflects B y → Reflects (A → B) (not x ∨ y)
 ofʸ  a →-reflects ofʸ  b = ofʸ (const b)
 ofʸ  a →-reflects ofⁿ ¬b = ofⁿ (¬b ∘ (_$ a))
 ofⁿ ¬a →-reflects _      = ofʸ (⊥-elim ∘ ¬a)
@@ -85,12 +87,12 @@ ofⁿ ¬a →-reflects _      = ofʸ (⊥-elim ∘ ¬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 : (T x → A) → (A → T x) → Reflects A x
+fromEquivalence {x = true}  sound complete = ofʸ (sound _)
+fromEquivalence {x = false} sound complete = ofⁿ complete
 
 -- `Reflects` is deterministic.
-det : ∀ {b b′} → Reflects A b → Reflects A b′ → b ≡ b′
+det : Reflects A x → Reflects A y → x ≡ y
 det (ofʸ  a) (ofʸ  _) = refl
 det (ofʸ  a) (ofⁿ ¬a) = contradiction a ¬a
 det (ofⁿ ¬a) (ofʸ  a) = contradiction a ¬a

From ea53921c9f33c9ac0efd426f8048278fa505c716 Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Tue, 31 Oct 2023 16:38:51 +0900
Subject: [PATCH 2/5] Var name fix

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

diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 3b4f9e8cbc..a27658aef1 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -79,9 +79,9 @@ recompute (no ¬a) a = ⊥-elim (¬a a)
 infixr 1 _⊎-dec_
 infixr 2 _×-dec_ _→-dec_
 
-T? : ∀ b → Dec (T b)
-does  (T? b) = b
-proof (T? b) = T-reflects b
+T? : ∀ x → Dec (T x)
+does  (T? x) = x
+proof (T? x) = T-reflects x
 
 ¬? : Dec A → Dec (¬ A)
 does  (¬? a?) = not (does a?)

From bfb7959be82f81ff9b2f4142d3bb054413b7def3 Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Wed, 1 Nov 2023 12:02:01 +0900
Subject: [PATCH 3/5] Some refactoring

---
 src/Data/Bool/Properties.agda            | 3 +--
 src/Relation/Nullary/Decidable/Core.agda | 3 +--
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index 70afaa07ba..bb8cda9a0e 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -28,8 +28,7 @@ open import Relation.Binary.Definitions
   using (Decidable; Reflexive; Transitive; Antisymmetric; Minimum; Maximum; Total; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri<; tri>; _Respects₂_)
 open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
-open import Relation.Nullary.Reflects using (ofʸ; ofⁿ)
-open import Relation.Nullary.Decidable.Core using (True; does; proof; yes; no; fromWitness)
+open import Relation.Nullary.Decidable.Core using (True; yes; no; fromWitness)
 import Relation.Unary as U
 
 open import Algebra.Definitions {A = Bool} _≡_
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index a27658aef1..bf6d426a2f 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -80,8 +80,7 @@ infixr 1 _⊎-dec_
 infixr 2 _×-dec_ _→-dec_
 
 T? : ∀ x → Dec (T x)
-does  (T? x) = x
-proof (T? x) = T-reflects x
+T? x = x because T-reflects x
 
 ¬? : Dec A → Dec (¬ A)
 does  (¬? a?) = not (does a?)

From e42161a2ccf75d824f2f3e3adc49d3e8f5829543 Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Wed, 1 Nov 2023 19:12:39 +0900
Subject: [PATCH 4/5] Fix failing tests and address remaining comments

---
 CHANGELOG.md                                  |  1 +
 README/Design/Hierarchies.agda                |  4 +--
 .../Relation/Binary/BagAndSetEquality.agda    |  2 +-
 src/Effect/Applicative.agda                   |  2 +-
 src/Function/Bundles.agda                     |  2 +-
 src/Relation/Nullary/Reflects.agda            | 33 +++++++++++--------
 6 files changed, 25 insertions(+), 19 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 36cf98fb1b..a64dd81168 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3569,6 +3569,7 @@ Additions to existing modules
 * Added new proof in `Relation.Nullary.Reflects`:
   ```agda
   T-reflects : Reflects (T b) b
+  T-reflects-elim : Reflects (T a) b → b ≡ a
   ```
 
 * Added new operations in `System.Exit`:
diff --git a/README/Design/Hierarchies.agda b/README/Design/Hierarchies.agda
index bc9220ba23..71ca5eed44 100644
--- a/README/Design/Hierarchies.agda
+++ b/README/Design/Hierarchies.agda
@@ -265,7 +265,7 @@ record Semigroup : Set (suc (a ⊔ ℓ)) where
 --       IsA                     A
 --    /  ||   \               /  ||  \
 -- IsB   IsC   IsD          B    C    D
- 
+
 -- The procedure for re-exports in the bundles is as follows:
 
 -- 1. `open IsA isA public using (IsC, M)` where `M` is everything
@@ -280,7 +280,7 @@ record Semigroup : Set (suc (a ⊔ ℓ)) where
 
 -- 5. `open B b public using (O)` where `O` is everything exported
 --    by `B` but not exported by `IsA`.
- 
+
 -- 6. Construct `d : D` via the `isC` obtained in step 1.
 
 -- 7. `open D d public using (P)` where `P` is everything exported
diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index 31ab6941ac..17af3d8955 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -44,7 +44,7 @@ import Relation.Binary.Reasoning.Preorder as PreorderReasoning
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; _≗_; refl)
 open import Relation.Binary.Reasoning.Syntax
-open import Relation.Nullary
+open import Relation.Nullary.Negation using (¬_)
 open import Data.List.Membership.Propositional.Properties
 
 private
diff --git a/src/Effect/Applicative.agda b/src/Effect/Applicative.agda
index a2263c6e0a..95e2debda8 100644
--- a/src/Effect/Applicative.agda
+++ b/src/Effect/Applicative.agda
@@ -56,7 +56,7 @@ record RawApplicative (F : Set f → Set g) : Set (suc f ⊔ g) where
   -- Haskell-style alternative name for pure
   return : A → F A
   return = pure
-  
+
   -- backwards compatibility: unicode variants
   _⊛_ : F (A → B) → F A → F B
   _⊛_ = _<*>_
diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda
index 9e18c30fe5..98aac7a48c 100644
--- a/src/Function/Bundles.agda
+++ b/src/Function/Bundles.agda
@@ -380,7 +380,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
   -- For further background on (split) surjections, one may consult any
   -- general mathematical references which work without the principle
   -- of choice. For example:
-  -- 
+  --
   --   https://ncatlab.org/nlab/show/split+epimorphism.
   --
   -- The connection to set-theoretic notions with the same names is
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index eae738262a..3b301fdbce 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -24,7 +24,6 @@ private
   variable
     a : Level
     A B : Set a
-    x y : Bool
 
 ------------------------------------------------------------------------
 -- `Reflects` idiom.
@@ -45,11 +44,11 @@ data Reflects (A : Set a) : Bool → Set a where
 -- `ofʸ`), and `invert` strips off the constructor to just give either
 -- the proof of `A` or the proof of `¬ A`.
 
-of : if x then A else ¬ A → Reflects A x
-of {x = false} ¬a = ofⁿ ¬a
-of {x = true }  a = ofʸ a
+of : ∀ {b} → if b then A else ¬ A → Reflects A b
+of {b = false} ¬a = ofⁿ ¬a
+of {b = true }  a = ofʸ a
 
-invert : Reflects A x → if x then A else ¬ A
+invert : ∀ {b} → Reflects A b → if b then A else ¬ A
 invert (ofʸ  a) = a
 invert (ofⁿ ¬a) = ¬a
 
@@ -59,27 +58,30 @@ invert (ofⁿ ¬a) = ¬a
 infixr 1 _⊎-reflects_
 infixr 2 _×-reflects_ _→-reflects_
 
-T-reflects : ∀ x → Reflects (T x) x
+T-reflects : ∀ b → Reflects (T b) b
 T-reflects true  = of _
 T-reflects false = of id
 
 -- If we can decide A, then we can decide its negation.
-¬-reflects : Reflects A x → Reflects (¬ A) (not x)
+¬-reflects : ∀ {b} → Reflects A b → Reflects (¬ A) (not b)
 ¬-reflects (ofʸ  a) = ofⁿ (_$ a)
 ¬-reflects (ofⁿ ¬a) = ofʸ ¬a
 
 -- If we can decide A and Q then we can decide their product
-_×-reflects_ : Reflects A x → Reflects B y → Reflects (A × B) (x ∧ y)
+_×-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₁)
 
-_⊎-reflects_ : Reflects A x → Reflects B y → Reflects (A ⊎ B) (x ∨ y)
+_⊎-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)
 
-_→-reflects_ : Reflects A x → Reflects B y → Reflects (A → B) (not x ∨ y)
+_→-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)
@@ -87,13 +89,16 @@ ofⁿ ¬a →-reflects _      = ofʸ (⊥-elim ∘ ¬a)
 ------------------------------------------------------------------------
 -- Other lemmas
 
-fromEquivalence : (T x → A) → (A → T x) → Reflects A x
-fromEquivalence {x = true}  sound complete = ofʸ (sound _)
-fromEquivalence {x = false} sound complete = ofⁿ complete
+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
 
 -- `Reflects` is deterministic.
-det : Reflects A x → Reflects A y → x ≡ y
+det : ∀ {b b′} → Reflects A b → Reflects A b′ → b ≡ b′
 det (ofʸ  a) (ofʸ  _) = refl
 det (ofʸ  a) (ofⁿ ¬a) = contradiction a ¬a
 det (ofⁿ ¬a) (ofʸ  a) = contradiction a ¬a
 det (ofⁿ ¬a) (ofⁿ  _) = refl
+
+T-reflects-elim : ∀ {a b} → Reflects (T a) b → b ≡ a
+T-reflects-elim {a} r = det r (T-reflects a)

From a17366465fab92143ed550509a723652f6ef71be Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Wed, 1 Nov 2023 19:17:42 +0900
Subject: [PATCH 5/5] Fix style-guide

---
 notes/style-guide.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/notes/style-guide.md b/notes/style-guide.md
index c79d8ca2e3..a74de87d4e 100644
--- a/notes/style-guide.md
+++ b/notes/style-guide.md
@@ -402,7 +402,7 @@ word within a compound word is capitalized except for the first word.
 
 * Rational variables are named `p`, `q`, `r`, ... (default `p`)
 
-* All other variables, including `Bool`, should be named `x`, `y`, `z`.
+* All other variables should be named `x`, `y`, `z`.
 
 * Collections of elements are usually indicated by appending an `s`
   (e.g. if you are naming your variables `x` and `y` then lists