From c5bf817edeacd8e11685dd04369440d43b97bbbf Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 17 Nov 2023 09:03:11 +0000
Subject: [PATCH 1/3] deprecating `isPropositional`

---
 CHANGELOG.md                                  |  5 ++++
 .../Binary/PropositionalEquality.agda         | 25 ++++++++++++++-----
 2 files changed, 24 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ddc3b262fc..51966c2176 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1727,6 +1727,11 @@ Deprecated names
   invPreorder   ↦ converse-preorder
   ```
 
+* In `Relation.Binary.PropositionalEquality`:
+  ```agda
+  isPropositional ↦ Relation.Nullary.Irrelevant
+  ```
+
 * In `Relation.Unary.Consequences`:
   ```agda
   dec⟶recomputable  ↦  dec⇒recomputable
diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda
index 6ff59d8c28..cddbc34c25 100644
--- a/src/Relation/Binary/PropositionalEquality.agda
+++ b/src/Relation/Binary/PropositionalEquality.agda
@@ -60,12 +60,6 @@ _≗_ {A = A} {B = B} = Setoid._≈_ (A →-setoid B)
          Dependent.Func (setoid A) (Trivial.indexedSetoid B)
 →-to-⟶ = :→-to-Π
 
-------------------------------------------------------------------------
--- Propositionality
-
-isPropositional : Set a → Set a
-isPropositional A = (a b : A) → a ≡ b
-
 ------------------------------------------------------------------------
 -- More complex rearrangement lemmas
 
@@ -125,3 +119,22 @@ record Reveal_·_is_ {A : Set a} {B : A → Set b}
 inspect : ∀ {A : Set a} {B : A → Set b}
           (f : (x : A) → B x) (x : A) → Reveal f · x is f x
 inspect f x = [ refl ]
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+isPropositional : Set a → Set a
+isPropositional A = (a b : A) → a ≡ b
+
+{-# WARNING_ON_USAGE isPropositional
+"Warning: isPropositional was deprecated in v2.0.
+Please use Relation.Nullary.Irrelevant instead. "
+#-}
+
+

From e50e171b508652f4976080d2dc7f5bcfd957e47a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 17 Nov 2023 10:05:31 +0000
Subject: [PATCH 2/3] tighten `import`s

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

diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda
index cddbc34c25..9b74a4acd6 100644
--- a/src/Relation/Binary/PropositionalEquality.agda
+++ b/src/Relation/Binary/PropositionalEquality.agda
@@ -8,14 +8,12 @@
 
 module Relation.Binary.PropositionalEquality where
 
-import Axiom.Extensionality.Propositional as Ext
 open import Axiom.UniquenessOfIdentityProofs
 open import Function.Base using (id; _∘_)
 import Function.Dependent.Bundles as Dependent
 open import Function.Indexed.Relation.Binary.Equality using (≡-setoid)
 open import Level using (Level; _⊔_)
-open import Data.Product.Base using (∃)
-
+open import Relation.Nullary using (Irrelevant)
 open import Relation.Nullary.Decidable using (yes; no; dec-yes-irr; dec-no)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions using (DecidableEquality)
@@ -130,7 +128,7 @@ inspect f x = [ refl ]
 -- Version 2.0
 
 isPropositional : Set a → Set a
-isPropositional A = (a b : A) → a ≡ b
+isPropositional = Irrelevant
 
 {-# WARNING_ON_USAGE isPropositional
 "Warning: isPropositional was deprecated in v2.0.

From f2ee05f4dcacc262899e1d52f983fd2d18755ad9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 17 Nov 2023 13:58:04 +0000
Subject: [PATCH 3/3] bumped Agda version number in comment

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

diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda
index 9b74a4acd6..7ba3825e31 100644
--- a/src/Relation/Binary/PropositionalEquality.agda
+++ b/src/Relation/Binary/PropositionalEquality.agda
@@ -105,7 +105,7 @@ module _ (_≟_ : DecidableEquality A) {x y : A} where
 -- See README.Inspect for an explanation of how/why to use this.
 
 -- Normally (but not always) the new `with ... in` syntax described at
--- https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality
+-- https://agda.readthedocs.io/en/v2.6.4/language/with-abstraction.html#with-abstraction-equality
 -- can be used instead."
 
 record Reveal_·_is_ {A : Set a} {B : A → Set b}