fix: remove module ι, and better description in CHANGELOG

Author: jamesmckinna

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

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
-