diff --git a/CHANGELOG.md b/CHANGELOG.md
index 11b10834de..50d27f893a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,13 @@ The library has been tested using Agda 2.8.0.
 Highlights
 ----------
 
+### Deprecated `Relation.Binary.PropositionalEquality.inspect`, in favour
+    of `with ... in ...` syntax (issue #1580; PRs #1630, #1930, #2934)
+
+* In `Relation.Binary.PropositionalEquality`, the record type `Reveal_·_is_`
+  and its principal mode of use, `inspect`, have been deprecated in favour of
+  the new `with ... in ...` syntax. See the documentation of [with-abstraction equality](https://agda.readthedocs.io/en/v2.9.0/language/with-abstraction.html#with-abstraction-equality).
+
 Bug-fixes
 ---------
 
@@ -400,6 +407,17 @@ Additions to existing modules
             Antisym P Q R → Antisym (Pointwise P {n}) (Pointwise Q) (Pointwise R)
   ```
 
+* In `Relation.Binary.PropositionalEquality`, replacing `Reveal`/`inspect`:
+  ```agda
+  module Graph {A : Set a} {B : A → Set b} (f : (x : A) → B x) (x : A) where
+
+    record View (y : B x) : Set (a ⊔ b) where
+      field fx≡y : f x ≡ y
+
+    view : View (f x)
+    view = record { fx≡y = refl }
+  ```
+
 * In `Relation.Nullary.Negation.Core`
   ```agda
   ¬¬-η           : A → ¬ ¬ A
diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda
index 283623cc96..44df77e791 100644
--- a/src/Relation/Binary/PropositionalEquality.agda
+++ b/src/Relation/Binary/PropositionalEquality.agda
@@ -92,26 +92,15 @@ module _ (_≟_ : DecidableEquality A) {x y : A} where
 
 
 ------------------------------------------------------------------------
--- Inspect
+-- The graph view of a function
 
--- Inspect can be used when you want to pattern match on the result r
--- of some expression e, and you also need to "remember" that r ≡ e.
+module Graph {A : Set a} {B : A → Set b} (f : (x : A) → B x) (x : A) where
 
--- See README.Inspect for an explanation of how/why to use this.
+  record View (y : B x) : Set (a ⊔ b) where
+    field fx≡y : f x ≡ y
 
--- Normally (but not always) the new `with ... in` syntax described at
--- 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}
-                    (f : (x : A) → B x) (x : A) (y : B x) :
-                    Set (a ⊔ b) where
-  constructor [_]
-  field eq : f x ≡ y
-
-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 ]
+  view : View (f x)
+  view = record { fx≡y = refl }
 
 
 ------------------------------------------------------------------------
@@ -130,3 +119,30 @@ isPropositional = Irrelevant
 Please use Relation.Nullary.Irrelevant instead. "
 #-}
 
+-- Version 2.4
+
+module _ {A : Set a} {B : A → Set b} where
+
+  open Graph
+
+  Reveal_·_is_ : (f : (x : A) → B x) (x : A) (y : B x) → Set (a ⊔ b)
+  Reveal f · x is y = View f x y
+
+  inspect : (f : (x : A) → B x) (x : A) → Reveal f · x is f x
+  inspect = view
+
+  pattern [_] eq = record { fx≡y = eq }
+  {-# WARNING_ON_USAGE [_]
+  "Warning: [_] was deprecated in v2.4.
+  Please use the `with ... in eq` syntax instead. "
+  #-}
+  {-# WARNING_ON_USAGE inspect
+  "Warning: inspect was deprecated in v2.4.
+  Please use the `with ... in eq` syntax described at
+  https://agda.readthedocs.io/en/v2.9.0/language/with-abstraction.html#with-abstraction-equality instead."
+  #-}
+  {-# WARNING_ON_USAGE Reveal_·_is_
+  "Warning: Reveal_·_is_ was deprecated in v2.4.
+  Please use the `with ... in eq` syntax described at
+  https://agda.readthedocs.io/en/v2.9.0/language/with-abstraction.html#with-abstraction-equality instead."
+  #-}