[ add ] `Relation.Binary.Morphism.Construct.On`

[jamesmckinna]

Given a Setoid/IsEquivalence bundle/structure on type B, and h : A → B, to construct

• _≈_ : Rel A _,
  by = B._≈_ on h
• isRelHomomorphism : IsRelHomomorphism _≈_ B._≈_ h,
  by isRelHomomorphism = record { cong = id }
• isRelMonomorphism : IsRelMonomorphism _≈_ B._≈_ h,
  by isRelMonomorphism = record { isRelHomomorphism = isRelHomomorphism; injective = id }

And... that's just about it!

UPDATED: After discussion (incl. concerning what module path/name this should live under) on the associated PR #2872 , I realise that this is the germ (but only as far as constructing the mono) of the Kernel of h construction (and the Isomorphism Theorems attaching to that), so a sensible followup would be to develop Algebra.Morphism.Construct.Kernel (again: path/name?) on a sound footing, with this buried somewhere at the bottom of such a development... cf. #1899 etc.