fixes agda#2458

jamesmckinna · jamesmckinna · commit 9d310abfec62 · 2024-08-29T12:42:56.000+01:00
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -24,6 +24,11 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Algebra.Morphism.Structures`:
+  ```agda
+  homo  ↦  ∙-homo
+  ```
+
 * In `Data.Vec.Properties`:
   ```agda
   ++-assoc _      ↦  ++-assoc-eqFree
diff --git a/src/Algebra/Lattice/Morphism/Structures.agda b/src/Algebra/Lattice/Morphism/Structures.agda
@@ -58,13 +58,13 @@ module LatticeMorphisms (L₁ : RawLattice a ℓ₁) (L₂ : RawLattice b ℓ₂
     ∧-isMagmaHomomorphism : ∧.IsMagmaHomomorphism ⟦_⟧
     ∧-isMagmaHomomorphism = record
       { isRelHomomorphism = isRelHomomorphism
-      ; homo = ∧-homo
+      ; ∙-homo = ∧-homo
       }
 
     ∨-isMagmaHomomorphism : ∨.IsMagmaHomomorphism ⟦_⟧
     ∨-isMagmaHomomorphism = record
       { isRelHomomorphism = isRelHomomorphism
-      ; homo = ∨-homo
+      ; ∙-homo = ∨-homo
       }
 
   record IsLatticeMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
diff --git a/src/Algebra/Morphism/Construct/Initial.agda b/src/Algebra/Morphism/Construct/Initial.agda
@@ -51,7 +51,7 @@ isMagmaHomomorphism : (M : RawMagma m ℓm) →
                       IsMagmaHomomorphism rawMagma M zero
 isMagmaHomomorphism M = record
   { isRelHomomorphism = record { cong = cong (RawMagma._≈_ M) }
-  ; homo = λ()
+  ; ∙-homo = λ()
   }
 
 isMagmaMonomorphism : (M : RawMagma m ℓm) →
diff --git a/src/Algebra/Morphism/Construct/Terminal.agda b/src/Algebra/Morphism/Construct/Terminal.agda
@@ -50,7 +50,7 @@ isMagmaHomomorphism : (M : RawMagma a ℓa) →
                       IsMagmaHomomorphism M rawMagma one
 isMagmaHomomorphism M = record
   { isRelHomomorphism = record { cong = _ }
-  ; homo = _
+  ; ∙-homo = _
   }
 
 isMonoidHomomorphism : (M : RawMonoid a ℓa) →
diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda
@@ -83,7 +83,14 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher
   record IsMagmaHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
-      homo              : Homomorphic₂ ⟦_⟧ _∙_ _◦_
+      ∙-homo              : Homomorphic₂ ⟦_⟧ _∙_ _◦_
+
+      -- Deprecated.
+    homo = ∙-homo
+    {-# WARNING_ON_USAGE homo
+    "Warning: homo was deprecated in v2.2.
+    Please use ∙-homo instead. "
+    #-}
 
     open IsRelHomomorphism isRelHomomorphism public
       renaming (cong to ⟦⟧-cong)
@@ -200,7 +207,6 @@ module GroupMorphisms (G₁ : RawGroup a ℓ₁) (G₂ : RawGroup b ℓ₂) wher
       injective           : Injective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsGroupHomomorphism isGroupHomomorphism public
-      renaming (homo to ∙-homo)
 
     isMonoidMonomorphism : IsMonoidMonomorphism ⟦_⟧
     isMonoidMonomorphism = record
@@ -265,7 +271,7 @@ module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSe
     *-isMagmaHomomorphism : *.IsMagmaHomomorphism ⟦_⟧
     *-isMagmaHomomorphism = record
       { isRelHomomorphism = isRelHomomorphism
-      ; homo = *-homo
+      ; ∙-homo = *-homo
       }
 
   record IsNearSemiringMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -430,7 +436,7 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi
     *-isMagmaHomomorphism : *.IsMagmaHomomorphism ⟦_⟧
     *-isMagmaHomomorphism = record
       { isRelHomomorphism = isRelHomomorphism
-      ; homo = *-homo
+      ; ∙-homo = *-homo
       }
 
   record IsRingWithoutOneMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -623,19 +629,19 @@ module QuasigroupMorphisms (Q₁ : RawQuasigroup a ℓ₁) (Q₂ : RawQuasigroup
     ∙-isMagmaHomomorphism : ∙.IsMagmaHomomorphism ⟦_⟧
     ∙-isMagmaHomomorphism = record
       { isRelHomomorphism = isRelHomomorphism
-      ; homo = ∙-homo
+      ; ∙-homo = ∙-homo
       }
 
     \\-isMagmaHomomorphism : \\.IsMagmaHomomorphism ⟦_⟧
     \\-isMagmaHomomorphism = record
       { isRelHomomorphism  = isRelHomomorphism
-      ; homo = \\-homo
+      ; ∙-homo = \\-homo
       }
 
     //-isMagmaHomomorphism : //.IsMagmaHomomorphism ⟦_⟧
     //-isMagmaHomomorphism = record
       { isRelHomomorphism  = isRelHomomorphism
-      ; homo = //-homo
+      ; ∙-homo = //-homo
       }
 
   record IsQuasigroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
@@ -229,7 +229,7 @@ module _ (A : Set a) where
     { isRelHomomorphism = record
       { cong = cong length
       }
-    ; homo = λ xs ys → length-++ xs {ys}
+    ; ∙-homo = λ xs ys → length-++ xs {ys}
     }
 
   length-isMonoidHomomorphism : IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length
diff --git a/src/Data/Parity/Properties.agda b/src/Data/Parity/Properties.agda
@@ -422,7 +422,7 @@ toSign-isMagmaHomomorphism : IsMagmaHomomorphism ℙ.+-rawMagma 𝕊.*-rawMagma
 toSign-isMagmaHomomorphism = record
   { isRelHomomorphism = record
     { cong = cong toSign }
-  ; homo = +-homo-*
+  ; ∙-homo = +-homo-*
   }
 
 toSign-isMagmaMonomorphism : IsMagmaMonomorphism ℙ.+-rawMagma 𝕊.*-rawMagma toSign
@@ -532,7 +532,7 @@ parity-isMagmaHomomorphism : IsMagmaHomomorphism ℕ.+-rawMagma ℙ.+-rawMagma p
 parity-isMagmaHomomorphism = record
   { isRelHomomorphism = record
     { cong = cong parity }
-  ; homo = +-homo-+
+  ; ∙-homo = +-homo-+
   }
 
 parity-isMonoidHomomorphism : IsMonoidHomomorphism ℕ.+-0-rawMonoid ℙ.+-0-rawMonoid parity
diff --git a/src/Function/Endo/Propositional.agda b/src/Function/Endo/Propositional.agda
@@ -111,7 +111,7 @@ module _ (f : Endo) where
   ^-isMagmaHomomorphism : IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
   ^-isMagmaHomomorphism = record
     { isRelHomomorphism = record { cong = cong (f ^_) }
-    ; homo = ^-homo
+    ; ∙-homo = ^-homo
     }
 
   ^-isMonoidHomomorphism : IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
diff --git a/src/Function/Endo/Setoid.agda b/src/Function/Endo/Setoid.agda
@@ -106,7 +106,7 @@ module _ (f : Endo) where
   ^-isMagmaHomomorphism : IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
   ^-isMagmaHomomorphism = record
     { isRelHomomorphism = record { cong = ^-cong₂ }
-    ; homo = ^-homo
+    ; ∙-homo = ^-homo
     }
 
   ^-isMonoidHomomorphism : IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)

Original file line number	Diff line number	Diff line change
`@@ -58,13 +58,13 @@ module LatticeMorphisms (L₁ : RawLattice a ℓ₁) (L₂ : RawLattice b ℓ₂`
`58`	`58`	`∧-isMagmaHomomorphism : ∧.IsMagmaHomomorphism ⟦_⟧`
`59`	`59`	`∧-isMagmaHomomorphism = record`
`60`	`60`	`{ isRelHomomorphism = isRelHomomorphism`
`61`		`- ; homo = ∧-homo`
	`61`	`+ ; ∙-homo = ∧-homo`
`62`	`62`	`}`
`63`	`63`
`64`	`64`	`∨-isMagmaHomomorphism : ∨.IsMagmaHomomorphism ⟦_⟧`
`65`	`65`	`∨-isMagmaHomomorphism = record`
`66`	`66`	`{ isRelHomomorphism = isRelHomomorphism`
`67`		`- ; homo = ∨-homo`
	`67`	`+ ; ∙-homo = ∨-homo`
`68`	`68`	`}`
`69`	`69`
`70`	`70`	`record IsLatticeMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where`
Original file line number	Diff line number	Diff line change
`@@ -51,7 +51,7 @@ isMagmaHomomorphism : (M : RawMagma m ℓm) →`
`51`	`51`	`IsMagmaHomomorphism rawMagma M zero`
`52`	`52`	`isMagmaHomomorphism M = record`
`53`	`53`	`{ isRelHomomorphism = record { cong = cong (RawMagma._≈_ M) }`
`54`		`- ; homo = λ()`
	`54`	`+ ; ∙-homo = λ()`
`55`	`55`	`}`
`56`	`56`
`57`	`57`	`isMagmaMonomorphism : (M : RawMagma m ℓm) →`
Original file line number	Diff line number	Diff line change
`@@ -50,7 +50,7 @@ isMagmaHomomorphism : (M : RawMagma a ℓa) →`
`50`	`50`	`IsMagmaHomomorphism M rawMagma one`
`51`	`51`	`isMagmaHomomorphism M = record`
`52`	`52`	`{ isRelHomomorphism = record { cong = _ }`
`53`		`- ; homo = _`
	`53`	`+ ; ∙-homo = _`
`54`	`54`	`}`
`55`	`55`
`56`	`56`	`isMonoidHomomorphism : (M : RawMonoid a ℓa) →`
Original file line number	Diff line number	Diff line change
`@@ -229,7 +229,7 @@ module _ (A : Set a) where`
`229`	`229`	`{ isRelHomomorphism = record`
`230`	`230`	`{ cong = cong length`
`231`	`231`	`}`
`232`		`- ; homo = λ xs ys → length-++ xs {ys}`
	`232`	`+ ; ∙-homo = λ xs ys → length-++ xs {ys}`
`233`	`233`	`}`
`234`	`234`
`235`	`235`	`length-isMonoidHomomorphism : IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length`
Original file line number	Diff line number	Diff line change
`@@ -111,7 +111,7 @@ module _ (f : Endo) where`
`111`	`111`	`^-isMagmaHomomorphism : IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)`
`112`	`112`	`^-isMagmaHomomorphism = record`
`113`	`113`	`{ isRelHomomorphism = record { cong = cong (f ^_) }`
`114`		`- ; homo = ^-homo`
	`114`	`+ ; ∙-homo = ^-homo`
`115`	`115`	`}`
`116`	`116`
`117`	`117`	`^-isMonoidHomomorphism : IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)`
Original file line number	Diff line number	Diff line change
`@@ -106,7 +106,7 @@ module _ (f : Endo) where`
`106`	`106`	`^-isMagmaHomomorphism : IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)`
`107`	`107`	`^-isMagmaHomomorphism = record`
`108`	`108`	`{ isRelHomomorphism = record { cong = ^-cong₂ }`
`109`		`- ; homo = ^-homo`
	`109`	`+ ; ∙-homo = ^-homo`
`110`	`110`	`}`
`111`	`111`
`112`	`112`	`^-isMonoidHomomorphism : IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)`