From 4ac0a86da9a68e585519a43aec03362497b339f2 Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Thu, 28 Sep 2023 10:36:11 +0900
Subject: [PATCH 1/3] Modernise Relation.Nullary code

---
 src/Relation/Nullary/Decidable.agda      |  77 +++++-------
 src/Relation/Nullary/Decidable/Core.agda | 151 ++++++++++++-----------
 src/Relation/Nullary/Negation.agda       |  68 +++++-----
 src/Relation/Nullary/Negation/Core.agda  |  59 +++++----
 src/Relation/Nullary/Reflects.agda       |  80 ++++++------
 5 files changed, 212 insertions(+), 223 deletions(-)

diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 37d3e0904a..f0882f3098 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -11,22 +11,20 @@ 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 as Prod hiding (map)
-open import Data.Sum.Base as Sum hiding (map)
+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.Negation
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong′)
 
 private
   variable
-    p q r : Level
-    P Q R : Set p
+    a b ℓ₁ ℓ₂ : Level
+    A B : Set a
 
 ------------------------------------------------------------------------
 -- Re-exporting the core definitions
@@ -36,56 +34,49 @@ open import Relation.Nullary.Decidable.Core public
 ------------------------------------------------------------------------
 -- Maps
 
-map : P ⇔ Q → Dec P → Dec Q
-map P⇔Q = map′ to from
-  where open Equivalence P⇔Q
-
-module _ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
-         (inj : Injection A B)
-  where
-
-  open Injection inj
-  open Setoid A using () renaming (_≈_ to _≈A_)
-  open Setoid B using () renaming (_≈_ to _≈B_)
-
-  -- If there is an injection from one setoid to another, and the
-  -- latter's equivalence relation is decidable, then the former's
-  -- equivalence relation is also decidable.
-
-  via-injection : Decidable _≈B_ → Decidable _≈A_
-  via-injection dec x y =
-    map′ injective cong (dec (to x) (to y))
-
+map : A ⇔ B → Dec A → Dec B
+map A⇔B = map′ to from
+  where open Equivalence A⇔B
+
+-- If there is an injection from one setoid to another, and the
+-- latter's equivalence relation is decidable, then the former's
+-- equivalence relation is also decidable.
+via-injection : {S : Setoid a ℓ₁} {T : Setoid b ℓ₂}
+                (inj : Injection S T) (open Injection inj) →
+                Decidable Eq₂._≈_ → Decidable Eq₁._≈_
+via-injection inj _≟_ x y = map′ injective cong (to x ≟ to y)
+  where open Injection inj
+  
 ------------------------------------------------------------------------
 -- A lemma relating True and Dec
 
-True-↔ : (dec : Dec P) → Irrelevant P → True dec ↔ P
-True-↔ (true  because  [p]) irr = mk↔ₛ′ (λ _ → invert [p]) _ (irr (invert [p])) cong′
-True-↔ (false because ofⁿ ¬p) _ = mk↔ₛ′ (λ ()) (invert (ofⁿ ¬p)) (⊥-elim ∘ ¬p) λ ()
+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) λ ()
 
 ------------------------------------------------------------------------
 -- Result of decidability
 
-isYes≗does : (P? : Dec P) → isYes P? ≡ does P?
+isYes≗does : (a? : Dec A) → isYes a? ≡ does a?
 isYes≗does (true  because _) = refl
 isYes≗does (false because _) = refl
 
-dec-true : (p? : Dec P) → P → does p? ≡ true
-dec-true (true  because   _ ) p = refl
-dec-true (false because [¬p]) p = ⊥-elim (invert [¬p] p)
+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-false : (p? : Dec P) → ¬ P → does p? ≡ false
-dec-false (false because  _ ) ¬p = refl
-dec-false (true  because [p]) ¬p = ⊥-elim (¬p (invert [p]))
+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-yes : (p? : Dec P) → P → ∃ λ p′ → p? ≡ yes p′
-dec-yes p? p with dec-true p? p
-dec-yes (yes p′) p | refl = p′ , refl
+dec-yes : (a? : Dec A) → A → ∃ λ a → a? ≡ yes a
+dec-yes a? a with dec-true a? a
+dec-yes (yes a′) a | refl = a′ , refl
 
