fix things as per Matthew's review - though this remains a breaking c…

…hange.
agda · Apr 4, 2024 · d1cae72 · d1cae72
1 parent e1e7c57
commit d1cae72
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 22 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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