From fafc400685cdeee0071c1d3141fcdee974f4dfe8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 12 Nov 2025 15:53:44 +0000
Subject: [PATCH 1/3] add: `Relation.Binary.Morphism.Construct.On`

---
 CHANGELOG.md                                  |  4 +++
 .../Binary/Morphism/Construct/On.agda         | 35 +++++++++++++++++++
 2 files changed, 39 insertions(+)
 create mode 100644 src/Relation/Binary/Morphism/Construct/On.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3eb803ac39..9b6e3e36df 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -105,6 +105,10 @@ New modules
   Data.List.NonEmpty.Membership.Setoid
   ```
 
+* `Relation.Binary.Morphism.Construct.On`: given a relation `_∼_` on `B`,
+  and a function `f : A → B`, lift to various `IsRelHomomorphism`s between
+  `_∼_ on f` and `_∼_`.
+
 Additions to existing modules
 -----------------------------
 
diff --git a/src/Relation/Binary/Morphism/Construct/On.agda b/src/Relation/Binary/Morphism/Construct/On.agda
new file mode 100644
index 0000000000..85d0c1bf80
--- /dev/null
+++ b/src/Relation/Binary/Morphism/Construct/On.agda
@@ -0,0 +1,35 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Construct IsRelHomomorphisms from a relation and a function
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+
+module Relation.Binary.Morphism.Construct.On
+  {a b ℓ} {A : Set a} {B : Set b} (_∼_ : Rel B ℓ) (f : A → B)
+  where
+
+open import Function.Base using (id; _on_)
+open import Relation.Binary.Morphism.Structures
+  using (IsRelHomomorphism; IsRelMonomorphism)
+
+------------------------------------------------------------------------
+-- Definition
+
+_≈_ : Rel A _
+_≈_ = _∼_ on f
+
+isRelHomomorphism : IsRelHomomorphism _≈_ _∼_ f
+isRelHomomorphism = record { cong = id }
+
+isRelMonomorphism : IsRelMonomorphism _≈_ _∼_ f
+isRelMonomorphism = record
+  { isHomomorphism = isRelHomomorphism
+  ; injective = id
+  }
+
+module ι = IsRelMonomorphism isRelMonomorphism
+

From 10f720565328767179219a47617230e5645d9f93 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 18 Nov 2025 05:57:38 +0000
Subject: [PATCH 2/3] fix: top-level descriptive comment

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

diff --git a/src/Relation/Binary/Morphism/Construct/On.agda b/src/Relation/Binary/Morphism/Construct/On.agda
index 85d0c1bf80..b23fc5d723 100644
--- a/src/Relation/Binary/Morphism/Construct/On.agda
+++ b/src/Relation/Binary/Morphism/Construct/On.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Construct IsRelHomomorphisms from a relation and a function
+-- Construct Morphisms from a relation and a function via `_on_`
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}

From 3dc4b35b5e5d2c5ff9c1860e4573c63234904036 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 20 Nov 2025 03:56:53 +0000
Subject: [PATCH 3/3] =?UTF-8?q?fix:=20remove=20`module=20=CE=B9`,=20and=20?=
 =?UTF-8?q?better=20description=20in=20`CHANGELOG`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                                   | 4 ++--
 src/Relation/Binary/Morphism/Construct/On.agda | 5 +----
 2 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9b6e3e36df..6aa775ab01 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -106,8 +106,8 @@ New modules
   ```
 
 * `Relation.Binary.Morphism.Construct.On`: given a relation `_∼_` on `B`,
-  and a function `f : A → B`, lift to various `IsRelHomomorphism`s between
-  `_∼_ on f` and `_∼_`.
+  and a function `f : A → B`, construct the canonical `IsRelMonomorphism`
+  between `_∼_ on f` and `_∼_`, witnessed by `f` itself.
 
 Additions to existing modules
 -----------------------------
diff --git a/src/Relation/Binary/Morphism/Construct/On.agda b/src/Relation/Binary/Morphism/Construct/On.agda
index b23fc5d723..036cf9b918 100644
--- a/src/Relation/Binary/Morphism/Construct/On.agda
+++ b/src/Relation/Binary/Morphism/Construct/On.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Construct Morphisms from a relation and a function via `_on_`
+-- Construct monomorphism from a relation and a function via `_on_`
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -30,6 +30,3 @@ isRelMonomorphism = record
   { isHomomorphism = isRelHomomorphism
   ; injective = id
   }
-
-module ι = IsRelMonomorphism isRelMonomorphism
-