-dec-no : (p? : Dec P) (¬p : ¬ P) → p? ≡ no ¬p
-dec-no p? ¬p with dec-false p? ¬p
+dec-no : (a? : Dec A) (¬a : ¬ A) → a? ≡ no ¬a
+dec-no a? ¬a with dec-false a? ¬a
 dec-no (no _) _ | refl = refl
 
-dec-yes-irr : (p? : Dec P) → Irrelevant P → (p : P) → p? ≡ yes p
-dec-yes-irr p? irr p with dec-yes p? p
-... | p′ , eq rewrite irr p p′ = eq
+dec-yes-irr : (a? : Dec A) → Irrelevant A → (a : A) → a? ≡ yes a
+dec-yes-irr a? irr a with dec-yes a? a
+... | a′ , eq rewrite irr a a′ = eq
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 2d827519d7..166b1f264e 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -24,9 +24,8 @@ open import Relation.Nullary.Negation.Core
 
 private
   variable
-    p q : Level
-    P : Set p
-    Q : Set q
+    a b : Level
+    A B : Set a
 
 ------------------------------------------------------------------------
 -- Definition.
@@ -41,25 +40,38 @@ private
 
 infix 2 _because_
 
-record Dec {p} (P : Set p) : Set p where
+record Dec (A : Set a) : Set a where
   constructor _because_
   field
     does  : Bool
-    proof : Reflects P does
+    proof : Reflects A does
 
 open Dec public
 
-pattern yes p =  true because ofʸ  p
-pattern no ¬p = false because ofⁿ ¬p
+pattern yes a =  true because ofʸ  a
+pattern no ¬a = false because ofⁿ ¬a
+
+------------------------------------------------------------------------
+-- Flattening
+
+module _ {A : Set a} where
+
+  From-yes : Dec A → Set a
+  From-yes (true  because _) = A
+  From-yes (false because _) = Lift a ⊤
+
+  From-no : Dec A → Set a
+  From-no (false because _) = ¬ A
+  From-no (true  because _) = Lift a ⊤
 
 ------------------------------------------------------------------------
 -- Recompute
 
 -- Given an irrelevant proof of a decidable type, a proof can
 -- be recomputed and subsequently used in relevant contexts.
-recompute : ∀ {a} {A : Set a} → Dec A → .A → A
-recompute (yes x) _ = x
-recompute (no ¬p) x = ⊥-elim (¬p x)
+recompute : Dec A → .A → A
+recompute (yes a) _ = a
+recompute (no ¬a) a = ⊥-elim (¬a a)
 
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
@@ -67,42 +79,42 @@ recompute (no ¬p) x = ⊥-elim (¬p x)
 infixr 1 _⊎-dec_
 infixr 2 _×-dec_ _→-dec_
 
-¬? : Dec P → Dec (¬ P)
-does  (¬? p?) = not (does p?)
-proof (¬? p?) = ¬-reflects (proof p?)
+¬? : Dec A → Dec (¬ A)
+does  (¬? a?) = not (does a?)
+proof (¬? a?) = ¬-reflects (proof a?)
 
-_×-dec_ : Dec P → Dec Q → Dec (P × Q)
-does  (p? ×-dec q?) = does p? ∧ does q?
-proof (p? ×-dec q?) = proof p? ×-reflects proof q?
+_×-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?
 
-_⊎-dec_ : Dec P → Dec Q → Dec (P ⊎ Q)
-does  (p? ⊎-dec q?) = does p? ∨ does q?
-proof (p? ⊎-dec q?) = proof p? ⊎-reflects proof q?
+_⊎-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?
 
-_→-dec_ : Dec P → Dec Q → Dec (P → Q)
-does  (p? →-dec q?) = not (does p?) ∨ does q?
-proof (p? →-dec q?) = proof p? →-reflects proof q?
+_→-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?
 
 ------------------------------------------------------------------------
 -- Relationship with booleans
 
 -- `isYes` is a stricter version of `does`. The lack of computation
--- means that we can recover the proposition `P` from `isYes P?` by
+-- means that we can recover the proposition `P` from `isYes a?` by
 -- unification. This is useful when we are using the decision procedure
 -- for proof automation.
 
