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] 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
+