From 5813fe6df711f319d1cc85ac17ad8440c20682df Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 6 Feb 2026 10:19:35 +0000
Subject: [PATCH 1/3] [ deprecate ]
 `Relation/Binary.PropositionalEquality.inspect`

---
 .../Binary/PropositionalEquality.agda         | 43 +++++++++----------
 1 file changed, 20 insertions(+), 23 deletions(-)

diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda
index 283623cc96..7c226dd054 100644
--- a/src/Relation/Binary/PropositionalEquality.agda
+++ b/src/Relation/Binary/PropositionalEquality.agda
@@ -91,29 +91,6 @@ module _ (_≟_ : DecidableEquality A) {x y : A} where
   ≢-≟-identity = dec-no (x ≟ y)
 
 
-------------------------------------------------------------------------
--- Inspect
-
--- 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.
-
--- 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.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 ]
-
-
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------
@@ -130,3 +107,23 @@ isPropositional = Irrelevant
 Please use Relation.Nullary.Irrelevant instead. "
 #-}
 
+-- Version 2.4
+
+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 ]
+
+{-# WARNING_ON_USAGE Reveal_·_is_
+"Warning: Reveal_·_is_ was deprecated in v2.4.
+Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.9.0/language/with-abstraction.html#with-abstraction-equality instead."
+#-}
+{-# WARNING_ON_USAGE inspect
+"Warning: inspect was deprecated in v2.4.
+Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.9.0/language/with-abstraction.html#with-abstraction-equality instead."
+#-}

From e6e91d3f130c5111e7bee6a43200b1db7ceaed60 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 6 Feb 2026 10:31:53 +0000
Subject: [PATCH 2/3] add : `CHANGELOG`

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 11b10834de..5fac4248c1 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
 ---------
 

From b23264ea0af8aac9ba574f300e478421493f1575 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 8 Feb 2026 10:57:15 +0000
Subject: [PATCH 3/3] refactor: introduce `Graph` module

---
 CHANGELOG.md                                  | 11 ++++
 .../Binary/PropositionalEquality.agda         | 55 +++++++++++++------
 2 files changed, 48 insertions(+), 18 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5fac4248c1..50d27f893a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -407,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 7c226dd054..44df77e791 100644
--- a/src/Relation/Binary/PropositionalEquality.agda
+++ b/src/Relation/Binary/PropositionalEquality.agda
@@ -91,6 +91,18 @@ module _ (_≟_ : DecidableEquality A) {x y : A} where
   ≢-≟-identity = dec-no (x ≟ y)
 
 
+------------------------------------------------------------------------
+-- The graph view of a function
+
+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 }
+
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------
@@ -109,21 +121,28 @@ Please use Relation.Nullary.Irrelevant instead. "
 
 -- Version 2.4
 
-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 ]
-
-{-# WARNING_ON_USAGE Reveal_·_is_
-"Warning: Reveal_·_is_ was deprecated in v2.4.
-Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.9.0/language/with-abstraction.html#with-abstraction-equality instead."
-#-}
-{-# WARNING_ON_USAGE inspect
-"Warning: inspect was deprecated in v2.4.
-Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.9.0/language/with-abstraction.html#with-abstraction-equality instead."
-#-}
+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."
+  #-}