-isYes : Dec P → Bool
+isYes : Dec A → Bool
 isYes (true  because _) = true
 isYes (false because _) = false
 
-isNo : Dec P → Bool
+isNo : Dec A → Bool
 isNo = not ∘ isYes
 
-True : Dec P → Set
-True Q = T (isYes Q)
+True : Dec A → Set
+True = T ∘ isYes
 
-False : Dec P → Set
-False Q = T (isNo Q)
+False : Dec A → Set
+False = T ∘ isNo
 
 -- The traditional name for isYes is ⌊_⌋, indicating the stripping of evidence.
 ⌊_⌋ = isYes
@@ -111,77 +123,72 @@ False Q = T (isNo Q)
 -- Witnesses
 
 -- Gives a witness to the "truth".
-toWitness : {Q : Dec P} → True Q → P
-toWitness {Q = true  because [p]} _  = invert [p]
-toWitness {Q = false because  _ } ()
+toWitness : {a? : Dec A} → True a? → A
+toWitness {a? = true  because [a]} _  = invert [a]
+toWitness {a? = false because  _ } ()
 
 -- Establishes a "truth", given a witness.
-fromWitness : {Q : Dec P} → P → True Q
-fromWitness {Q = true  because   _ } = const _
-fromWitness {Q = false because [¬p]} = invert [¬p]
+fromWitness : {a? : Dec A} → A → True a?
+fromWitness {a? = true  because   _ } = const _
+fromWitness {a? = false because [¬a]} = invert [¬a]
 
 -- Variants for False.
-toWitnessFalse : {Q : Dec P} → False Q → ¬ P
-toWitnessFalse {Q = true  because   _ } ()
-toWitnessFalse {Q = false because [¬p]} _  = invert [¬p]
-
-fromWitnessFalse : {Q : Dec P} → ¬ P → False Q
-fromWitnessFalse {Q = true  because [p]} = flip _$_ (invert [p])
-fromWitnessFalse {Q = false because  _ } = const _
+toWitnessFalse : {a? : Dec A} → False a? → ¬ A
+toWitnessFalse {a? = true  because   _ } ()
+toWitnessFalse {a? = false because [¬a]} _  = invert [¬a]
 
-module _ {p} {P : Set p} where
+fromWitnessFalse : {a? : Dec A} → ¬ A → False a?
+fromWitnessFalse {a? = true  because [a]} = flip _$_ (invert [a])
+fromWitnessFalse {a? = false because  _ } = const _
 
 -- If a decision procedure returns "yes", then we can extract the
 -- proof using from-yes.
-
-  From-yes : Dec P → Set p
-  From-yes (true  because _) = P
-  From-yes (false because _) = Lift p ⊤
-
-  from-yes : (p : Dec P) → From-yes p
-  from-yes (true  because [p]) = invert [p]
-  from-yes (false because _ ) = _
+from-yes : (a? : Dec A) → From-yes a?
+from-yes (true  because [a]) = invert [a]
+from-yes (false because _ ) = _
 
 -- If a decision procedure returns "no", then we can extract the proof
 -- using from-no.
-
-  From-no : Dec P → Set p
-  From-no (false because _) = ¬ P
-  From-no (true  because _) = Lift p ⊤
-
-  from-no : (p : Dec P) → From-no p
-  from-no (false because [¬p]) = invert [¬p]
-  from-no (true  because   _ ) = _
+from-no : (a? : Dec A) → From-no a?
+from-no (false because [¬a]) = invert [¬a]
+from-no (true  because   _ ) = _
 
 ------------------------------------------------------------------------
 -- Maps
 
-map′ : (P → Q) → (Q → P) → Dec P → Dec Q
-does  (map′ P→Q Q→P p?)                   = does p?
-proof (map′ P→Q Q→P (true  because  [p])) = ofʸ (P→Q (invert [p]))
-proof (map′ P→Q Q→P (false because [¬p])) = ofⁿ (invert [¬p] ∘ Q→P)
+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)
 
 ------------------------------------------------------------------------
 -- Relationship with double-negation
 
 -- Decidable predicates are stable.
 
