From 6619f114346e86ead3cf62b1170ab23d31056b48 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Tue, 2 Apr 2024 21:28:09 -0400
Subject: [PATCH 01/19] port over two modules

---
 src/Algebra/Morphism/Structures.agda         |  8 ++
 src/Function/Endomorphism/Propositional.agda | 35 ++++----
 src/Function/Endomorphism/Setoid.agda        | 84 ++++++++++++--------
 3 files changed, 80 insertions(+), 47 deletions(-)

diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda
index e73fa7e9e6..3dad55ac87 100644
--- a/src/Algebra/Morphism/Structures.agda
+++ b/src/Algebra/Morphism/Structures.agda
@@ -68,6 +68,14 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher
       ; surjective     = surjective
       }
 
+  IsSemigroupHomomorphism : (⟦_⟧ : A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  IsSemigroupHomomorphism = IsMagmaHomomorphism
+
+  IsSemigroupMonomorphism : (⟦_⟧ : A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  IsSemigroupMonomorphism = IsMagmaMonomorphism
+
+  IsSemigroupIsomorphism : (⟦_⟧ : A → B) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
+  IsSemigroupIsomorphism = IsMagmaIsomorphism
 
 ------------------------------------------------------------------------
 -- Morphisms over monoid-like structures
diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda
index c8dd685328..c6995bd6fd 100644
--- a/src/Function/Endomorphism/Propositional.agda
+++ b/src/Function/Endomorphism/Propositional.agda
@@ -5,21 +5,19 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-
--- Disabled to prevent warnings from deprecated names
-{-# OPTIONS --warn=noUserWarning #-}
-
 module Function.Endomorphism.Propositional {a} (A : Set a) where
 
 open import Algebra
-open import Algebra.Morphism; open Definitions
+open import Algebra.Structures
+open import Algebra.Morphism
+open Definitions
 
-open import Data.Nat.Base using (ℕ; zero; suc; _+_)
+open import Data.Nat.Base using (ℕ; _+_; zero; suc; +-rawMagma; +-0-rawMonoid)
 open import Data.Nat.Properties using (+-0-monoid; +-semigroup)
 open import Data.Product.Base using (_,_)
 
 open import Function.Base using (id; _∘′_; _∋_)
-open import Function.Equality using (_⟨$⟩_)
+open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
 open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
 import Relation.Binary.PropositionalEquality.Properties as ≡
@@ -37,7 +35,7 @@ fromSetoidEndo = _⟨$⟩_
 
 toSetoidEndo : Endo → Setoid.Endo
 toSetoidEndo f = record
-  { _⟨$⟩_ = f
+  { to = f
   ; cong  = cong f
   }
 
@@ -84,17 +82,24 @@ f ^ suc n = f ∘′ (f ^ n)
 ∘-id-monoid : Monoid _ _
 ∘-id-monoid = record { isMonoid = ∘-id-isMonoid }
 
+private
+  ∘-rawMagma : RawMagma a a
+  ∘-rawMagma = Semigroup.rawMagma ∘-semigroup
+
+  ∘-id-rawMonoid : RawMonoid a a
+  ∘-id-rawMonoid = Monoid.rawMonoid ∘-id-monoid
+
 ------------------------------------------------------------------------
 -- Homomorphism
 
-^-isSemigroupMorphism : ∀ f → IsSemigroupMorphism +-semigroup ∘-semigroup (f ^_)
+^-isSemigroupMorphism : ∀ f → IsSemigroupHomomorphism +-rawMagma ∘-rawMagma (f ^_)
 ^-isSemigroupMorphism f = record
-  { ⟦⟧-cong = cong (f ^_)
-  ; ∙-homo  = ^-homo f
+  { isRelHomomorphism = record { cong = cong (f ^_) }
+  ; homo = ^-homo f
   }
-
-^-isMonoidMorphism : ∀ f → IsMonoidMorphism +-0-monoid ∘-id-monoid (f ^_)
+  
+^-isMonoidMorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
 ^-isMonoidMorphism f = record
-  { sm-homo = ^-isSemigroupMorphism f
-  ; ε-homo  = refl
+  { isMagmaHomomorphism = ^-isSemigroupMorphism f
+  ; ε-homo = refl
   }
diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda
index a715ef5262..be4fa80816 100644
--- a/src/Function/Endomorphism/Setoid.agda
+++ b/src/Function/Endomorphism/Setoid.agda
@@ -6,48 +6,55 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
--- Disabled to prevent warnings from deprecated names
-{-# OPTIONS --warn=noUserWarning #-}
-
-open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.Bundles using (Setoid)
 
 module Function.Endomorphism.Setoid {c e} (S : Setoid c e) where
 
 open import Agda.Builtin.Equality
 
-open import Algebra
-open import Algebra.Structures
-open import Algebra.Morphism; open Definitions
-open import Function.Equality using (setoid; _⟶_; id; _∘_; cong)
-open import Data.Nat.Base using (ℕ; _+_); open ℕ
-open import Data.Nat.Properties
+open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
+open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
+open import Algebra.Morphism
+  using (module Definitions; IsSemigroupHomomorphism; IsMonoidHomomorphism)
+open Definitions using (Homomorphic₂)
+open import Data.Nat.Base using (ℕ; _+_; +-rawMagma; +-0-rawMonoid)
+open ℕ
+open import Data.Nat.Properties using (+-semigroup; +-identityʳ)
 open import Data.Product.Base using (_,_)
-
-import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial as Trivial
+open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
+open import Function.Construct.Identity using () renaming (function to identity)
+open import Function.Construct.Composition using () renaming (function to _∘_)
+open import Function.Relation.Binary.Setoid.Equality as Eq using (_⇨_)
+open import Level using (Level; _⊔_)
+open import Relation.Binary.Core using (_Preserves_⟶_)
 
 private
-  module E = Setoid (setoid S (Trivial.indexedSetoid S))
+  module E = Setoid (S ⇨ S)
   open E hiding (refl)
-
+  open Func using (cong)
 ------------------------------------------------------------------------
 -- Basic type and functions
 
 Endo : Set _
-Endo = S ⟶ S
+Endo = S ⟶ₛ S
 
 infixr 8 _^_
 
+private
+  id : Endo
+  id = identity S
+  
 _^_ : Endo → ℕ → Endo
 f ^ zero  = id
 f ^ suc n = f ∘ (f ^ n)
 
 ^-cong₂ : ∀ f → (f ^_) Preserves _≡_ ⟶ _≈_
-^-cong₂ f {n} refl = cong (f ^ n)
+^-cong₂ f {n} refl = cong (f ^ n) (Setoid.refl S)
 
 ^-homo : ∀ f → Homomorphic₂ ℕ Endo _≈_ (f ^_) _+_ _∘_
-^-homo f zero    n x≈y = cong (f ^ n) x≈y
-^-homo f (suc m) n x≈y = cong f (^-homo f m n x≈y)
+^-homo f zero    n           = Setoid.refl S
+^-homo f (suc m) zero    = ^-cong₂ f (+-identityʳ m)
+^-homo f (suc m) (suc n) = ^-homo f m (suc n)
 
 ------------------------------------------------------------------------
 -- Structures
@@ -55,41 +62,54 @@ f ^ suc n = f ∘ (f ^ n)
 ∘-isMagma : IsMagma _≈_ _∘_
 ∘-isMagma = record
   { isEquivalence = isEquivalence
-  ; ∙-cong        = λ g f x → g (f x)
+  ; ∙-cong        = λ {_} {_} {_} {v} x≈y u≈v → S.trans u≈v (cong v x≈y) 
   }
+  where
+    module S = Setoid S
 
-∘-magma : Magma _ _
+∘-magma : Magma (c ⊔ e) (c ⊔ e)
 ∘-magma = record { isMagma = ∘-isMagma }
 
 ∘-isSemigroup : IsSemigroup _≈_ _∘_
 ∘-isSemigroup = record
   { isMagma = ∘-isMagma
-  ; assoc   = λ h g f x≈y → cong h (cong g (cong f x≈y))
+  ; assoc   = λ h g f {s} → Setoid.refl S
   }
 
-∘-semigroup : Semigroup _ _
+∘-semigroup : Semigroup (c ⊔ e) (c ⊔ e)
 ∘-semigroup = record { isSemigroup = ∘-isSemigroup }
 
 ∘-id-isMonoid : IsMonoid _≈_ _∘_ id
 ∘-id-isMonoid = record
   { isSemigroup = ∘-isSemigroup
-  ; identity    = cong , cong
+  ; identity    = (λ f → Setoid.refl S) , (λ _ → Setoid.refl S)
   }
 
-∘-id-monoid : Monoid _ _
+∘-id-monoid : Monoid (c ⊔ e) (c ⊔ e)
 ∘-id-monoid = record { isMonoid = ∘-id-isMonoid }
 
+private
+  ∘-rawMagma : RawMagma (c ⊔ e) (c ⊔ e)
+  ∘-rawMagma = Semigroup.rawMagma ∘-semigroup
+
+  ∘-id-rawMonoid : RawMonoid (c ⊔ e) (c ⊔ e)
+  ∘-id-rawMonoid = Monoid.rawMonoid ∘-id-monoid
+  
 ------------------------------------------------------------------------
 -- Homomorphism
 
-^-isSemigroupMorphism : ∀ f → IsSemigroupMorphism +-semigroup ∘-semigroup (f ^_)
-^-isSemigroupMorphism f = record
-  { ⟦⟧-cong = ^-cong₂ f
-  ; ∙-homo  = ^-homo f
+^-isSemigroupHomomorphism : ∀ f → IsSemigroupHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isSemigroupHomomorphism f = record
+  { isRelHomomorphism = record { cong = ^-cong₂ f }
+  ; homo = ^-homo f
   }
 
-^-isMonoidMorphism : ∀ f → IsMonoidMorphism +-0-monoid ∘-id-monoid (f ^_)
-^-isMonoidMorphism f = record
-  { sm-homo = ^-isSemigroupMorphism f
-  ; ε-homo  = λ x≈y → x≈y
+^-isMonoidHomoorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
+^-isMonoidHomoorphism f = record
+  { isMagmaHomomorphism = record
+    { isRelHomomorphism = record { cong = ^-cong₂ f }
+    ; homo = ^-homo f
+    }
+  ; ε-homo = Setoid.refl S
   }
+

From 1af553ef22f880c5c81c3d9cdcec7f6727b2c458 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Tue, 2 Apr 2024 21:29:29 -0400
Subject: [PATCH 02/19] and add to CHANGELOG

---
 CHANGELOG.md | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2b9d357511..e405b347be 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -36,6 +36,13 @@ Deprecated modules
 * `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` deprecated in favour of
   `Data.List.Relation.Binary.Sublist.Propositional.Slice`.
 
+Un-deprecated modules
+---------------------
+
+* The modules `Function.Endomorphism.Propositional` and
+  `Function.Endomorphism.Setoid` previously used the old `Function`
+  hierarchy but have now been ported to using the new one.
+  
 Deprecated names
 ----------------
 
@@ -173,7 +180,14 @@ Additions to existing modules
   rawModule          : RawModule R c ℓ
   ```
 
-* In `Algebra.Properties.Group`:
+* In `Algebra.Morphism.Structures`:
+  ```agda
+  IsSemigroupHomomorphism : (A → B) → Set _
+  IsSemigroupMonomorphism : (A → B) → Set _
+  IsSemigroupIsomorphism : (A → B) → Set _
+  ```
+  
+ * In `Algebra.Properties.Group`:
   ```agda
   isQuasigroup    : IsQuasigroup _∙_ _\\_ _//_
   quasigroup      : Quasigroup _ _

From 81230ecf0c8ff634433c9d17d53c9d2e8b3c1fd2 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Tue, 2 Apr 2024 21:32:48 -0400
Subject: [PATCH 03/19] fix whitespace

---
 CHANGELOG.md                                 | 4 ++--
 src/Function/Endomorphism/Propositional.agda | 2 +-
 src/Function/Endomorphism/Setoid.agda        | 6 +++---
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e405b347be..c611e0bbd1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -42,7 +42,7 @@ Un-deprecated modules
 * The modules `Function.Endomorphism.Propositional` and
   `Function.Endomorphism.Setoid` previously used the old `Function`
   hierarchy but have now been ported to using the new one.
-  
+
 Deprecated names
 ----------------
 
@@ -186,7 +186,7 @@ Additions to existing modules
   IsSemigroupMonomorphism : (A → B) → Set _
   IsSemigroupIsomorphism : (A → B) → Set _
   ```
-  
+
  * In `Algebra.Properties.Group`:
   ```agda
   isQuasigroup    : IsQuasigroup _∙_ _\\_ _//_
diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda
index c6995bd6fd..369315d39b 100644
--- a/src/Function/Endomorphism/Propositional.agda
+++ b/src/Function/Endomorphism/Propositional.agda
@@ -97,7 +97,7 @@ private
   { isRelHomomorphism = record { cong = cong (f ^_) }
   ; homo = ^-homo f
   }
-  
+
 ^-isMonoidMorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
 ^-isMonoidMorphism f = record
   { isMagmaHomomorphism = ^-isSemigroupMorphism f
diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda
index be4fa80816..fbb4c31ff9 100644
--- a/src/Function/Endomorphism/Setoid.agda
+++ b/src/Function/Endomorphism/Setoid.agda
@@ -43,7 +43,7 @@ infixr 8 _^_
 private
   id : Endo
   id = identity S
-  
+
 _^_ : Endo → ℕ → Endo
 f ^ zero  = id
 f ^ suc n = f ∘ (f ^ n)
@@ -62,7 +62,7 @@ f ^ suc n = f ∘ (f ^ n)
 ∘-isMagma : IsMagma _≈_ _∘_
 ∘-isMagma = record
   { isEquivalence = isEquivalence
-  ; ∙-cong        = λ {_} {_} {_} {v} x≈y u≈v → S.trans u≈v (cong v x≈y) 
+  ; ∙-cong        = λ {_} {_} {_} {v} x≈y u≈v → S.trans u≈v (cong v x≈y)
   }
   where
     module S = Setoid S
@@ -94,7 +94,7 @@ private
 
   ∘-id-rawMonoid : RawMonoid (c ⊔ e) (c ⊔ e)
   ∘-id-rawMonoid = Monoid.rawMonoid ∘-id-monoid
-  
+
 ------------------------------------------------------------------------
 -- Homomorphism
 

From 3305480bb0ed6ba527f772f9dfbb1f51960a9a3d Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Wed, 3 Apr 2024 21:18:27 -0400
Subject: [PATCH 04/19] fix warning: it was pointing to a record that did not
 exist.

---
 src/Algebra/Morphism.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Algebra/Morphism.agda b/src/Algebra/Morphism.agda
index 45b7a46a1d..e3bcb53e9b 100644
--- a/src/Algebra/Morphism.agda
+++ b/src/Algebra/Morphism.agda
@@ -185,7 +185,7 @@ module _ {c₁ ℓ₁ c₂ ℓ₂}
 
 {-# WARNING_ON_USAGE IsSemigroupMorphism
 "Warning: IsSemigroupMorphism was deprecated in v1.5.
-Please use IsSemigroupHomomorphism instead."
+Please use IsMagmaHomomorphism instead."
 #-}
 {-# WARNING_ON_USAGE IsMonoidMorphism
 "Warning: IsMonoidMorphism was deprecated in v1.5.

From d1cae72dcb3b44d4ba3c7290f3535544be32ab1e Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Wed, 3 Apr 2024 21:31:13 -0400
Subject: [PATCH 05/19] fix things as per Matthew's review - though this
 remains a breaking change.

---
 CHANGELOG.md                                 |  7 -------
 src/Algebra/Morphism/Structures.agda         |  9 ---------
 src/Function/Endomorphism/Propositional.agda | 10 ++++++----
 src/Function/Endomorphism/Setoid.agda        |  4 ++--
 4 files changed, 8 insertions(+), 22 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c611e0bbd1..c3aa7ad6d5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -180,13 +180,6 @@ Additions to existing modules
   rawModule          : RawModule R c ℓ
   ```
 
-* In `Algebra.Morphism.Structures`:
-  ```agda
-  IsSemigroupHomomorphism : (A → B) → Set _
-  IsSemigroupMonomorphism : (A → B) → Set _
-  IsSemigroupIsomorphism : (A → B) → Set _
-  ```
-
  * In `Algebra.Properties.Group`:
   ```agda
   isQuasigroup    : IsQuasigroup _∙_ _\\_ _//_
diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda
index 3dad55ac87..03d2cc0b94 100644
--- a/src/Algebra/Morphism/Structures.agda
+++ b/src/Algebra/Morphism/Structures.agda
@@ -68,15 +68,6 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher
       ; surjective     = surjective
       }
 
-  IsSemigroupHomomorphism : (⟦_⟧ : A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
-  IsSemigroupHomomorphism = IsMagmaHomomorphism
-
-  IsSemigroupMonomorphism : (⟦_⟧ : A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
-  IsSemigroupMonomorphism = IsMagmaMonomorphism
-
-  IsSemigroupIsomorphism : (⟦_⟧ : A → B) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
-  IsSemigroupIsomorphism = IsMagmaIsomorphism
-
 ------------------------------------------------------------------------
 -- Morphisms over monoid-like structures
 ------------------------------------------------------------------------
diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda
index 369315d39b..61176f79f5 100644
--- a/src/Function/Endomorphism/Propositional.agda
+++ b/src/Function/Endomorphism/Propositional.agda
@@ -7,10 +7,12 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 module Function.Endomorphism.Propositional {a} (A : Set a) where
 
-open import Algebra
-open import Algebra.Structures
+open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
+open import Algebra.Core
+open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
 open import Algebra.Morphism
-open Definitions
+  using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
+open Definitions using (Homomorphic₂)
 
 open import Data.Nat.Base using (ℕ; _+_; zero; suc; +-rawMagma; +-0-rawMonoid)
 open import Data.Nat.Properties using (+-0-monoid; +-semigroup)
@@ -92,7 +94,7 @@ private
 ------------------------------------------------------------------------
 -- Homomorphism
 
-^-isSemigroupMorphism : ∀ f → IsSemigroupHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isSemigroupMorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
 ^-isSemigroupMorphism f = record
   { isRelHomomorphism = record { cong = cong (f ^_) }
   ; homo = ^-homo f
diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda
index fbb4c31ff9..bd3b7109ba 100644
--- a/src/Function/Endomorphism/Setoid.agda
+++ b/src/Function/Endomorphism/Setoid.agda
@@ -15,7 +15,7 @@ open import Agda.Builtin.Equality
 open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
 open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
 open import Algebra.Morphism
-  using (module Definitions; IsSemigroupHomomorphism; IsMonoidHomomorphism)
+  using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
 open Definitions using (Homomorphic₂)
 open import Data.Nat.Base using (ℕ; _+_; +-rawMagma; +-0-rawMonoid)
 open ℕ
@@ -98,7 +98,7 @@ private
 ------------------------------------------------------------------------
 -- Homomorphism
 
-^-isSemigroupHomomorphism : ∀ f → IsSemigroupHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isSemigroupHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
 ^-isSemigroupHomomorphism f = record
   { isRelHomomorphism = record { cong = ^-cong₂ f }
   ; homo = ^-homo f

From 93e9e0fdf482164c0fb7e709ef8799fbc3fa0385 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Mon, 8 Apr 2024 21:51:18 -0400
Subject: [PATCH 06/19] take care of comments from James.

---
 CHANGELOG.md                                 |  2 +-
 src/Function/Endomorphism/Propositional.agda | 29 ++++++++++---
 src/Function/Endomorphism/Setoid.agda        | 43 +++++++++++++-------
 3 files changed, 52 insertions(+), 22 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c3aa7ad6d5..c574e6d4ad 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -180,7 +180,7 @@ Additions to existing modules
   rawModule          : RawModule R c ℓ
   ```
 
- * In `Algebra.Properties.Group`:
+* In `Algebra.Properties.Group`:
   ```agda
   isQuasigroup    : IsQuasigroup _∙_ _\\_ _//_
   quasigroup      : Quasigroup _ _
diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda
index 61176f79f5..440456916f 100644
--- a/src/Function/Endomorphism/Propositional.agda
+++ b/src/Function/Endomorphism/Propositional.agda
@@ -14,7 +14,7 @@ open import Algebra.Morphism
   using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
 open Definitions using (Homomorphic₂)
 
-open import Data.Nat.Base using (ℕ; _+_; zero; suc; +-rawMagma; +-0-rawMonoid)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_; +-rawMagma; +-0-rawMonoid)
 open import Data.Nat.Properties using (+-0-monoid; +-semigroup)
 open import Data.Product.Base using (_,_)
 
@@ -94,14 +94,31 @@ private
 ------------------------------------------------------------------------
 -- Homomorphism
 
-^-isSemigroupMorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
-^-isSemigroupMorphism f = record
+^-isMagmaHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isMagmaHomomorphism f = record
   { isRelHomomorphism = record { cong = cong (f ^_) }
   ; homo = ^-homo f
   }
 
-^-isMonoidMorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
-^-isMonoidMorphism f = record
-  { isMagmaHomomorphism = ^-isSemigroupMorphism f
+^-isMonoidHomomorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
+^-isMonoidHomomorphism f = record
+  { isMagmaHomomorphism = ^-isMagmaHomomorphism f
   ; ε-homo = refl
   }
+
+------------------------------------------------------------------------
+-- Deprecations
+
+-- Version 2.1
+
+^-isSemigroupMorphism = ^-isMagmaHomomorphism
+{-# WARNING_ON_USAGE ^-isSemigroupMorphism
+"Warning: ^-isSemigroupMorphism was deprecated in v2.1.
+Please use ^-isMagmaHomomorphism instead."
+#-}
+
+^-isMonoidMorphism = ^-isMonoidHomomorphism
+{-# WARNING_ON_USAGE ^-isMonoidMorphism
+"Warning: ^-isMonoidMorphism was deprecated in v2.1.
+Please use ^-isMonoidHomomorphism instead."
+#-}
diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda
index bd3b7109ba..687e6f1033 100644
--- a/src/Function/Endomorphism/Setoid.agda
+++ b/src/Function/Endomorphism/Setoid.agda
@@ -17,8 +17,7 @@ open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
 open import Algebra.Morphism
   using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
 open Definitions using (Homomorphic₂)
-open import Data.Nat.Base using (ℕ; _+_; +-rawMagma; +-0-rawMonoid)
-open ℕ
+open import Data.Nat.Base using (ℕ; zero; suc; _+_; +-rawMagma; +-0-rawMonoid)
 open import Data.Nat.Properties using (+-semigroup; +-identityʳ)
 open import Data.Product.Base using (_,_)
 open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
@@ -29,8 +28,8 @@ open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (_Preserves_⟶_)
 
 private
-  module E = Setoid (S ⇨ S)
-  open E hiding (refl)
+  open module E = Setoid (S ⇨ S) hiding (refl)
+  module S = Setoid S
   open Func using (cong)
 ------------------------------------------------------------------------
 -- Basic type and functions
@@ -49,10 +48,10 @@ f ^ zero  = id
 f ^ suc n = f ∘ (f ^ n)
 
 ^-cong₂ : ∀ f → (f ^_) Preserves _≡_ ⟶ _≈_
-^-cong₂ f {n} refl = cong (f ^ n) (Setoid.refl S)
+^-cong₂ f {n} refl = cong (f ^ n) S.refl
 
 ^-homo : ∀ f → Homomorphic₂ ℕ Endo _≈_ (f ^_) _+_ _∘_
-^-homo f zero    n           = Setoid.refl S
+^-homo f zero    n           = S.refl
 ^-homo f (suc m) zero    = ^-cong₂ f (+-identityʳ m)
 ^-homo f (suc m) (suc n) = ^-homo f m (suc n)
 
@@ -64,8 +63,6 @@ f ^ suc n = f ∘ (f ^ n)
   { isEquivalence = isEquivalence
   ; ∙-cong        = λ {_} {_} {_} {v} x≈y u≈v → S.trans u≈v (cong v x≈y)
   }
-  where
-    module S = Setoid S
 
 ∘-magma : Magma (c ⊔ e) (c ⊔ e)
 ∘-magma = record { isMagma = ∘-isMagma }
@@ -73,7 +70,7 @@ f ^ suc n = f ∘ (f ^ n)
 ∘-isSemigroup : IsSemigroup _≈_ _∘_
 ∘-isSemigroup = record
   { isMagma = ∘-isMagma
-  ; assoc   = λ h g f {s} → Setoid.refl S
+  ; assoc   = λ _ _ _ → S.refl
   }
 
 ∘-semigroup : Semigroup (c ⊔ e) (c ⊔ e)
@@ -82,7 +79,7 @@ f ^ suc n = f ∘ (f ^ n)
 ∘-id-isMonoid : IsMonoid _≈_ _∘_ id
 ∘-id-isMonoid = record
   { isSemigroup = ∘-isSemigroup
-  ; identity    = (λ f → Setoid.refl S) , (λ _ → Setoid.refl S)
+  ; identity    = (λ _ → S.refl) , (λ _ → S.refl)
   }
 
 ∘-id-monoid : Monoid (c ⊔ e) (c ⊔ e)
@@ -98,18 +95,34 @@ private
 ------------------------------------------------------------------------
 -- Homomorphism
 
-^-isSemigroupHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
-^-isSemigroupHomomorphism f = record
+^-isMagmaHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isMagmaHomomorphism f = record
   { isRelHomomorphism = record { cong = ^-cong₂ f }
   ; homo = ^-homo f
   }
 
-^-isMonoidHomoorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
-^-isMonoidHomoorphism f = record
+^-isMonoidHomomorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
+^-isMonoidHomomorphism f = record
   { isMagmaHomomorphism = record
     { isRelHomomorphism = record { cong = ^-cong₂ f }
     ; homo = ^-homo f
     }
-  ; ε-homo = Setoid.refl S
+  ; ε-homo = S.refl
   }
 
+------------------------------------------------------------------------
+-- Deprecations
+
+-- Version 2.1
+
+^-isSemigroupMorphism = ^-isMagmaHomomorphism
+{-# WARNING_ON_USAGE ^-isSemigroupMorphism
+"Warning: ^-isSemigroupMorphism was deprecated in v2.1.
+Please use ^-isMagmaHomomorphism instead."
+#-}
+
+^-isMonoidMorphism = ^-isMonoidHomomorphism
+{-# WARNING_ON_USAGE ^-isMonoidMorphism
+"Warning: ^-isMonoidMorphism was deprecated in v2.1.
+Please use ^-isMonoidHomomorphism instead."
+#-}

From a2e3c269a2c8243f82cdb2145ca320524883492e Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Wed, 15 May 2024 22:28:49 -0400
Subject: [PATCH 07/19] adjust CHANGELOG for what will be implemented shortly

---
 CHANGELOG.md | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6ed0da2652..775d811e9e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -46,12 +46,10 @@ Deprecated modules
 * `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` deprecated in favour of
   `Data.List.Relation.Binary.Sublist.Propositional.Slice`.
 
-Un-deprecated modules
----------------------
-
 * The modules `Function.Endomorphism.Propositional` and
-  `Function.Endomorphism.Setoid` previously used the old `Function`
-  hierarchy but have now been ported to using the new one.
+  `Function.Endomorphism.Setoid` that use the old `Function`
+  hierarchy. Use `Function.Endo.Propositional` and
+  `Function.Endo.Setoid` instead.
 
 Deprecated names
 ----------------
@@ -138,6 +136,11 @@ New modules
   indexedSetoid        : {A : Set a} → IndexedSetoid ℕ a _
   ```
 
+* The modules `Function.Endo.Propositional` and
+  `Function.Endo.Setoid` are new but are actually proper ports of
+  `Function.Endomorphism.Propositional` and
+  `Function.Endomorphism.Setoid`.
+
 * `Function.Relation.Binary.Equality`
   ```agda
   setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _

From e9fc1458efbf615a595627958330e0aab3f5d849 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Wed, 15 May 2024 22:30:53 -0400
Subject: [PATCH 08/19] Revert "take care of comments from James."

This reverts commit 93e9e0fdf482164c0fb7e709ef8799fbc3fa0385.
---
 src/Function/Endomorphism/Propositional.agda | 29 +++----------
 src/Function/Endomorphism/Setoid.agda        | 43 +++++++-------------
 2 files changed, 21 insertions(+), 51 deletions(-)

diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda
index 440456916f..61176f79f5 100644
--- a/src/Function/Endomorphism/Propositional.agda
+++ b/src/Function/Endomorphism/Propositional.agda
@@ -14,7 +14,7 @@ open import Algebra.Morphism
   using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
 open Definitions using (Homomorphic₂)
 
-open import Data.Nat.Base using (ℕ; zero; suc; _+_; +-rawMagma; +-0-rawMonoid)
+open import Data.Nat.Base using (ℕ; _+_; zero; suc; +-rawMagma; +-0-rawMonoid)
 open import Data.Nat.Properties using (+-0-monoid; +-semigroup)
 open import Data.Product.Base using (_,_)
 
@@ -94,31 +94,14 @@ private
 ------------------------------------------------------------------------
 -- Homomorphism
 
-^-isMagmaHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
-^-isMagmaHomomorphism f = record
+^-isSemigroupMorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isSemigroupMorphism f = record
   { isRelHomomorphism = record { cong = cong (f ^_) }
   ; homo = ^-homo f
   }
 
-^-isMonoidHomomorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
-^-isMonoidHomomorphism f = record
-  { isMagmaHomomorphism = ^-isMagmaHomomorphism f
+^-isMonoidMorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
+^-isMonoidMorphism f = record
+  { isMagmaHomomorphism = ^-isSemigroupMorphism f
   ; ε-homo = refl
   }
-
-------------------------------------------------------------------------
--- Deprecations
-
--- Version 2.1
-
-^-isSemigroupMorphism = ^-isMagmaHomomorphism
-{-# WARNING_ON_USAGE ^-isSemigroupMorphism
-"Warning: ^-isSemigroupMorphism was deprecated in v2.1.
-Please use ^-isMagmaHomomorphism instead."
-#-}
-
-^-isMonoidMorphism = ^-isMonoidHomomorphism
-{-# WARNING_ON_USAGE ^-isMonoidMorphism
-"Warning: ^-isMonoidMorphism was deprecated in v2.1.
-Please use ^-isMonoidHomomorphism instead."
-#-}
diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda
index 687e6f1033..bd3b7109ba 100644
--- a/src/Function/Endomorphism/Setoid.agda
+++ b/src/Function/Endomorphism/Setoid.agda
@@ -17,7 +17,8 @@ open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
 open import Algebra.Morphism
   using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
 open Definitions using (Homomorphic₂)
-open import Data.Nat.Base using (ℕ; zero; suc; _+_; +-rawMagma; +-0-rawMonoid)
+open import Data.Nat.Base using (ℕ; _+_; +-rawMagma; +-0-rawMonoid)
+open ℕ
 open import Data.Nat.Properties using (+-semigroup; +-identityʳ)
 open import Data.Product.Base using (_,_)
 open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
@@ -28,8 +29,8 @@ open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (_Preserves_⟶_)
 
 private
-  open module E = Setoid (S ⇨ S) hiding (refl)
-  module S = Setoid S
+  module E = Setoid (S ⇨ S)
+  open E hiding (refl)
   open Func using (cong)
 ------------------------------------------------------------------------
 -- Basic type and functions
@@ -48,10 +49,10 @@ f ^ zero  = id
 f ^ suc n = f ∘ (f ^ n)
 
 ^-cong₂ : ∀ f → (f ^_) Preserves _≡_ ⟶ _≈_
-^-cong₂ f {n} refl = cong (f ^ n) S.refl
+^-cong₂ f {n} refl = cong (f ^ n) (Setoid.refl S)
 
 ^-homo : ∀ f → Homomorphic₂ ℕ Endo _≈_ (f ^_) _+_ _∘_
-^-homo f zero    n           = S.refl
+^-homo f zero    n           = Setoid.refl S
 ^-homo f (suc m) zero    = ^-cong₂ f (+-identityʳ m)
 ^-homo f (suc m) (suc n) = ^-homo f m (suc n)
 
@@ -63,6 +64,8 @@ f ^ suc n = f ∘ (f ^ n)
   { isEquivalence = isEquivalence
   ; ∙-cong        = λ {_} {_} {_} {v} x≈y u≈v → S.trans u≈v (cong v x≈y)
   }
+  where
+    module S = Setoid S
 
 ∘-magma : Magma (c ⊔ e) (c ⊔ e)
 ∘-magma = record { isMagma = ∘-isMagma }
@@ -70,7 +73,7 @@ f ^ suc n = f ∘ (f ^ n)
 ∘-isSemigroup : IsSemigroup _≈_ _∘_
 ∘-isSemigroup = record
   { isMagma = ∘-isMagma
-  ; assoc   = λ _ _ _ → S.refl
+  ; assoc   = λ h g f {s} → Setoid.refl S
   }
 
 ∘-semigroup : Semigroup (c ⊔ e) (c ⊔ e)
@@ -79,7 +82,7 @@ f ^ suc n = f ∘ (f ^ n)
 ∘-id-isMonoid : IsMonoid _≈_ _∘_ id
 ∘-id-isMonoid = record
   { isSemigroup = ∘-isSemigroup
-  ; identity    = (λ _ → S.refl) , (λ _ → S.refl)
+  ; identity    = (λ f → Setoid.refl S) , (λ _ → Setoid.refl S)
   }
 
 ∘-id-monoid : Monoid (c ⊔ e) (c ⊔ e)
@@ -95,34 +98,18 @@ private
 ------------------------------------------------------------------------
 -- Homomorphism
 
-^-isMagmaHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
-^-isMagmaHomomorphism f = record
+^-isSemigroupHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isSemigroupHomomorphism f = record
   { isRelHomomorphism = record { cong = ^-cong₂ f }
   ; homo = ^-homo f
   }
 
-^-isMonoidHomomorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
-^-isMonoidHomomorphism f = record
+^-isMonoidHomoorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
+^-isMonoidHomoorphism f = record
   { isMagmaHomomorphism = record
     { isRelHomomorphism = record { cong = ^-cong₂ f }
     ; homo = ^-homo f
     }
-  ; ε-homo = S.refl
+  ; ε-homo = Setoid.refl S
   }
 
-------------------------------------------------------------------------
--- Deprecations
-
--- Version 2.1
-
-^-isSemigroupMorphism = ^-isMagmaHomomorphism
-{-# WARNING_ON_USAGE ^-isSemigroupMorphism
-"Warning: ^-isSemigroupMorphism was deprecated in v2.1.
-Please use ^-isMagmaHomomorphism instead."
-#-}
-
-^-isMonoidMorphism = ^-isMonoidHomomorphism
-{-# WARNING_ON_USAGE ^-isMonoidMorphism
-"Warning: ^-isMonoidMorphism was deprecated in v2.1.
-Please use ^-isMonoidHomomorphism instead."
-#-}

From 9665443f12c1d62782c8f4f794d84cb0dd6fc0be Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Wed, 15 May 2024 22:34:46 -0400
Subject: [PATCH 09/19] Revert "fix things as per Matthew's review - though
 this remains a breaking change."

This reverts commit d1cae72dcb3b44d4ba3c7290f3535544be32ab1e.
---
 CHANGELOG.md                                 | 11 +++++------
 src/Algebra/Morphism/Structures.agda         |  9 +++++++++
 src/Function/Endomorphism/Propositional.agda | 10 ++++------
 src/Function/Endomorphism/Setoid.agda        |  4 ++--
 4 files changed, 20 insertions(+), 14 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 775d811e9e..c5e24b3f0a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -245,19 +245,18 @@ Additions to existing modules
   rawModule          : RawModule R c ℓ
   ```
 
-* In `Algebra.Morphism.Structures`
+* In `Algebra.Morphism.Structures`:
   ```agda
-  module SuccessorSetMorphisms (N₁ : RawSuccessorSet a ℓ₁) (N₂ : RawSuccessorSet b ℓ₂) where
-    record IsSuccessorSetHomomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
-    record IsSuccessorSetMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
-    record IsSuccessorSetIsomorphism  (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
+  IsSemigroupHomomorphism : (A → B) → Set _
+  IsSemigroupMonomorphism : (A → B) → Set _
+  IsSemigroupIsomorphism : (A → B) → Set _
+  ```
 
 * In `Algebra.Properties.AbelianGroup`:
   ```
   ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x
   ```
 
-* In `Algebra.Properties.Group`:
   ```agda
   isQuasigroup    : IsQuasigroup _∙_ _\\_ _//_
   quasigroup      : Quasigroup _ _
diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda
index d98cc34f8d..a02f104e04 100644
--- a/src/Algebra/Morphism/Structures.agda
+++ b/src/Algebra/Morphism/Structures.agda
@@ -116,6 +116,15 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher
       ; surjective     = surjective
       }
 
+  IsSemigroupHomomorphism : (⟦_⟧ : A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  IsSemigroupHomomorphism = IsMagmaHomomorphism
+
+  IsSemigroupMonomorphism : (⟦_⟧ : A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  IsSemigroupMonomorphism = IsMagmaMonomorphism
+
+  IsSemigroupIsomorphism : (⟦_⟧ : A → B) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
+  IsSemigroupIsomorphism = IsMagmaIsomorphism
+
 ------------------------------------------------------------------------
 -- Morphisms over monoid-like structures
 ------------------------------------------------------------------------
diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda
index 61176f79f5..369315d39b 100644
--- a/src/Function/Endomorphism/Propositional.agda
+++ b/src/Function/Endomorphism/Propositional.agda
@@ -7,12 +7,10 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 module Function.Endomorphism.Propositional {a} (A : Set a) where
 
-open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
-open import Algebra.Core
-open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
+open import Algebra
+open import Algebra.Structures
 open import Algebra.Morphism
-  using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
-open Definitions using (Homomorphic₂)
+open Definitions
 
 open import Data.Nat.Base using (ℕ; _+_; zero; suc; +-rawMagma; +-0-rawMonoid)
 open import Data.Nat.Properties using (+-0-monoid; +-semigroup)
@@ -94,7 +92,7 @@ private
 ------------------------------------------------------------------------
 -- Homomorphism
 
-^-isSemigroupMorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isSemigroupMorphism : ∀ f → IsSemigroupHomomorphism +-rawMagma ∘-rawMagma (f ^_)
 ^-isSemigroupMorphism f = record
   { isRelHomomorphism = record { cong = cong (f ^_) }
   ; homo = ^-homo f
diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda
index bd3b7109ba..fbb4c31ff9 100644
--- a/src/Function/Endomorphism/Setoid.agda
+++ b/src/Function/Endomorphism/Setoid.agda
@@ -15,7 +15,7 @@ open import Agda.Builtin.Equality
 open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
 open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
 open import Algebra.Morphism
-  using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
+  using (module Definitions; IsSemigroupHomomorphism; IsMonoidHomomorphism)
 open Definitions using (Homomorphic₂)
 open import Data.Nat.Base using (ℕ; _+_; +-rawMagma; +-0-rawMonoid)
 open ℕ
@@ -98,7 +98,7 @@ private
 ------------------------------------------------------------------------
 -- Homomorphism
 
-^-isSemigroupHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isSemigroupHomomorphism : ∀ f → IsSemigroupHomomorphism +-rawMagma ∘-rawMagma (f ^_)
 ^-isSemigroupHomomorphism f = record
   { isRelHomomorphism = record { cong = ^-cong₂ f }
   ; homo = ^-homo f

From 8cb04db53a9de263fb64ca6bb91f1d8276dcea22 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Wed, 15 May 2024 22:36:47 -0400
Subject: [PATCH 10/19] Revert "fix whitespace"

This reverts commit 81230ecf0c8ff634433c9d17d53c9d2e8b3c1fd2.
---
 CHANGELOG.md                                 | 2 +-
 src/Function/Endomorphism/Propositional.agda | 2 +-
 src/Function/Endomorphism/Setoid.agda        | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c5e24b3f0a..a560d089ef 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -251,12 +251,12 @@ Additions to existing modules
   IsSemigroupMonomorphism : (A → B) → Set _
   IsSemigroupIsomorphism : (A → B) → Set _
   ```
-
 * In `Algebra.Properties.AbelianGroup`:
   ```
   ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x
   ```
 
+ * In `Algebra.Properties.Group`:
   ```agda
   isQuasigroup    : IsQuasigroup _∙_ _\\_ _//_
   quasigroup      : Quasigroup _ _
diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda
index 369315d39b..c6995bd6fd 100644
--- a/src/Function/Endomorphism/Propositional.agda
+++ b/src/Function/Endomorphism/Propositional.agda
@@ -97,7 +97,7 @@ private
   { isRelHomomorphism = record { cong = cong (f ^_) }
   ; homo = ^-homo f
   }
-
+  
 ^-isMonoidMorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
 ^-isMonoidMorphism f = record
   { isMagmaHomomorphism = ^-isSemigroupMorphism f
diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda
index fbb4c31ff9..be4fa80816 100644
--- a/src/Function/Endomorphism/Setoid.agda
+++ b/src/Function/Endomorphism/Setoid.agda
@@ -43,7 +43,7 @@ infixr 8 _^_
 private
   id : Endo
   id = identity S
-
+  
 _^_ : Endo → ℕ → Endo
 f ^ zero  = id
 f ^ suc n = f ∘ (f ^ n)
@@ -62,7 +62,7 @@ f ^ suc n = f ∘ (f ^ n)
 ∘-isMagma : IsMagma _≈_ _∘_
 ∘-isMagma = record
   { isEquivalence = isEquivalence
-  ; ∙-cong        = λ {_} {_} {_} {v} x≈y u≈v → S.trans u≈v (cong v x≈y)
+  ; ∙-cong        = λ {_} {_} {_} {v} x≈y u≈v → S.trans u≈v (cong v x≈y) 
   }
   where
     module S = Setoid S
@@ -94,7 +94,7 @@ private
 
   ∘-id-rawMonoid : RawMonoid (c ⊔ e) (c ⊔ e)
   ∘-id-rawMonoid = Monoid.rawMonoid ∘-id-monoid
-
+  
 ------------------------------------------------------------------------
 -- Homomorphism
 

From 154fb0e9e0dd7d444e73a0d0333b51590878a494 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Wed, 15 May 2024 22:37:29 -0400
Subject: [PATCH 11/19] Revert "port over two modules"

This reverts commit 6619f114346e86ead3cf62b1170ab23d31056b48.
---
 src/Algebra/Morphism/Structures.agda         |  8 --
 src/Function/Endomorphism/Propositional.agda | 35 ++++----
 src/Function/Endomorphism/Setoid.agda        | 84 ++++++++------------
 3 files changed, 47 insertions(+), 80 deletions(-)

diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda
index a02f104e04..c352904be7 100644
--- a/src/Algebra/Morphism/Structures.agda
+++ b/src/Algebra/Morphism/Structures.agda
@@ -116,14 +116,6 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher
       ; surjective     = surjective
       }
 
-  IsSemigroupHomomorphism : (⟦_⟧ : A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
-  IsSemigroupHomomorphism = IsMagmaHomomorphism
-
-  IsSemigroupMonomorphism : (⟦_⟧ : A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
-  IsSemigroupMonomorphism = IsMagmaMonomorphism
-
-  IsSemigroupIsomorphism : (⟦_⟧ : A → B) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
-  IsSemigroupIsomorphism = IsMagmaIsomorphism
 
 ------------------------------------------------------------------------
 -- Morphisms over monoid-like structures
diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda
index c6995bd6fd..c8dd685328 100644
--- a/src/Function/Endomorphism/Propositional.agda
+++ b/src/Function/Endomorphism/Propositional.agda
@@ -5,19 +5,21 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
+
+-- Disabled to prevent warnings from deprecated names
+{-# OPTIONS --warn=noUserWarning #-}
+
 module Function.Endomorphism.Propositional {a} (A : Set a) where
 
 open import Algebra
-open import Algebra.Structures
-open import Algebra.Morphism
-open Definitions
+open import Algebra.Morphism; open Definitions
 
-open import Data.Nat.Base using (ℕ; _+_; zero; suc; +-rawMagma; +-0-rawMonoid)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Data.Nat.Properties using (+-0-monoid; +-semigroup)
 open import Data.Product.Base using (_,_)
 
 open import Function.Base using (id; _∘′_; _∋_)
-open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
+open import Function.Equality using (_⟨$⟩_)
 open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
 import Relation.Binary.PropositionalEquality.Properties as ≡
@@ -35,7 +37,7 @@ fromSetoidEndo = _⟨$⟩_
 
 toSetoidEndo : Endo → Setoid.Endo
 toSetoidEndo f = record
-  { to = f
+  { _⟨$⟩_ = f
   ; cong  = cong f
   }
 
@@ -82,24 +84,17 @@ f ^ suc n = f ∘′ (f ^ n)
 ∘-id-monoid : Monoid _ _
 ∘-id-monoid = record { isMonoid = ∘-id-isMonoid }
 
-private
-  ∘-rawMagma : RawMagma a a
-  ∘-rawMagma = Semigroup.rawMagma ∘-semigroup
-
-  ∘-id-rawMonoid : RawMonoid a a
-  ∘-id-rawMonoid = Monoid.rawMonoid ∘-id-monoid
-
 ------------------------------------------------------------------------
 -- Homomorphism
 
-^-isSemigroupMorphism : ∀ f → IsSemigroupHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isSemigroupMorphism : ∀ f → IsSemigroupMorphism +-semigroup ∘-semigroup (f ^_)
 ^-isSemigroupMorphism f = record
-  { isRelHomomorphism = record { cong = cong (f ^_) }
-  ; homo = ^-homo f
+  { ⟦⟧-cong = cong (f ^_)
+  ; ∙-homo  = ^-homo f
   }
-  
-^-isMonoidMorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
+
+^-isMonoidMorphism : ∀ f → IsMonoidMorphism +-0-monoid ∘-id-monoid (f ^_)
 ^-isMonoidMorphism f = record
-  { isMagmaHomomorphism = ^-isSemigroupMorphism f
-  ; ε-homo = refl
+  { sm-homo = ^-isSemigroupMorphism f
+  ; ε-homo  = refl
   }
diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda
index be4fa80816..a715ef5262 100644
--- a/src/Function/Endomorphism/Setoid.agda
+++ b/src/Function/Endomorphism/Setoid.agda
@@ -6,55 +6,48 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
+-- Disabled to prevent warnings from deprecated names
+{-# OPTIONS --warn=noUserWarning #-}
+
+open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.Bundles using (Setoid)
 
 module Function.Endomorphism.Setoid {c e} (S : Setoid c e) where
 
 open import Agda.Builtin.Equality
 
-open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
-open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
-open import Algebra.Morphism
-  using (module Definitions; IsSemigroupHomomorphism; IsMonoidHomomorphism)
-open Definitions using (Homomorphic₂)
-open import Data.Nat.Base using (ℕ; _+_; +-rawMagma; +-0-rawMonoid)
-open ℕ
-open import Data.Nat.Properties using (+-semigroup; +-identityʳ)
+open import Algebra
+open import Algebra.Structures
+open import Algebra.Morphism; open Definitions
+open import Function.Equality using (setoid; _⟶_; id; _∘_; cong)
+open import Data.Nat.Base using (ℕ; _+_); open ℕ
+open import Data.Nat.Properties
 open import Data.Product.Base using (_,_)
-open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
-open import Function.Construct.Identity using () renaming (function to identity)
-open import Function.Construct.Composition using () renaming (function to _∘_)
-open import Function.Relation.Binary.Setoid.Equality as Eq using (_⇨_)
-open import Level using (Level; _⊔_)
-open import Relation.Binary.Core using (_Preserves_⟶_)
+
+import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial as Trivial
 
 private
-  module E = Setoid (S ⇨ S)
+  module E = Setoid (setoid S (Trivial.indexedSetoid S))
   open E hiding (refl)
-  open Func using (cong)
+
 ------------------------------------------------------------------------
 -- Basic type and functions
 
 Endo : Set _
-Endo = S ⟶ₛ S
+Endo = S ⟶ S
 
 infixr 8 _^_
 
-private
-  id : Endo
-  id = identity S
-  
 _^_ : Endo → ℕ → Endo
 f ^ zero  = id
 f ^ suc n = f ∘ (f ^ n)
 
 ^-cong₂ : ∀ f → (f ^_) Preserves _≡_ ⟶ _≈_
-^-cong₂ f {n} refl = cong (f ^ n) (Setoid.refl S)
+^-cong₂ f {n} refl = cong (f ^ n)
 
 ^-homo : ∀ f → Homomorphic₂ ℕ Endo _≈_ (f ^_) _+_ _∘_
-^-homo f zero    n           = Setoid.refl S
-^-homo f (suc m) zero    = ^-cong₂ f (+-identityʳ m)
-^-homo f (suc m) (suc n) = ^-homo f m (suc n)
+^-homo f zero    n x≈y = cong (f ^ n) x≈y
+^-homo f (suc m) n x≈y = cong f (^-homo f m n x≈y)
 
 ------------------------------------------------------------------------
 -- Structures
@@ -62,54 +55,41 @@ f ^ suc n = f ∘ (f ^ n)
 ∘-isMagma : IsMagma _≈_ _∘_
 ∘-isMagma = record
   { isEquivalence = isEquivalence
-  ; ∙-cong        = λ {_} {_} {_} {v} x≈y u≈v → S.trans u≈v (cong v x≈y) 
+  ; ∙-cong        = λ g f x → g (f x)
   }
-  where
-    module S = Setoid S
 
-∘-magma : Magma (c ⊔ e) (c ⊔ e)
+∘-magma : Magma _ _
 ∘-magma = record { isMagma = ∘-isMagma }
 
 ∘-isSemigroup : IsSemigroup _≈_ _∘_
 ∘-isSemigroup = record
   { isMagma = ∘-isMagma
-  ; assoc   = λ h g f {s} → Setoid.refl S
+  ; assoc   = λ h g f x≈y → cong h (cong g (cong f x≈y))
   }
 
-∘-semigroup : Semigroup (c ⊔ e) (c ⊔ e)
+∘-semigroup : Semigroup _ _
 ∘-semigroup = record { isSemigroup = ∘-isSemigroup }
 
 ∘-id-isMonoid : IsMonoid _≈_ _∘_ id
 ∘-id-isMonoid = record
   { isSemigroup = ∘-isSemigroup
-  ; identity    = (λ f → Setoid.refl S) , (λ _ → Setoid.refl S)
+  ; identity    = cong , cong
   }
 
-∘-id-monoid : Monoid (c ⊔ e) (c ⊔ e)
+∘-id-monoid : Monoid _ _
 ∘-id-monoid = record { isMonoid = ∘-id-isMonoid }
 
-private
-  ∘-rawMagma : RawMagma (c ⊔ e) (c ⊔ e)
-  ∘-rawMagma = Semigroup.rawMagma ∘-semigroup
-
-  ∘-id-rawMonoid : RawMonoid (c ⊔ e) (c ⊔ e)
-  ∘-id-rawMonoid = Monoid.rawMonoid ∘-id-monoid
-  
 ------------------------------------------------------------------------
 -- Homomorphism
 
-^-isSemigroupHomomorphism : ∀ f → IsSemigroupHomomorphism +-rawMagma ∘-rawMagma (f ^_)
-^-isSemigroupHomomorphism f = record
-  { isRelHomomorphism = record { cong = ^-cong₂ f }
-  ; homo = ^-homo f
+^-isSemigroupMorphism : ∀ f → IsSemigroupMorphism +-semigroup ∘-semigroup (f ^_)
+^-isSemigroupMorphism f = record
+  { ⟦⟧-cong = ^-cong₂ f
+  ; ∙-homo  = ^-homo f
   }
 
-^-isMonoidHomoorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
-^-isMonoidHomoorphism f = record
-  { isMagmaHomomorphism = record
-    { isRelHomomorphism = record { cong = ^-cong₂ f }
-    ; homo = ^-homo f
-    }
-  ; ε-homo = Setoid.refl S
+^-isMonoidMorphism : ∀ f → IsMonoidMorphism +-0-monoid ∘-id-monoid (f ^_)
+^-isMonoidMorphism f = record
+  { sm-homo = ^-isSemigroupMorphism f
+  ; ε-homo  = λ x≈y → x≈y
   }
-

From d5d811363a555fdadd5d71899185869a39da2e0d Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Wed, 15 May 2024 22:48:04 -0400
Subject: [PATCH 12/19] rename these

---
 src/Function/Endo/Propositional.agda | 124 ++++++++++++++++++++++++++
 src/Function/Endo/Setoid.agda        | 128 +++++++++++++++++++++++++++
 2 files changed, 252 insertions(+)
 create mode 100644 src/Function/Endo/Propositional.agda
 create mode 100644 src/Function/Endo/Setoid.agda

diff --git a/src/Function/Endo/Propositional.agda b/src/Function/Endo/Propositional.agda
new file mode 100644
index 0000000000..d7b1f2c9f5
--- /dev/null
+++ b/src/Function/Endo/Propositional.agda
@@ -0,0 +1,124 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Endomorphisms on a Set
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+module Function.Endo.Propositional {a} (A : Set a) where
+
+open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
+open import Algebra.Core
+open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
+open import Algebra.Morphism
+  using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
+open Definitions using (Homomorphic₂)
+
+open import Data.Nat.Base using (ℕ; zero; suc; _+_; +-rawMagma; +-0-rawMonoid)
+open import Data.Nat.Properties using (+-0-monoid; +-semigroup)
+open import Data.Product.Base using (_,_)
+
+open import Function.Base using (id; _∘′_; _∋_)
+open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
+open import Relation.Binary.Core using (_Preserves_⟶_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
+import Relation.Binary.PropositionalEquality.Properties as ≡
+
+import Function.Endo.Setoid (≡.setoid A) as Setoid
+
+Endo : Set a
+Endo = A → A
+
+------------------------------------------------------------------------
+-- Conversion back and forth with the Setoid-based notion of Endomorphism
+
+fromSetoidEndo : Setoid.Endo → Endo
+fromSetoidEndo = _⟨$⟩_
+
+toSetoidEndo : Endo → Setoid.Endo
+toSetoidEndo f = record
+  { to = f
+  ; cong  = cong f
+  }
+
+------------------------------------------------------------------------
+-- N-th composition
+
+infixr 8 _^_
+
+_^_ : Endo → ℕ → Endo
+f ^ zero  = id
+f ^ suc n = f ∘′ (f ^ n)
+
+^-homo : ∀ f → Homomorphic₂ ℕ Endo _≡_ (f ^_) _+_ _∘′_
+^-homo f zero    n = refl
+^-homo f (suc m) n = cong (f ∘′_) (^-homo f m n)
+
+------------------------------------------------------------------------
+-- Structures
+
+∘-isMagma : IsMagma _≡_ (Op₂ Endo ∋ _∘′_)
+∘-isMagma = record
+  { isEquivalence = ≡.isEquivalence
+  ; ∙-cong        = cong₂ _∘′_
+  }
+
+∘-magma : Magma _ _
+∘-magma = record { isMagma = ∘-isMagma }
+
+∘-isSemigroup : IsSemigroup _≡_ (Op₂ Endo ∋ _∘′_)
+∘-isSemigroup = record
+  { isMagma = ∘-isMagma
+  ; assoc   = λ _ _ _ → refl
+  }
+
+∘-semigroup : Semigroup _ _
+∘-semigroup = record { isSemigroup = ∘-isSemigroup }
+
+∘-id-isMonoid : IsMonoid _≡_ _∘′_ id
+∘-id-isMonoid = record
+  { isSemigroup = ∘-isSemigroup
+  ; identity    = (λ _ → refl) , (λ _ → refl)
+  }
+
+∘-id-monoid : Monoid _ _
+∘-id-monoid = record { isMonoid = ∘-id-isMonoid }
+
+private
+  ∘-rawMagma : RawMagma a a
+  ∘-rawMagma = Semigroup.rawMagma ∘-semigroup
+
+  ∘-id-rawMonoid : RawMonoid a a
+  ∘-id-rawMonoid = Monoid.rawMonoid ∘-id-monoid
+
+------------------------------------------------------------------------
+-- Homomorphism
+
+^-isMagmaHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isMagmaHomomorphism f = record
+  { isRelHomomorphism = record { cong = cong (f ^_) }
+  ; homo = ^-homo f
+  }
+
+^-isMonoidHomomorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
+^-isMonoidHomomorphism f = record
+  { isMagmaHomomorphism = ^-isMagmaHomomorphism f
+  ; ε-homo = refl
+  }
+
+------------------------------------------------------------------------
+-- Deprecations
+
+-- Version 2.1
+
+^-isSemigroupMorphism = ^-isMagmaHomomorphism
+{-# WARNING_ON_USAGE ^-isSemigroupMorphism
+"Warning: ^-isSemigroupMorphism was deprecated in v2.1.
+Please use ^-isMagmaHomomorphism instead."
+#-}
+
+^-isMonoidMorphism = ^-isMonoidHomomorphism
+{-# WARNING_ON_USAGE ^-isMonoidMorphism
+"Warning: ^-isMonoidMorphism was deprecated in v2.1.
+Please use ^-isMonoidHomomorphism instead."
+#-}
diff --git a/src/Function/Endo/Setoid.agda b/src/Function/Endo/Setoid.agda
new file mode 100644
index 0000000000..5a5b31337b
--- /dev/null
+++ b/src/Function/Endo/Setoid.agda
@@ -0,0 +1,128 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Endomorphisms on a Setoid
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (Setoid)
+
+module Function.Endo.Setoid {c e} (S : Setoid c e) where
+
+open import Agda.Builtin.Equality
+
+open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
+open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
+open import Algebra.Morphism
+  using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
+open Definitions using (Homomorphic₂)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_; +-rawMagma; +-0-rawMonoid)
+open import Data.Nat.Properties using (+-semigroup; +-identityʳ)
+open import Data.Product.Base using (_,_)
+open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
+open import Function.Construct.Identity using () renaming (function to identity)
+open import Function.Construct.Composition using () renaming (function to _∘_)
+open import Function.Relation.Binary.Setoid.Equality as Eq using (_⇨_)
+open import Level using (Level; _⊔_)
+open import Relation.Binary.Core using (_Preserves_⟶_)
+
+private
+  open module E = Setoid (S ⇨ S) hiding (refl)
+  module S = Setoid S
+  open Func using (cong)
+------------------------------------------------------------------------
+-- Basic type and functions
+
+Endo : Set _
+Endo = S ⟶ₛ S
+
+infixr 8 _^_
+
+private
+  id : Endo
+  id = identity S
+
+_^_ : Endo → ℕ → Endo
+f ^ zero  = id
+f ^ suc n = f ∘ (f ^ n)
+
+^-cong₂ : ∀ f → (f ^_) Preserves _≡_ ⟶ _≈_
+^-cong₂ f {n} refl = cong (f ^ n) S.refl
+
+^-homo : ∀ f → Homomorphic₂ ℕ Endo _≈_ (f ^_) _+_ _∘_
+^-homo f zero    n           = S.refl
+^-homo f (suc m) zero    = ^-cong₂ f (+-identityʳ m)
+^-homo f (suc m) (suc n) = ^-homo f m (suc n)
+
+------------------------------------------------------------------------
+-- Structures
+
+∘-isMagma : IsMagma _≈_ _∘_
+∘-isMagma = record
+  { isEquivalence = isEquivalence
+  ; ∙-cong        = λ {_} {_} {_} {v} x≈y u≈v → S.trans u≈v (cong v x≈y)
+  }
+
+∘-magma : Magma (c ⊔ e) (c ⊔ e)
+∘-magma = record { isMagma = ∘-isMagma }
+
+∘-isSemigroup : IsSemigroup _≈_ _∘_
+∘-isSemigroup = record
+  { isMagma = ∘-isMagma
+  ; assoc   = λ _ _ _ → S.refl
+  }
+
+∘-semigroup : Semigroup (c ⊔ e) (c ⊔ e)
+∘-semigroup = record { isSemigroup = ∘-isSemigroup }
+
+∘-id-isMonoid : IsMonoid _≈_ _∘_ id
+∘-id-isMonoid = record
+  { isSemigroup = ∘-isSemigroup
+  ; identity    = (λ _ → S.refl) , (λ _ → S.refl)
+  }
+
+∘-id-monoid : Monoid (c ⊔ e) (c ⊔ e)
+∘-id-monoid = record { isMonoid = ∘-id-isMonoid }
+
+private
+  ∘-rawMagma : RawMagma (c ⊔ e) (c ⊔ e)
+  ∘-rawMagma = Semigroup.rawMagma ∘-semigroup
+
+  ∘-id-rawMonoid : RawMonoid (c ⊔ e) (c ⊔ e)
+  ∘-id-rawMonoid = Monoid.rawMonoid ∘-id-monoid
+
+------------------------------------------------------------------------
+-- Homomorphism
+
+^-isMagmaHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isMagmaHomomorphism f = record
+  { isRelHomomorphism = record { cong = ^-cong₂ f }
+  ; homo = ^-homo f
+  }
+
+^-isMonoidHomomorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
+^-isMonoidHomomorphism f = record
+  { isMagmaHomomorphism = record
+    { isRelHomomorphism = record { cong = ^-cong₂ f }
+    ; homo = ^-homo f
+    }
+  ; ε-homo = S.refl
+  }
+
+------------------------------------------------------------------------
+-- Deprecations
+
+-- Version 2.1
+
+^-isSemigroupMorphism = ^-isMagmaHomomorphism
+{-# WARNING_ON_USAGE ^-isSemigroupMorphism
+"Warning: ^-isSemigroupMorphism was deprecated in v2.1.
+Please use ^-isMagmaHomomorphism instead."
+#-}
+
+^-isMonoidMorphism = ^-isMonoidHomomorphism
+{-# WARNING_ON_USAGE ^-isMonoidMorphism
+"Warning: ^-isMonoidMorphism was deprecated in v2.1.
+Please use ^-isMonoidHomomorphism instead."
+#-}

From b04ab5d9290fe030d96e33cbfa2274695bdfeff6 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Wed, 15 May 2024 22:51:07 -0400
Subject: [PATCH 13/19] fix tiny merge issue

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a560d089ef..3cdab80c9b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -256,7 +256,7 @@ Additions to existing modules
   ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x
   ```
 
- * In `Algebra.Properties.Group`:
+* In `Algebra.Properties.Group`:
   ```agda
   isQuasigroup    : IsQuasigroup _∙_ _\\_ _//_
   quasigroup      : Quasigroup _ _

From 60ecbeb823657a334445510bc3aa0a940afc43ef Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Wed, 22 May 2024 10:15:28 -0400
Subject: [PATCH 14/19] get deprecations right (remove where not needed, make
 more global where needed)

---
 src/Function/Endo/Propositional.agda         | 17 -----------------
 src/Function/Endo/Setoid.agda                | 17 -----------------
 src/Function/Endomorphism/Propositional.agda |  8 +++++---
 src/Function/Endomorphism/Setoid.agda        |  8 +++++---
 4 files changed, 10 insertions(+), 40 deletions(-)

diff --git a/src/Function/Endo/Propositional.agda b/src/Function/Endo/Propositional.agda
index d7b1f2c9f5..9a57c3f2ad 100644
--- a/src/Function/Endo/Propositional.agda
+++ b/src/Function/Endo/Propositional.agda
@@ -105,20 +105,3 @@ private
   { isMagmaHomomorphism = ^-isMagmaHomomorphism f
   ; ε-homo = refl
   }
-
-------------------------------------------------------------------------
--- Deprecations
-
--- Version 2.1
-
-^-isSemigroupMorphism = ^-isMagmaHomomorphism
-{-# WARNING_ON_USAGE ^-isSemigroupMorphism
-"Warning: ^-isSemigroupMorphism was deprecated in v2.1.
-Please use ^-isMagmaHomomorphism instead."
-#-}
-
-^-isMonoidMorphism = ^-isMonoidHomomorphism
-{-# WARNING_ON_USAGE ^-isMonoidMorphism
-"Warning: ^-isMonoidMorphism was deprecated in v2.1.
-Please use ^-isMonoidHomomorphism instead."
-#-}
diff --git a/src/Function/Endo/Setoid.agda b/src/Function/Endo/Setoid.agda
index 5a5b31337b..4f30411e75 100644
--- a/src/Function/Endo/Setoid.agda
+++ b/src/Function/Endo/Setoid.agda
@@ -109,20 +109,3 @@ private
     }
   ; ε-homo = S.refl
   }
-
-------------------------------------------------------------------------
--- Deprecations
-
--- Version 2.1
-
-^-isSemigroupMorphism = ^-isMagmaHomomorphism
-{-# WARNING_ON_USAGE ^-isSemigroupMorphism
-"Warning: ^-isSemigroupMorphism was deprecated in v2.1.
-Please use ^-isMagmaHomomorphism instead."
-#-}
-
-^-isMonoidMorphism = ^-isMonoidHomomorphism
-{-# WARNING_ON_USAGE ^-isMonoidMorphism
-"Warning: ^-isMonoidMorphism was deprecated in v2.1.
-Please use ^-isMonoidHomomorphism instead."
-#-}
diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda
index c8dd685328..8a3a6794eb 100644
--- a/src/Function/Endomorphism/Propositional.agda
+++ b/src/Function/Endomorphism/Propositional.agda
@@ -6,11 +6,13 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
--- Disabled to prevent warnings from deprecated names
-{-# OPTIONS --warn=noUserWarning #-}
-
 module Function.Endomorphism.Propositional {a} (A : Set a) where
 
+{-# WARNING_ON_IMPORT
+"Function.Endomorphism.Propositional was deprecated in v2.1.
+Use Function.Endo.Propositional instead."
+#-}
+
 open import Algebra
 open import Algebra.Morphism; open Definitions
 
diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda
index a715ef5262..80d3b71360 100644
--- a/src/Function/Endomorphism/Setoid.agda
+++ b/src/Function/Endomorphism/Setoid.agda
@@ -6,14 +6,16 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
--- Disabled to prevent warnings from deprecated names
-{-# OPTIONS --warn=noUserWarning #-}
-
 open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.Bundles using (Setoid)
 
 module Function.Endomorphism.Setoid {c e} (S : Setoid c e) where
 
+{-# WARNING_ON_IMPORT
+"Function.Endomorphism.Setoid was deprecated in v2.1.
+Use Function.Endo.Setoid instead."
+#-}
+
 open import Agda.Builtin.Equality
 
 open import Algebra

From 08c8866791ad8b1e7360181db118e947b7673aa1 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Wed, 22 May 2024 10:16:56 -0400
Subject: [PATCH 15/19] style guide - missing blank lines

---
 src/Function/Endo/Setoid.agda | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Function/Endo/Setoid.agda b/src/Function/Endo/Setoid.agda
index 4f30411e75..c10d4d293a 100644
--- a/src/Function/Endo/Setoid.agda
+++ b/src/Function/Endo/Setoid.agda
@@ -31,6 +31,8 @@ private
   open module E = Setoid (S ⇨ S) hiding (refl)
   module S = Setoid S
   open Func using (cong)
+
+
 ------------------------------------------------------------------------
 -- Basic type and functions
 

From e7d49614bb30faae15ae6bf66550bee76fd1fece Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Wed, 22 May 2024 10:20:52 -0400
Subject: [PATCH 16/19] fix a bad merge

---
 CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3cdab80c9b..0a32e781a8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -247,6 +247,11 @@ Additions to existing modules
 
 * In `Algebra.Morphism.Structures`:
   ```agda
+  module SuccessorSetMorphisms (N₁ : RawSuccessorSet a ℓ₁) (N₂ : RawSuccessorSet b ℓ₂) where
+    record IsSuccessorSetHomomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
+    record IsSuccessorSetMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
+    record IsSuccessorSetIsomorphism  (⟦_⟧ : N₁.Carrier →  N₂.Carrier) : Set _
+
   IsSemigroupHomomorphism : (A → B) → Set _
   IsSemigroupMonomorphism : (A → B) → Set _
   IsSemigroupIsomorphism : (A → B) → Set _

From b28f62d1d43a39b8ff3e428a81dd5e73e00c069d Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 25 May 2024 16:51:10 +0100
Subject: [PATCH 17/19] fixed deprecations

---
 src/Function/Endo/Propositional.agda         | 1 +
 src/Function/Endo/Setoid.agda                | 7 ++-----
 src/Function/Endomorphism/Propositional.agda | 2 +-
 src/Function/Endomorphism/Setoid.agda        | 2 +-
 src/Function/Equality.agda                   | 1 -
 5 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/src/Function/Endo/Propositional.agda b/src/Function/Endo/Propositional.agda
index 9a57c3f2ad..6d2e8a2204 100644
--- a/src/Function/Endo/Propositional.agda
+++ b/src/Function/Endo/Propositional.agda
@@ -5,6 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
+
 module Function.Endo.Propositional {a} (A : Set a) where
 
 open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
diff --git a/src/Function/Endo/Setoid.agda b/src/Function/Endo/Setoid.agda
index c10d4d293a..cd36f2028f 100644
--- a/src/Function/Endo/Setoid.agda
+++ b/src/Function/Endo/Setoid.agda
@@ -53,7 +53,7 @@ f ^ suc n = f ∘ (f ^ n)
 ^-cong₂ f {n} refl = cong (f ^ n) S.refl
 
 ^-homo : ∀ f → Homomorphic₂ ℕ Endo _≈_ (f ^_) _+_ _∘_
-^-homo f zero    n           = S.refl
+^-homo f zero    n       = S.refl
 ^-homo f (suc m) zero    = ^-cong₂ f (+-identityʳ m)
 ^-homo f (suc m) (suc n) = ^-homo f m (suc n)
 
@@ -105,9 +105,6 @@ private
 
 ^-isMonoidHomomorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
 ^-isMonoidHomomorphism f = record
-  { isMagmaHomomorphism = record
-    { isRelHomomorphism = record { cong = ^-cong₂ f }
-    ; homo = ^-homo f
-    }
+  { isMagmaHomomorphism = ^-isMagmaHomomorphism f
   ; ε-homo = S.refl
   }
diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda
index 8a3a6794eb..7f9d99a155 100644
--- a/src/Function/Endomorphism/Propositional.agda
+++ b/src/Function/Endomorphism/Propositional.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Endomorphisms on a Set
+-- This module is DEPRECATED.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda
index 80d3b71360..5d4993ecf6 100644
--- a/src/Function/Endomorphism/Setoid.agda
+++ b/src/Function/Endomorphism/Setoid.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Endomorphisms on a Setoid
+-- This module is DEPRECATED.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
diff --git a/src/Function/Equality.agda b/src/Function/Equality.agda
index 647dca7416..4748834a83 100644
--- a/src/Function/Equality.agda
+++ b/src/Function/Equality.agda
@@ -5,7 +5,6 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-}
 
 module Function.Equality where
 

From 278547ab5f3a36bbf2bbd114fc18f30187eab77c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 5 Jun 2024 14:44:06 +0100
Subject: [PATCH 18/19] fix #2394

---
 src/Function/Endo/Propositional.agda | 79 ++++++++++++++++------------
 src/Function/Endo/Setoid.agda        | 65 +++++++++++++----------
 2 files changed, 82 insertions(+), 62 deletions(-)

diff --git a/src/Function/Endo/Propositional.agda b/src/Function/Endo/Propositional.agda
index 6d2e8a2204..2305db5452 100644
--- a/src/Function/Endo/Propositional.agda
+++ b/src/Function/Endo/Propositional.agda
@@ -10,6 +10,8 @@ module Function.Endo.Propositional {a} (A : Set a) where
 
 open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
 open import Algebra.Core
+import Algebra.Definitions.RawMonoid as RawMonoidDefinitions
+import Algebra.Properties.Monoid.Mult as MonoidMultProperties
 open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
 open import Algebra.Morphism
   using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
@@ -19,7 +21,7 @@ open import Data.Nat.Base using (ℕ; zero; suc; _+_; +-rawMagma; +-0-rawMonoid)
 open import Data.Nat.Properties using (+-0-monoid; +-semigroup)
 open import Data.Product.Base using (_,_)
 
-open import Function.Base using (id; _∘′_; _∋_)
+open import Function.Base using (id; _∘′_; _∋_; flip)
 open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
 open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
@@ -27,9 +29,25 @@ import Relation.Binary.PropositionalEquality.Properties as ≡
 
 import Function.Endo.Setoid (≡.setoid A) as Setoid
 
+------------------------------------------------------------------------
+-- Basic type and raw bundles
+
 Endo : Set a
 Endo = A → A
 
+private
+
+  _∘_ : Op₂ Endo
+  _∘_ = _∘′_
+
+  ∘-id-rawMonoid : RawMonoid a a
+  ∘-id-rawMonoid = record { Carrier = Endo; _≈_ = _≡_ ; _∙_ = _∘_ ; ε = id }
+
+  open RawMonoid ∘-id-rawMonoid
+    using ()
+    renaming (rawMagma to ∘-rawMagma)
+
+
 ------------------------------------------------------------------------
 -- Conversion back and forth with the Setoid-based notion of Endomorphism
 
@@ -42,32 +60,19 @@ toSetoidEndo f = record
   ; cong  = cong f
   }
 
-------------------------------------------------------------------------
--- N-th composition
-
-infixr 8 _^_
-
-_^_ : Endo → ℕ → Endo
-f ^ zero  = id
-f ^ suc n = f ∘′ (f ^ n)
-
-^-homo : ∀ f → Homomorphic₂ ℕ Endo _≡_ (f ^_) _+_ _∘′_
-^-homo f zero    n = refl
-^-homo f (suc m) n = cong (f ∘′_) (^-homo f m n)
-
 ------------------------------------------------------------------------
 -- Structures
 
-∘-isMagma : IsMagma _≡_ (Op₂ Endo ∋ _∘′_)
+∘-isMagma : IsMagma _≡_ _∘_
 ∘-isMagma = record
   { isEquivalence = ≡.isEquivalence
-  ; ∙-cong        = cong₂ _∘′_
+  ; ∙-cong        = cong₂ _∘_
   }
 
 ∘-magma : Magma _ _
 ∘-magma = record { isMagma = ∘-isMagma }
 
-∘-isSemigroup : IsSemigroup _≡_ (Op₂ Endo ∋ _∘′_)
+∘-isSemigroup : IsSemigroup _≡_ _∘_
 ∘-isSemigroup = record
   { isMagma = ∘-isMagma
   ; assoc   = λ _ _ _ → refl
@@ -76,7 +81,7 @@ f ^ suc n = f ∘′ (f ^ n)
 ∘-semigroup : Semigroup _ _
 ∘-semigroup = record { isSemigroup = ∘-isSemigroup }
 
-∘-id-isMonoid : IsMonoid _≡_ _∘′_ id
+∘-id-isMonoid : IsMonoid _≡_ _∘_ id
 ∘-id-isMonoid = record
   { isSemigroup = ∘-isSemigroup
   ; identity    = (λ _ → refl) , (λ _ → refl)
@@ -85,24 +90,32 @@ f ^ suc n = f ∘′ (f ^ n)
 ∘-id-monoid : Monoid _ _
 ∘-id-monoid = record { isMonoid = ∘-id-isMonoid }
 
-private
-  ∘-rawMagma : RawMagma a a
-  ∘-rawMagma = Semigroup.rawMagma ∘-semigroup
+------------------------------------------------------------------------
+-- n-th iterated composition
 
-  ∘-id-rawMonoid : RawMonoid a a
-  ∘-id-rawMonoid = Monoid.rawMonoid ∘-id-monoid
+infixr 8 _^_
+
+_^_ : Endo → ℕ → Endo
+_^_ = flip _×_ where open RawMonoidDefinitions ∘-id-rawMonoid
 
 ------------------------------------------------------------------------
 -- Homomorphism
 
-^-isMagmaHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
-^-isMagmaHomomorphism f = record
-  { isRelHomomorphism = record { cong = cong (f ^_) }
-  ; homo = ^-homo f
-  }
+module _ (f : Endo) where
 
-^-isMonoidHomomorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
-^-isMonoidHomomorphism f = record
-  { isMagmaHomomorphism = ^-isMagmaHomomorphism f
-  ; ε-homo = refl
-  }
+  open MonoidMultProperties ∘-id-monoid
+
+  ^-homo : Homomorphic₂ ℕ Endo _≡_ (f ^_) _+_ _∘_
+  ^-homo = ×-homo-+ f
+
+  ^-isMagmaHomomorphism : IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+  ^-isMagmaHomomorphism = record
+    { isRelHomomorphism = record { cong = cong (f ^_) }
+    ; homo = ^-homo
+    }
+
+  ^-isMonoidHomomorphism : IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
+  ^-isMonoidHomomorphism = record
+    { isMagmaHomomorphism = ^-isMagmaHomomorphism
+    ; ε-homo = refl
+    }
diff --git a/src/Function/Endo/Setoid.agda b/src/Function/Endo/Setoid.agda
index cd36f2028f..ffe8273943 100644
--- a/src/Function/Endo/Setoid.agda
+++ b/src/Function/Endo/Setoid.agda
@@ -13,6 +13,8 @@ module Function.Endo.Setoid {c e} (S : Setoid c e) where
 open import Agda.Builtin.Equality
 
 open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
+import Algebra.Definitions.RawMonoid as RawMonoidDefinitions
+import Algebra.Properties.Monoid.Mult as MonoidMultProperties
 open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
 open import Algebra.Morphism
   using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
@@ -34,30 +36,23 @@ private
 
 
 ------------------------------------------------------------------------
--- Basic type and functions
+-- Basic type and raw bundles
 
 Endo : Set _
 Endo = S ⟶ₛ S
 
-infixr 8 _^_
-
 private
   id : Endo
   id = identity S
 
-_^_ : Endo → ℕ → Endo
-f ^ zero  = id
-f ^ suc n = f ∘ (f ^ n)
-
-^-cong₂ : ∀ f → (f ^_) Preserves _≡_ ⟶ _≈_
-^-cong₂ f {n} refl = cong (f ^ n) S.refl
+  ∘-id-rawMonoid : RawMonoid (c ⊔ e) (c ⊔ e)
+  ∘-id-rawMonoid = record { Carrier = Endo; _≈_ = _≈_ ; _∙_ = _∘_ ; ε = id }
 
-^-homo : ∀ f → Homomorphic₂ ℕ Endo _≈_ (f ^_) _+_ _∘_
-^-homo f zero    n       = S.refl
-^-homo f (suc m) zero    = ^-cong₂ f (+-identityʳ m)
-^-homo f (suc m) (suc n) = ^-homo f m (suc n)
+  open RawMonoid ∘-id-rawMonoid
+    using ()
+    renaming (rawMagma to ∘-rawMagma)
 
-------------------------------------------------------------------------
+--------------------------------------------------------------
 -- Structures
 
 ∘-isMagma : IsMagma _≈_ _∘_
@@ -87,24 +82,36 @@ f ^ suc n = f ∘ (f ^ n)
 ∘-id-monoid : Monoid (c ⊔ e) (c ⊔ e)
 ∘-id-monoid = record { isMonoid = ∘-id-isMonoid }
 
-private
-  ∘-rawMagma : RawMagma (c ⊔ e) (c ⊔ e)
-  ∘-rawMagma = Semigroup.rawMagma ∘-semigroup
+------------------------------------------------------------------------
+-- -- n-th iterated composition
 
-  ∘-id-rawMonoid : RawMonoid (c ⊔ e) (c ⊔ e)
-  ∘-id-rawMonoid = Monoid.rawMonoid ∘-id-monoid
+infixr 8 _^_
+
+_^_ : Endo → ℕ → Endo
+f ^ n = n × f where open RawMonoidDefinitions ∘-id-rawMonoid
 
 ------------------------------------------------------------------------
 -- Homomorphism
 
-^-isMagmaHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
-^-isMagmaHomomorphism f = record
-  { isRelHomomorphism = record { cong = ^-cong₂ f }
-  ; homo = ^-homo f
-  }
+module _ (f : Endo) where
+
+  open MonoidMultProperties ∘-id-monoid
+
+  ^-cong₂ : (f ^_) Preserves _≡_ ⟶ _≈_
+  ^-cong₂ = ×-congˡ {f}
+
+  ^-homo : Homomorphic₂ ℕ Endo _≈_ (f ^_) _+_ _∘_
+  ^-homo = ×-homo-+ f
+
+  ^-isMagmaHomomorphism : IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+  ^-isMagmaHomomorphism = record
+    { isRelHomomorphism = record { cong = ^-cong₂ }
+    ; homo = ^-homo
+    }
+
+  ^-isMonoidHomomorphism : IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
+  ^-isMonoidHomomorphism = record
+    { isMagmaHomomorphism = ^-isMagmaHomomorphism
+    ; ε-homo = S.refl
+    }
 
-^-isMonoidHomomorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
-^-isMonoidHomomorphism f = record
-  { isMagmaHomomorphism = ^-isMagmaHomomorphism f
-  ; ε-homo = S.refl
-  }

From c71cb837bc8bf6e6daca697c662867aebd883f68 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Thu, 6 Jun 2024 22:07:37 -0400
Subject: [PATCH 19/19] minor tweaks

---
 src/Function/Endo/Propositional.agda | 4 ++--
 src/Function/Endo/Setoid.agda        | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Function/Endo/Propositional.agda b/src/Function/Endo/Propositional.agda
index 2305db5452..4d1bb21cbb 100644
--- a/src/Function/Endo/Propositional.agda
+++ b/src/Function/Endo/Propositional.agda
@@ -96,14 +96,14 @@ toSetoidEndo f = record
 infixr 8 _^_
 
 _^_ : Endo → ℕ → Endo
-_^_ = flip _×_ where open RawMonoidDefinitions ∘-id-rawMonoid
+_^_ = flip _×_ where open RawMonoidDefinitions ∘-id-rawMonoid using (_×_)
 
 ------------------------------------------------------------------------
 -- Homomorphism
 
 module _ (f : Endo) where
 
-  open MonoidMultProperties ∘-id-monoid
+  open MonoidMultProperties ∘-id-monoid using (×-homo-+)
 
   ^-homo : Homomorphic₂ ℕ Endo _≡_ (f ^_) _+_ _∘_
   ^-homo = ×-homo-+ f
diff --git a/src/Function/Endo/Setoid.agda b/src/Function/Endo/Setoid.agda
index ffe8273943..99716b35db 100644
--- a/src/Function/Endo/Setoid.agda
+++ b/src/Function/Endo/Setoid.agda
@@ -10,7 +10,7 @@ open import Relation.Binary.Bundles using (Setoid)
 
 module Function.Endo.Setoid {c e} (S : Setoid c e) where
 
-open import Agda.Builtin.Equality
+open import Agda.Builtin.Equality using (_≡_)
 
 open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
 import Algebra.Definitions.RawMonoid as RawMonoidDefinitions
@@ -88,14 +88,14 @@ private
 infixr 8 _^_
 
 _^_ : Endo → ℕ → Endo
-f ^ n = n × f where open RawMonoidDefinitions ∘-id-rawMonoid
+f ^ n = n × f where open RawMonoidDefinitions ∘-id-rawMonoid using (_×_)
 
 ------------------------------------------------------------------------
 -- Homomorphism
 
 module _ (f : Endo) where
 
-  open MonoidMultProperties ∘-id-monoid
+  open MonoidMultProperties ∘-id-monoid using (×-congˡ; ×-homo-+)
 
   ^-cong₂ : (f ^_) Preserves _≡_ ⟶ _≈_
   ^-cong₂ = ×-congˡ {f}