diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3eb803ac39..6aa775ab01 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`, 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
new file mode 100644
index 0000000000..036cf9b918
--- /dev/null
+++ b/src/Relation/Binary/Morphism/Construct/On.agda
@@ -0,0 +1,32 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Construct monomorphism from a relation and a function via `_on_`
+------------------------------------------------------------------------
+
+{-# 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
+  }