-decidable-stable : Dec P → Stable P
-decidable-stable (yes p) ¬¬p = p
-decidable-stable (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p)
+decidable-stable : Dec A → Stable A
+decidable-stable (yes a) ¬¬a = a
+decidable-stable (no ¬a) ¬¬a = ⊥-elim (¬¬a ¬a)
 
-¬-drop-Dec : Dec (¬ ¬ P) → Dec (¬ P)
-¬-drop-Dec ¬¬p? = map′ negated-stable contradiction (¬? ¬¬p?)
+¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A)
+¬-drop-Dec ¬¬a? = map′ negated-stable contradiction (¬? ¬¬a?)
 
 -- A double-negation-translated variant of excluded middle (or: every
 -- nullary relation is decidable in the double-negation monad).
 
-¬¬-excluded-middle : DoubleNegation (Dec P)
-¬¬-excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p)))
+¬¬-excluded-middle : DoubleNegation (Dec A)
+¬¬-excluded-middle ¬?a = ¬?a (no (λ a → ¬?a (yes a)))
 
-excluded-middle : DoubleNegation (Dec P)
-excluded-middle = ¬¬-excluded-middle
 
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+excluded-middle = ¬¬-excluded-middle
 {-# WARNING_ON_USAGE excluded-middle
 "Warning: excluded-middle was deprecated in v2.0.
 Please use ¬¬-excluded-middle instead."
diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda
index 59e96f3429..4d9ee54208 100644
--- a/src/Relation/Nullary/Negation.agda
+++ b/src/Relation/Nullary/Negation.agda
@@ -16,15 +16,13 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
 open import Function.Base using (flip; _∘_; const; _∘′_)
 open import Level using (Level)
 open import Relation.Nullary.Decidable.Core using (Dec; yes; no; ¬¬-excluded-middle)
-open import Relation.Unary using (Universal)
+open import Relation.Unary using (Universal; Pred)
 
 private
   variable
-    a p q r w : Level
-    A : Set a
-    P : Set p
-    Q : Set q
-    R : Set r
+    a b c d p w : Level
+    A B C D : Set a
+    P : Pred A p
     Whatever : Set w
 
 ------------------------------------------------------------------------
@@ -35,22 +33,20 @@ open import Relation.Nullary.Negation.Core public
 ------------------------------------------------------------------------
 -- Quantifier juggling
 
-module _ {P : A → Set p} where
+∃⟶¬∀¬ : ∃ P → ¬ (∀ x → ¬ P x)
+∃⟶¬∀¬ = flip uncurry
 
-  ∃⟶¬∀¬ : ∃ P → ¬ (∀ x → ¬ P x)
-  ∃⟶¬∀¬ = flip uncurry
+∀⟶¬∃¬ : (∀ x → P x) → ¬ ∃ λ x → ¬ P x
+∀⟶¬∃¬ ∀xPx (x , ¬Px) = ¬Px (∀xPx x)
 
-  ∀⟶¬∃¬ : (∀ x → P x) → ¬ ∃ λ x → ¬ P x
-  ∀⟶¬∃¬ ∀xPx (x , ¬Px) = ¬Px (∀xPx x)
+¬∃⟶∀¬ : ¬ ∃ (λ x → P x) → ∀ x → ¬ P x
+¬∃⟶∀¬ = curry
 
-  ¬∃⟶∀¬ : ¬ ∃ (λ x → P x) → ∀ x → ¬ P x
-  ¬∃⟶∀¬ = curry
+∀¬⟶¬∃ : (∀ x → ¬ P x) → ¬ ∃ (λ x → P x)
+∀¬⟶¬∃ = uncurry
 
-  ∀¬⟶¬∃ : (∀ x → ¬ P x) → ¬ ∃ (λ x → P x)
-  ∀¬⟶¬∃ = uncurry
-
-  ∃¬⟶¬∀ : ∃ (λ x → ¬ P x) → ¬ (∀ x → P x)
-  ∃¬⟶¬∀ = flip ∀⟶¬∃¬
+∃¬⟶¬∀ : ∃ (λ x → ¬ P x) → ¬ (∀ x → P x)
+∃¬⟶¬∀ = flip ∀⟶¬∃¬
 
 ------------------------------------------------------------------------
 -- Double Negation
@@ -58,15 +54,14 @@ module _ {P : A → Set p} where
 -- Double-negation is a monad (if we assume that all elements of ¬ ¬ P
 -- are equal).
 
-¬¬-Monad : RawMonad {p} DoubleNegation
+¬¬-Monad : RawMonad {a} DoubleNegation
 ¬¬-Monad = mkRawMonad
   DoubleNegation
   contradiction
   (λ x f → negated-stable (¬¬-map f x))
 
-¬¬-push : {Q : P → Set q} →
-          DoubleNegation Π[ Q ] → Π[ DoubleNegation ∘ Q ]
-¬¬-push ¬¬P⟶Q P ¬Q = ¬¬P⟶Q (λ P⟶Q → ¬Q (P⟶Q P))
+¬¬-push : DoubleNegation Π[ P ] → Π[ DoubleNegation ∘ P ]
+¬¬-push ¬¬∀P a ¬Pa = ¬¬∀P (λ ∀P → ¬Pa (∀P a))
 
 -- If Whatever is instantiated with ¬ ¬ something, then this function
 -- is call with current continuation in the double-negation monad, or,
@@ -77,26 +72,25 @@ module _ {P : A → Set p} where
 -- that case this function can be used (with Whatever instantiated to
 -- ⊥).
 
-call/cc : ((P → Whatever) → DoubleNegation P) → DoubleNegation P
-call/cc hyp ¬p = hyp (λ p → ⊥-elim (¬p p)) ¬p
+call/cc : ((A → Whatever) → DoubleNegation A) → DoubleNegation A
+call/cc hyp ¬a = hyp (λ a → ⊥-elim (¬a a)) ¬a
 
 -- The "independence of premise" rule, in the double-negation monad.
--- It is assumed that the index set (Q) is inhabited.
+-- It is assumed that the index set (A) is inhabited.
 
-independence-of-premise : {R : Q → Set r} →
-                          Q → (P → Σ Q R) → DoubleNegation (Σ[ x ∈ Q ] (P → R x))
-independence-of-premise {P = P} q f = ¬¬-map helper ¬¬-excluded-middle
+independence-of-premise : A → (B → Σ A P) → DoubleNegation (Σ[ x ∈ A ] (B → P x))
+independence-of-premise {A = A} {B = B} {P = P} q f = ¬¬-map helper ¬¬-excluded-middle
   where
-  helper : Dec P → _
+  helper : Dec B → Σ[ x ∈ A ] (B → P x)
   helper (yes p) = Prod.map₂ const (f p)
   helper (no ¬p) = (q , ⊥-elim ∘′ ¬p)
 
 -- The independence of premise rule for binary sums.
 
-independence-of-premise-⊎ : (P → Q ⊎ R) → DoubleNegation ((P → Q) ⊎ (P → R))
-independence-of-premise-⊎ {P = P} f = ¬¬-map helper ¬¬-excluded-middle
+independence-of-premise-⊎ : (A → B ⊎ C) → DoubleNegation ((A → B) ⊎ (A → C))
+independence-of-premise-⊎ {A = A} {B = B} {C = C} f = ¬¬-map helper ¬¬-excluded-middle
   where
-  helper : Dec P → _
+  helper : Dec A → (A → B) ⊎ (A → C)
   helper (yes p) = Sum.map const const (f p)
   helper (no ¬p) = inj₁ (⊥-elim ∘′ ¬p)
 
@@ -106,12 +100,10 @@ private
   -- independence-of-premise (for simplicity it is assumed that Q and
   -- R have the same type here):
 
-  corollary : {Q R : Set q} →
-              (P → Q ⊎ R) → DoubleNegation ((P → Q) ⊎ (P → R))
-  corollary {P = P} {Q} {R} f =
-    ¬¬-map helper (independence-of-premise
-                     true ([ _,_ true , _,_ false ] ∘′ f))
+  corollary : {B C : Set b} → (A → B ⊎ C) → DoubleNegation ((A → B) ⊎ (A → C))
+  corollary {A = A} {B = B} {C = C} f =
+    ¬¬-map helper (independence-of-premise true ([ _,_ true , _,_ false ] ∘′ f))
     where
-    helper : ∃ (λ b → P → if b then Q else R) → (P → Q) ⊎ (P → R)
+    helper : ∃ (λ b → A → if b then B else C) → (A → B) ⊎ (A → C)
     helper (true  , f) = inj₁ f
     helper (false , f) = inj₂ f
diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 5c4efaf4fb..cbe9ac6da9 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -9,9 +9,7 @@
 module Relation.Nullary.Negation.Core where
 
 open import Data.Bool.Base using (not)
-open import Data.Empty using (⊥)
-open import Data.Empty.Irrelevant using (⊥-elim)
-open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Sum.Base using (_⊎_; [_,_]; inj₁; inj₂)
 open import Function.Base using (flip; _$_; _∘_; const)
 open import Level
@@ -19,9 +17,7 @@ open import Level
 private
   variable
     a p q w : Level
-    A : Set a
-    P : Set p
-    Q : Set q
+    A B C : Set a
     Whatever : Set w
 
 ------------------------------------------------------------------------
@@ -29,48 +25,51 @@ private
 
 infix 3 ¬_
 ¬_ : Set a → Set a
-¬ P = P → ⊥
+¬ A = A → ⊥
+
+------------------------------------------------------------------------
+-- Stability.
 
 -- Double-negation
-DoubleNegation : Set p → Set p
-DoubleNegation P = ¬ ¬ P
+DoubleNegation : Set a → Set a
+DoubleNegation A = ¬ ¬ A
 
 -- Stability under double-negation.
-Stable : Set p → Set p
-Stable P = ¬ ¬ P → P
+Stable : Set a → Set a
+Stable A = ¬ ¬ A → A
 
 ------------------------------------------------------------------------
--- Relationship to product and sum
+-- Relationship to sum
 
 infixr 1 _¬-⊎_
-_¬-⊎_ : ¬ P → ¬ Q → ¬ (P ⊎ Q)
+_¬-⊎_ : ¬ A → ¬ B → ¬ (A ⊎ B)
 _¬-⊎_ = [_,_]
 
 ------------------------------------------------------------------------
 -- Uses of negation
 
-contradiction : P → ¬ P → Whatever
-contradiction p ¬p = ⊥-elim (¬p p)
-
-contradiction₂ : P ⊎ Q → ¬ P → ¬ Q → Whatever
-contradiction₂ (inj₁ p) ¬p ¬q = contradiction p ¬p
-contradiction₂ (inj₂ q) ¬p ¬q = contradiction q ¬q
+contradiction : A → ¬ A → Whatever
+contradiction a ¬a = ⊥-elim (¬a a)
 
-contraposition : (P → Q) → ¬ Q → ¬ P
-contraposition f ¬q p = contradiction (f p) ¬q
+contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
+contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a
+contradiction₂ (inj₂ b) ¬a ¬b = contradiction b ¬b
 
--- Note also the following use of flip:
-private
-  note : (P → ¬ Q) → Q → ¬ P
-  note = flip
+contraposition : (A → B) → ¬ B → ¬ A
+contraposition f ¬b a = contradiction (f a) ¬b
 
 -- Everything is stable in the double-negation monad.
-stable : ¬ ¬ Stable P
-stable ¬[¬¬p→p] = ¬[¬¬p→p] (λ ¬¬p → ⊥-elim (¬¬p (¬[¬¬p→p] ∘ const)))
+stable : ¬ ¬ Stable A
+stable ¬[¬¬a→a] = ¬[¬¬a→a] (λ ¬¬a → ⊥-elim (¬¬a (¬[¬¬a→a] ∘ const)))
 
 -- Negated predicates are stable.
-negated-stable : Stable (¬ P)
-negated-stable ¬¬¬P P = ¬¬¬P (λ ¬P → ¬P P)
+negated-stable : Stable (¬ A)
+negated-stable ¬¬¬a a = ¬¬¬a (_$ a)
 
-¬¬-map : (P → Q) → ¬ ¬ P → ¬ ¬ Q
+¬¬-map : (A → B) → ¬ ¬ A → ¬ ¬ B
 ¬¬-map f = contraposition (contraposition f)
+
+-- Note also the following use of flip:
+private
+  note : (A → ¬ B) → B → ¬ A
+  note = flip
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 66556e8ae6..4f97bd8709 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -21,18 +21,18 @@ open import Relation.Nullary.Negation.Core
 
 private
   variable
-    p q : Level
-    P Q : Set p
+    a : Level
+    A B : Set a
 
 ------------------------------------------------------------------------
 -- `Reflects` idiom.
 
--- The truth value of P is reflected by a boolean value.
--- `Reflects P b` is equivalent to `if b then P else ¬ P`.
+-- The truth value of A is reflected by a boolean value.
+-- `Reflects A b` is equivalent to `if b then A else ¬ A`.
 
-data Reflects {p} (P : Set p) : Bool → Set p where
-  ofʸ : ( p :   P) → Reflects P true
-  ofⁿ : (¬p : ¬ P) → Reflects P false
+data Reflects (A : Set a) : Bool → Set a where
+  ofʸ : ( a :   A) → Reflects A true
+  ofⁿ : (¬a : ¬ A) → Reflects A false
 
 ------------------------------------------------------------------------
 -- Constructors and destructors
@@ -41,57 +41,57 @@ data Reflects {p} (P : Set p) : Bool → Set p where
 -- 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 `P` or the proof of `¬ P`.
+-- the proof of `A` or the proof of `¬ A`.
 
-of : ∀ {b} → if b then P else ¬ P → Reflects P b
-of {b = false} ¬p = ofⁿ ¬p
-of {b = true }  p = ofʸ p
+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 P b → if b then P else ¬ P
-invert (ofʸ  p) = p
-invert (ofⁿ ¬p) = ¬p
+invert : ∀ {b} → Reflects A b → if b then A else ¬ A
+invert (ofʸ  a) = a
+invert (ofⁿ ¬a) = ¬a
 
 ------------------------------------------------------------------------
 -- Interaction with negation, product, sums etc.
 
--- If we can decide P, then we can decide its negation.
-¬-reflects : ∀ {b} → Reflects P b → Reflects (¬ P) (not b)
-¬-reflects (ofʸ  p) = ofⁿ (_$ p)
-¬-reflects (ofⁿ ¬p) = ofʸ ¬p
+-- 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
 
--- If we can decide P and Q then we can decide their product
+-- If we can decide A and Q then we can decide their product
 infixr 2 _×-reflects_
-_×-reflects_ : ∀ {a b} → Reflects P a → Reflects Q b →
-               Reflects (P × Q) (a ∧ b)
-ofʸ  p ×-reflects ofʸ  q = ofʸ (p , q)
-ofʸ  p ×-reflects ofⁿ ¬q = ofⁿ (¬q ∘ proj₂)
-ofⁿ ¬p ×-reflects _      = ofⁿ (¬p ∘ proj₁)
+_×-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₁)
 
 
 infixr 1 _⊎-reflects_
