diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2d61629e75..31bd9be59a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -41,6 +41,10 @@ Minor improvements
   an alias, and should be backwards compatible, but does improve the behaviour
   of the termination checker for some `Vector`-defined operations.
 
+* `Relation.Binary.Morphism.Definitions` is no longer imported by any module,
+  but retained as a compatibility stub for external users, and for uniformity
+  with the design of existing hierarchies.
+
 * The type of `Relation.Nullary.Negation.Core.contradiction-irr` has been further
   weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is
   safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`.
@@ -116,6 +120,7 @@ Deprecated names
   _×-dec_  ↦   _×?_
   _⊎-dec_  ↦   _⊎?_
   _→-dec_  ↦   _→?_
+  ```
 
 * In `Relation.Nullary.Negation`:
   ```agda
diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda
index 5c6a8063ae..dbe10b50da 100644
--- a/src/Algebra/Morphism/Bundles.agda
+++ b/src/Algebra/Morphism/Bundles.agda
@@ -16,8 +16,6 @@ open import Algebra.Bundles.Raw using
   ; RawRingWithoutOne; RawRing)
 open import Algebra.Morphism.Structures
 open import Level using (Level; suc; _⊔_)
---open import Relation.Binary.Morphism using (IsRelHomomorphism)
---open import Relation.Binary.Morphism.Bundles using (SetoidHomomorphism)
 
 private
   variable
diff --git a/src/Algebra/Morphism/Construct/Initial.agda b/src/Algebra/Morphism/Construct/Initial.agda
index 8e86bcea48..5bd3258442 100644
--- a/src/Algebra/Morphism/Construct/Initial.agda
+++ b/src/Algebra/Morphism/Construct/Initial.agda
@@ -17,8 +17,7 @@ module Algebra.Morphism.Construct.Initial {c ℓ : Level} where
 open import Algebra.Bundles.Raw using (RawMagma)
 open import Algebra.Morphism.Structures
   using (IsMagmaHomomorphism; IsMagmaMonomorphism)
-open import Function.Definitions using (Injective)
-import Relation.Binary.Morphism.Definitions as Rel
+open import Function.Definitions using (Congruent; Injective)
 open import Relation.Binary.Core using (Rel)
 
 open import Algebra.Construct.Initial {c} {ℓ}
@@ -27,7 +26,7 @@ private
   variable
     a m ℓm : Level
     A : Set a
-    ≈ : Rel A ℓm
+
 
 ------------------------------------------------------------------------
 -- The unique morphism
@@ -38,25 +37,29 @@ zero ()
 ------------------------------------------------------------------------
 -- Basic properties
 
-cong : (≈ : Rel A ℓm) → Rel.Homomorphic₂ ℤero.Carrier A ℤero._≈_ ≈ zero
-cong _ {x = ()}
+module _ (≈ : Rel A ℓm) where
+
+  cong : Congruent ℤero._≈_ ≈ zero
+  cong {x = ()}
 
-injective : (≈ : Rel A ℓm) → Injective ℤero._≈_ ≈ zero
-injective _ {x = ()}
+  injective : Injective ℤero._≈_ ≈ zero
+  injective {x = ()}
 
 ------------------------------------------------------------------------
 -- Morphism structures
 
-isMagmaHomomorphism : (M : RawMagma m ℓm) →
-                      IsMagmaHomomorphism rawMagma M zero
-isMagmaHomomorphism M = record
-  { isRelHomomorphism = record { cong = cong (RawMagma._≈_ M) }
-  ; homo = λ()
-  }
-
-isMagmaMonomorphism : (M : RawMagma m ℓm) →
-                      IsMagmaMonomorphism rawMagma M zero
-isMagmaMonomorphism M = record
-  { isMagmaHomomorphism = isMagmaHomomorphism M
-  ; injective = injective (RawMagma._≈_ M)
-  }
+module _ (M : RawMagma m ℓm) where
+
+  open RawMagma M using (_≈_)
+
+  isMagmaHomomorphism : IsMagmaHomomorphism rawMagma M zero
+  isMagmaHomomorphism = record
+    { isRelHomomorphism = record { cong = cong _≈_ }
+    ; homo = λ()
+    }
+
+  isMagmaMonomorphism : IsMagmaMonomorphism rawMagma M zero
+  isMagmaMonomorphism = record
+    { isMagmaHomomorphism = isMagmaHomomorphism
+    ; injective = injective _≈_
+    }
diff --git a/src/Algebra/Morphism/Construct/Terminal.agda b/src/Algebra/Morphism/Construct/Terminal.agda
index 0b366708b5..00ef216bed 100644
--- a/src/Algebra/Morphism/Construct/Terminal.agda
+++ b/src/Algebra/Morphism/Construct/Terminal.agda
@@ -23,8 +23,6 @@ open import Algebra.Morphism.Structures
         ; IsRingHomomorphism)
 open import Data.Product.Base using (_,_)
 open import Function.Definitions using (StrictlySurjective)
-import Relation.Binary.Morphism.Definitions as Rel
-open import Relation.Binary.Morphism.Structures using (IsRelHomomorphism)
 
 open import Algebra.Construct.Terminal {c} {ℓ}
 
diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda
index af7e025fff..51707874fd 100644
--- a/src/Algebra/Morphism/Structures.agda
+++ b/src/Algebra/Morphism/Structures.agda
@@ -13,7 +13,6 @@ open import Algebra.Bundles
 import Algebra.Morphism.Definitions as MorphismDefinitions
 open import Level using (Level; _⊔_)
 open import Function.Definitions using (Injective; Surjective)
-open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Morphism.Structures
   using (IsRelHomomorphism; IsRelMonomorphism; IsRelIsomorphism)
 
diff --git a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
index 616247b696..40f1da67f6 100644
--- a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
@@ -24,19 +24,19 @@ import Data.List.Relation.Unary.AllPairs.Properties as AllPairs
 open import Data.Fin.Base using (Fin)
 open import Data.Nat.Base using (_<_)
 open import Function.Base using (_∘_; id)
-open import Function.Definitions using (Congruent)
+open import Function.Definitions using (Congruent; Injective)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Nullary.Negation.Core using (¬_; contraposition)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary.Negation using (¬_)
-open import Relation.Nullary.Negation using (contraposition)
 
 private
   variable
     a b c p ℓ ℓ₁ ℓ₂ ℓ₃ : Level
 
+
 ------------------------------------------------------------------------
 -- Introduction (⁺) and elimination (⁻) rules for list operations
 ------------------------------------------------------------------------
@@ -47,7 +47,7 @@ module _ (S : Setoid a ℓ₁) (R : Setoid b ℓ₂) where
   open Setoid S renaming (_≈_ to _≈₁_)
   open Setoid R renaming (_≈_ to _≈₂_)
 
-  map⁺ : ∀ {f} → (∀ {x y} → f x ≈₂ f y → x ≈₁ y) →
+  map⁺ : ∀ {f} → Injective _≈₁_ _≈₂_ f →
          ∀ {xs} → Unique S xs → Unique R (map f xs)
   map⁺ inj xs! = AllPairs.map⁺ (AllPairs.map (contraposition inj) xs!)
 
diff --git a/src/Function/Structures/Biased.agda b/src/Function/Structures/Biased.agda
index 8e570f2618..fee983ece7 100644
--- a/src/Function/Structures/Biased.agda
+++ b/src/Function/Structures/Biased.agda
@@ -19,7 +19,8 @@ module Function.Structures.Biased {a b ℓ₁ ℓ₂}
 
 open import Data.Product.Base as Product using (∃; _×_; _,_)
 open import Function.Base using (_∘_; id)
-open import Function.Definitions using(StrictlySurjective; StrictlyInverseˡ; StrictlyInverseʳ; Congruent)
+open import Function.Definitions
+  using (StrictlySurjective; StrictlyInverseˡ; StrictlyInverseʳ; Congruent)
 open import Function.Consequences.Setoid
   using (strictlySurjective⇒surjective; strictlyInverseˡ⇒inverseˡ
         ; strictlyInverseʳ⇒inverseʳ)
diff --git a/src/Relation/Binary/Morphism/Bundles.agda b/src/Relation/Binary/Morphism/Bundles.agda
index 29e400e886..6ee2596360 100644
--- a/src/Relation/Binary/Morphism/Bundles.agda
+++ b/src/Relation/Binary/Morphism/Bundles.agda
@@ -9,17 +9,18 @@
 module Relation.Binary.Morphism.Bundles where
 
 open import Level using (Level; _⊔_)
-open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.Bundles using (Setoid; Preorder; Poset)
+open import Relation.Binary.Consequences using (mono⇒cong)
+open import Relation.Binary.Definitions using (Monotonic₁)
 open import Relation.Binary.Morphism.Structures
   using (IsRelHomomorphism; IsRelMonomorphism; IsRelIsomorphism
         ; IsOrderHomomorphism; IsOrderMonomorphism; IsOrderIsomorphism)
-open import Relation.Binary.Consequences using (mono⇒cong)
 
 private
   variable
     ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level
 
+
 ------------------------------------------------------------------------
 -- Setoids
 ------------------------------------------------------------------------
@@ -96,7 +97,7 @@ module _ (P : Poset ℓ₁ ℓ₂ ℓ₃) (Q : Poset ℓ₄ ℓ₅ ℓ₆) where
 
   -- Smart constructor that automatically constructs the congruence
   -- proof from the monotonicity proof
-  mkPosetHomo : ∀ f → f Preserves P._≤_ ⟶ Q._≤_ → PosetHomomorphism
+  mkPosetHomo : ∀ f → Monotonic₁ P._≤_ Q._≤_ f → PosetHomomorphism
   mkPosetHomo f mono = record
     { ⟦_⟧ = f
     ; isOrderHomomorphism = record
diff --git a/src/Relation/Binary/Morphism/Definitions.agda b/src/Relation/Binary/Morphism/Definitions.agda
index 4e687e4868..1c20f6a8a3 100644
--- a/src/Relation/Binary/Morphism/Definitions.agda
+++ b/src/Relation/Binary/Morphism/Definitions.agda
@@ -1,24 +1,17 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Basic definitions for morphisms between algebraic structures
+-- Issue #2318/#2875:
+-- this is now a stub module, retained solely for compatibility
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core
-
 module Relation.Binary.Morphism.Definitions
   {a} (A : Set a)     -- The domain of the morphism
   {b} (B : Set b)     -- The codomain of the morphism
   where
 
-open import Level using (Level)
-
-private
-  variable
-    ℓ₁ ℓ₂ : Level
-
 ------------------------------------------------------------------------
 -- Morphism definition in Function.Core
 
@@ -28,5 +21,6 @@ open import Function.Core public
 ------------------------------------------------------------------------
 -- Basic definitions
 
-Homomorphic₂ : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → Set _
-Homomorphic₂ _∼₁_ _∼₂_ ⟦_⟧ = ∀ {x y} → x ∼₁ y → ⟦ x ⟧ ∼₂ ⟦ y ⟧
+open import Function.Definitions public
+  using ()
+  renaming (Congruent to Homomorphic₂)
diff --git a/src/Relation/Binary/Morphism/Structures.agda b/src/Relation/Binary/Morphism/Structures.agda
index f7372afd58..aad5fe048a 100644
--- a/src/Relation/Binary/Morphism/Structures.agda
+++ b/src/Relation/Binary/Morphism/Structures.agda
@@ -1,27 +1,26 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Order morphisms
+-- Relational morphisms, incl. in particular, order morphisms
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core using (Rel)
-
 module Relation.Binary.Morphism.Structures
   {a b} {A : Set a} {B : Set b}
   where
 
 open import Data.Product.Base using (_,_)
-open import Function.Definitions using (Injective; Surjective; Bijective)
+open import Function.Definitions
+  using (Congruent; Injective; Surjective; Bijective)
 open import Level using (Level; _⊔_)
-
-open import Relation.Binary.Morphism.Definitions A B
+open import Relation.Binary.Core using (Rel)
 
 private
   variable
     ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
 
+
 ------------------------------------------------------------------------
 -- Relations
 ------------------------------------------------------------------------
@@ -29,7 +28,7 @@ private
 record IsRelHomomorphism (_∼₁_ : Rel A ℓ₁) (_∼₂_ : Rel B ℓ₂)
                          (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   field
-    cong : Homomorphic₂ _∼₁_ _∼₂_ ⟦_⟧
+    cong : Congruent _∼₁_ _∼₂_ ⟦_⟧
 
 
 record IsRelMonomorphism (_∼₁_ : Rel A ℓ₁) (_∼₂_ : Rel B ℓ₂)
@@ -62,8 +61,8 @@ record IsOrderHomomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
                            (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
                            where
   field
-    cong  : Homomorphic₂ _≈₁_ _≈₂_ ⟦_⟧
-    mono  : Homomorphic₂ _≲₁_ _≲₂_ ⟦_⟧
+    cong  : Congruent _≈₁_ _≈₂_ ⟦_⟧
+    mono  : Congruent _≲₁_ _≲₂_ ⟦_⟧
 
   module Eq where
     isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