From 025cb2d48aff0bd32378a1204917675361471a4a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 24 Jan 2026 18:54:38 +0000
Subject: [PATCH 1/4] [ refactor ] make `elation.Binary.Morphism.Definitions`
 obsolete

---
 CHANGELOG.md                                  |  3 ++
 src/Algebra/Morphism/Bundles.agda             |  2 -
 src/Algebra/Morphism/Construct/Initial.agda   | 43 ++++++++++---------
 src/Algebra/Morphism/Construct/Terminal.agda  |  2 -
 src/Algebra/Morphism/Structures.agda          |  1 -
 src/Relation/Binary/Morphism/Bundles.agda     |  7 +--
 src/Relation/Binary/Morphism/Definitions.agda | 15 ++-----
 src/Relation/Binary/Morphism/Structures.agda  | 17 ++++----
 8 files changed, 42 insertions(+), 48 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 88e250b35b..11388d7590 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -29,6 +29,9 @@ Minor improvements
   properties (and their proofs). In particular, `truncate-irrelevant` is now
   deprecated, because definitionally trivial.
 
+* `Relation.Binary.Morphism.Definitions` is no longer imported by any module,
+  but retained as a stub for compatibility with external users.
+
 * 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`.
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/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..fb40f65a1e 100644
--- a/src/Relation/Binary/Morphism/Definitions.agda
+++ b/src/Relation/Binary/Morphism/Definitions.agda
@@ -1,24 +1,16 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Basic definitions for morphisms between algebraic structures
+-- Issue #2875: this is 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 +20,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 _≈₁_ _≈₂_ ⟦_⟧

From 38634be825e544af2f2a6bac7986baff9630c37e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 4 Mar 2026 15:47:02 +0000
Subject: [PATCH 2/4] deprecate: middle ground, only deprecate names in this
 release; module in v3.0

---
 CHANGELOG.md                                  |  8 ++++++++
 src/Relation/Binary/Morphism/Definitions.agda | 18 ++++++++++++++----
 2 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 996f93f219..c8288d921b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -101,6 +101,12 @@ Deprecated names
   truncate-irrelevant  ↦  Relation.Binary.PropositionalEquality.Core.refl
   ```
 
