Merge branch 'agda:master' into centres-bis

Author: jamesmckinna

CHANGELOG.md

@@ -53,6 +53,11 @@ Deprecated names
   interchange  ↦   medial
   ```
 
+* In `Algebra.Properties.Monoid`:
+  ```agda
+  ε-comm  ↦   ε-central
+  ```
+
 * In `Data.Fin.Properties`:
   ```agda
   ¬∀⟶∃¬-smallest  ↦   ¬∀⇒∃¬-smallest
@@ -109,6 +114,10 @@ New modules
   Data.List.NonEmpty.Membership.Setoid
   ```
 
+* `Relation.Binary.Morphism.Construct.On`: given a relation `_∼_` on `B`,
+  and a function `f : A → B`, construct the canonical `IsRelMonomorphism`
+  between `_∼_ on f` and `_∼_`, witnessed by `f` itself.
+
 Additions to existing modules
 -----------------------------
 

src/Algebra/Properties/Monoid.agda

@@ -8,26 +8,37 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles using (Monoid)
-open import Function using (_∘_)
 
 module Algebra.Properties.Monoid {o ℓ} (M : Monoid o ℓ) where
 
+open import Function using (_∘_)
+
 open Monoid M
-  using (Carrier; _∙_; _≈_; setoid; isMagma; semigroup; ε; sym; identityˡ
-  ; identityʳ ; ∙-cong; refl; assoc; ∙-congˡ; ∙-congʳ; trans)
+  using (Carrier; _∙_; ε; _≈_; refl; sym; trans; setoid
+        ; ∙-cong; ∙-congˡ; ∙-congʳ; isMagma
+        ; assoc; semigroup; identity; identityˡ; identityʳ)
+
+open import Algebra.Consequences.Setoid setoid using (identity⇒central)
+open import Algebra.Definitions _≈_ using (Central)
 open import Relation.Binary.Reasoning.Setoid setoid
 
+private
+  variable
+    a b c d : Carrier
+
+------------------------------------------------------------------------
+-- Re-export `Semigroup` properties
+
 open import Algebra.Properties.Semigroup semigroup public
 
-private
-    variable
-        a b c d : Carrier
+------------------------------------------------------------------------
+-- Properties of identity
 
 ε-unique : ∀ a → (∀ b → b ∙ a ≈ b) → a ≈ ε
 ε-unique a b∙a≈b = trans (sym (identityˡ a)) (b∙a≈b ε)
 
-ε-comm : ∀ a → a ∙ ε ≈ ε ∙ a
-ε-comm a = trans (identityʳ a) (sym (identityˡ a))
+ε-central : Central _∙_ ε
+ε-central = identity⇒central {_∙_ = _∙_} identity
 
 module _ (a≈ε : a ≈ ε) where
   elimʳ : ∀ b → b ∙ a ≈ b
@@ -65,3 +76,17 @@ module _ (inv : a ∙ c ≈ ε) where
   insertᶜ : ∀ b d → b ∙ d ≈ (b ∙ a) ∙ (c ∙ d)
   insertᶜ = λ b d → sym (cancelᶜ b d)
 
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+ε-comm = ε-central
+{-# WARNING_ON_USAGE ε-comm
+"Warning: ε-comm was deprecated in v2.4.
+Please use ε-central instead."
+#-}

src/Relation/Binary/Morphism/Construct/On.agda

@@ -0,0 +1,32 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Construct monomorphism from a relation and a function via `_on_`
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+
+module Relation.Binary.Morphism.Construct.On
+  {a b ℓ} {A : Set a} {B : Set b} (_∼_ : Rel B ℓ) (f : A → B)
+  where
+
+open import Function.Base using (id; _on_)
+open import Relation.Binary.Morphism.Structures
+  using (IsRelHomomorphism; IsRelMonomorphism)
+
+------------------------------------------------------------------------
+-- Definition
+
+_≈_ : Rel A _
+_≈_ = _∼_ on f
+
+isRelHomomorphism : IsRelHomomorphism _≈_ _∼_ f
+isRelHomomorphism = record { cong = id }
+
+isRelMonomorphism : IsRelMonomorphism _≈_ _∼_ f
+isRelMonomorphism = record
+  { isHomomorphism = isRelHomomorphism
+  ; injective = id
+  }