[ add ] Relation.Binary.Morphism.Construct.On (#2872)

* add: `Relation.Binary.Morphism.Construct.On`

* fix: top-level descriptive comment

* fix: remove `module ι`, and better description in `CHANGELOG`

Author: jamesmckinna

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

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