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

CHANGELOG.md

@@ -41,6 +41,9 @@ 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 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`.
@@ -109,13 +112,20 @@ 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     ↦   ⊤?
   ⊥-dec     ↦   ⊥?
   _×-dec_  ↦   _×?_
   _⊎-dec_  ↦   _⊎?_
   _→-dec_  ↦   _→?_
+  ```
 
 * In `Relation.Nullary.Negation`:
   ```agda

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/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!)
 

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

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,32 +1,44 @@
 ------------------------------------------------------------------------
 -- 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
 
-open import Function.Core public
+import Function.Core
   using (Morphism)
 
 ------------------------------------------------------------------------
 -- Basic definitions
 
-Homomorphic₂ : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → Set _
-Homomorphic₂ _∼₁_ _∼₂_ ⟦_⟧ = ∀ {x y} → x ∼₁ y → ⟦ x ⟧ ∼₂ ⟦ y ⟧
+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."
+#-}

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 _≈₁_ _≈₂_ ⟦_⟧