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..7ba3825e31 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)
@@ -60,12 +58,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
 
@@ -113,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}
@@ -125,3 +117,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 = Irrelevant
+
+{-# WARNING_ON_USAGE isPropositional
+"Warning: isPropositional was deprecated in v2.0.
+Please use Relation.Nullary.Irrelevant instead. "
+#-}
+
+