-_⊎-reflects_ : ∀ {a b} → Reflects P a → Reflects Q b →
-               Reflects (P ⊎ Q) (a ∨ b)
-ofʸ  p ⊎-reflects      _ = ofʸ (inj₁ p)
-ofⁿ ¬p ⊎-reflects ofʸ  q = ofʸ (inj₂ q)
-ofⁿ ¬p ⊎-reflects ofⁿ ¬q = ofⁿ (¬p ¬-⊎ ¬q)
+_⊎-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)
 
 infixr 2 _→-reflects_
-_→-reflects_ : ∀ {a b} → Reflects P a → Reflects Q b →
-                Reflects (P → Q) (not a ∨ b)
-ofʸ  p →-reflects ofʸ  q = ofʸ (const q)
-ofʸ  p →-reflects ofⁿ ¬q = ofⁿ (¬q ∘ (_$ p))
-ofⁿ ¬p →-reflects _      = ofʸ (⊥-elim ∘ ¬p)
+_→-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)
 
 ------------------------------------------------------------------------
 -- Other lemmas
 
-fromEquivalence : ∀ {b} → (T b → P) → (P → T b) → Reflects P b
+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 : ∀ {b b′} → Reflects P b → Reflects P b′ → b ≡ b′
-det (ofʸ  p) (ofʸ  p′) = refl
-det (ofʸ  p) (ofⁿ ¬p′) = ⊥-elim (¬p′ p)
-det (ofⁿ ¬p) (ofʸ  p′) = ⊥-elim (¬p p′)
-det (ofⁿ ¬p) (ofⁿ ¬p′) = refl
+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

