[ refactor ] make Relation.Binary.Morphism.Definitions obsolete

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

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

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

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} {ℓ}
 

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)
 

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

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

src/Relation/Binary/Morphism/Structures.agda

@@ -1,35 +1,34 @@
 ------------------------------------------------------------------------
 -- 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
 ------------------------------------------------------------------------
 
 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 _≈₁_ _≈₂_ ⟦_⟧