+* In `Relation.Binary.Morphism.Definitions`:
+  ```agda
+  Morphism A B    ↦   A → B
+  Homomorphic₂    ↦   Function.Definitions.Congruent
+  ```
+
 * In `Relation.Nullary.Decidable.Core`:
   ```agda
   ⊤-dec     ↦   ⊤?
@@ -108,6 +114,8 @@ Deprecated names
   _×-dec_  ↦   _×?_
   _⊎-dec_  ↦   _⊎?_
   _→-dec_  ↦   _→?_
+  ```
+
 
 * In `Relation.Nullary.Negation`:
   ```agda
diff --git a/src/Relation/Binary/Morphism/Definitions.agda b/src/Relation/Binary/Morphism/Definitions.agda
index fb40f65a1e..869aee940c 100644
--- a/src/Relation/Binary/Morphism/Definitions.agda
+++ b/src/Relation/Binary/Morphism/Definitions.agda
@@ -12,14 +12,24 @@ module Relation.Binary.Morphism.Definitions
   where
 
 ------------------------------------------------------------------------
--- Morphism definition in Function.Core
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
 
 open import Function.Core public
   using (Morphism)
-
-------------------------------------------------------------------------
--- Basic definitions
+{-# WARNING_ON_USAGE Morphism
+"Warning: Morphism was deprecated in v2.4.
+Please use the standard function notation (e.g. A → B) instead."
+#-}
 
 open import Function.Definitions public
   using ()
   renaming (Congruent to Homomorphic₂)
+{-# WARNING_ON_USAGE Homomorphic₂
+"Warning: Homomorphic₂ was deprecated in v2.4.
+Please use Function.Definitions.Congruent instead."
+#-}

From 337b722ba5b03c0450f51d1761d037ed5b05433b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 4 Mar 2026 17:20:29 +0000
Subject: [PATCH 3/4] refactor: not sure what fixed the problem, but hey?

---
 .../Unary/Unique/Setoid/Properties.agda       |  8 ++++----
 src/Function/Structures/Biased.agda           |  3 ++-
 src/Relation/Binary/Morphism/Definitions.agda | 19 ++++++++++++++-----
 3 files changed, 20 insertions(+), 10 deletions(-)

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/Definitions.agda b/src/Relation/Binary/Morphism/Definitions.agda
index 869aee940c..20cd9e4905 100644
--- a/src/Relation/Binary/Morphism/Definitions.agda
+++ b/src/Relation/Binary/Morphism/Definitions.agda
@@ -11,6 +11,18 @@ module Relation.Binary.Morphism.Definitions
   {b} (B : Set b)     -- The codomain of the morphism
   where
 
+------------------------------------------------------------------------
+-- Morphism definition in Function.Core
+
+import Function.Core
+  using (Morphism)
+
+------------------------------------------------------------------------
+-- Basic definitions
+
+import Function.Definitions
+  using (Congruent)
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------
@@ -19,16 +31,13 @@ module Relation.Binary.Morphism.Definitions
 
 -- Version 2.4
 
-open import Function.Core public
-  using (Morphism)
+Morphism = Function.Core.Morphism
 {-# WARNING_ON_USAGE Morphism
 "Warning: Morphism was deprecated in v2.4.
 Please use the standard function notation (e.g. A → B) instead."
 #-}
 
-open import Function.Definitions public
-  using ()
-  renaming (Congruent to Homomorphic₂)
+Homomorphic₂ = Function.Definitions.Congruent
 {-# WARNING_ON_USAGE Homomorphic₂
 "Warning: Homomorphic₂ was deprecated in v2.4.
 Please use Function.Definitions.Congruent instead."

From b7961a4ca6db047d630a6a9addf38bacfb174b16 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 8 Apr 2026 16:48:51 +0100
Subject: [PATCH 4/4] revert: deprecations, in favour of `using`/`renaming`
 public re-exports

---
 CHANGELOG.md                                  |  9 ++----
 src/Relation/Binary/Morphism/Definitions.agda | 30 ++++---------------
 2 files changed, 8 insertions(+), 31 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 47bdd0370d..31bd9be59a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -42,7 +42,8 @@ Minor improvements
   of the termination checker for some `Vector`-defined operations.
 
 * `Relation.Binary.Morphism.Definitions` is no longer imported by any module,
-  but retained as a stub for compatibility with external users.
+  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
@@ -112,12 +113,6 @@ Deprecated names
   decidable     ↦   _∪?_
   ```
 
-* In `Relation.Binary.Morphism.Definitions`:
-  ```agda
-  Morphism A B    ↦   A → B
-  Homomorphic₂    ↦   Function.Definitions.Congruent
-  ```
-
 * In `Relation.Nullary.Decidable.Core`:
   ```agda
   ⊤-dec     ↦   ⊤?
diff --git a/src/Relation/Binary/Morphism/Definitions.agda b/src/Relation/Binary/Morphism/Definitions.agda
index 20cd9e4905..1c20f6a8a3 100644
--- a/src/Relation/Binary/Morphism/Definitions.agda
+++ b/src/Relation/Binary/Morphism/Definitions.agda
@@ -1,7 +1,8 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Issue #2875: this is a stub module, retained solely for compatibility
+-- Issue #2318/#2875:
+-- this is now a stub module, retained solely for compatibility
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -14,31 +15,12 @@ module Relation.Binary.Morphism.Definitions
 ------------------------------------------------------------------------
 -- Morphism definition in Function.Core
 
-import Function.Core
+open import Function.Core public
   using (Morphism)
 
 ------------------------------------------------------------------------
 -- Basic definitions
 
-import Function.Definitions
-  using (Congruent)
-
-------------------------------------------------------------------------
--- DEPRECATED NAMES
-------------------------------------------------------------------------
--- Please use the new names as continuing support for the old names is
--- not guaranteed.
-
--- Version 2.4
-
-Morphism = Function.Core.Morphism
-{-# WARNING_ON_USAGE Morphism
-"Warning: Morphism was deprecated in v2.4.
-Please use the standard function notation (e.g. A → B) instead."
-#-}
-
-Homomorphic₂ = Function.Definitions.Congruent
-{-# WARNING_ON_USAGE Homomorphic₂
-"Warning: Homomorphic₂ was deprecated in v2.4.
-Please use Function.Definitions.Congruent instead."
-#-}
+open import Function.Definitions public
+  using ()
+  renaming (Congruent to Homomorphic₂)