From 7ecdfc89038b422459c64ab9269bcf093089d043 Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Thu, 28 Sep 2023 11:18:27 +0900
Subject: [PATCH 2/3] Minor fixes

---
 src/Codata/Musical/Colist.agda      | 4 ++--
 src/Data/Nat/InfinitelyOften.agda   | 3 ++-
 src/Relation/Nullary/Decidable.agda | 2 +-
 src/Relation/Nullary/Universe.agda  | 2 +-
 4 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/Codata/Musical/Colist.agda b/src/Codata/Musical/Colist.agda
index 21dde992bc..2f59082e22 100644
--- a/src/Codata/Musical/Colist.agda
+++ b/src/Codata/Musical/Colist.agda
@@ -67,8 +67,8 @@ take (suc n) []       = Vec≤.[]
 take (suc n) (x ∷ xs) = x Vec≤.∷ take n (♭ xs)
 
 
-module ¬¬Monad {p} where
-  open RawMonad (¬¬-Monad {p}) public
+module ¬¬Monad {a} where
+  open RawMonad (¬¬-Monad {a}) public
 open ¬¬Monad  -- we don't want the RawMonad content to be opened publicly
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Nat/InfinitelyOften.agda b/src/Data/Nat/InfinitelyOften.agda
index f85ceb196a..6d86336193 100644
--- a/src/Data/Nat/InfinitelyOften.agda
+++ b/src/Data/Nat/InfinitelyOften.agda
@@ -20,7 +20,8 @@ open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Negation using (¬¬-Monad; call/cc)
 open import Relation.Unary using (Pred; _∪_; _⊆_)
-open RawMonad (¬¬-Monad {p = 0ℓ})
+
+open RawMonad (¬¬-Monad {a = 0ℓ})
 
 private
   variable
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index f0882f3098..cb5f72b6e0 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -46,7 +46,7 @@ via-injection : {S : Setoid a ℓ₁} {T : Setoid b ℓ₂}
                 Decidable Eq₂._≈_ → Decidable Eq₁._≈_
 via-injection inj _≟_ x y = map′ injective cong (to x ≟ to y)
   where open Injection inj
-  
+
 ------------------------------------------------------------------------
 -- A lemma relating True and Dec
 
diff --git a/src/Relation/Nullary/Universe.agda b/src/Relation/Nullary/Universe.agda
index 8d72845f07..34e087ec69 100644
--- a/src/Relation/Nullary/Universe.agda
+++ b/src/Relation/Nullary/Universe.agda
@@ -116,7 +116,7 @@ sequence {AF = AF} A extract-⊥ sequence-⇒ = helper
 -- Some lemmas about double negation.
 
 private
-  open module M {p} = RawMonad (¬¬-Monad {p = p})
+  open module M {a} = RawMonad (¬¬-Monad {a = a})
 
 ¬¬-pull : ∀ {p} (F : PropF p) {P} →
           ⟦ F ⟧ (¬ ¬ P) → ¬ ¬ ⟦ F ⟧ P

From eed9ce32dcbb31fec4e821b7e6816bffaffe92a0 Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Fri, 29 Sep 2023 08:58:44 +0900
Subject: [PATCH 3/3] Added excluded-middle to CHANGELOG

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 35a0991cac..98048ac580 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1555,6 +1555,11 @@ Deprecated names
   invPreorder   ↦ converse-preorder
   ```
 
+* In `Relation.Nullary.Decidable.Core`:
+  ```
+  excluded-middle  ↦  ¬¬-excluded-middle
+  ```
+
 ### Renamed Data.Erased to Data.Irrelevant
 
 * This fixes the fact we had picked the wrong name originally. The erased modality