From 9d310abfec62842cae6ac082ca6a4e32d1d6baa9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 29 Aug 2024 12:42:56 +0100 Subject: [PATCH 01/12] fixes #2458 --- CHANGELOG.md | 5 +++++ src/Algebra/Lattice/Morphism/Structures.agda | 4 ++-- src/Algebra/Morphism/Construct/Initial.agda | 2 +- src/Algebra/Morphism/Construct/Terminal.agda | 2 +- src/Algebra/Morphism/Structures.agda | 20 +++++++++++++------- src/Data/List/Properties.agda | 2 +- src/Data/Parity/Properties.agda | 4 ++-- src/Function/Endo/Propositional.agda | 2 +- src/Function/Endo/Setoid.agda | 2 +- 9 files changed, 27 insertions(+), 16 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 57222329ef..3401eed61b 100644 --- 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 index 87cf92e616..80c84eb721 100644 --- 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 index 883b70109d..5e7d798de7 100644 --- 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 index 227ebf2887..fa35e03c47 100644 --- 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 index c352904be7..ed9c7cffed 100644 --- 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 index f847d8a059..938c508093 100644 --- 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 index ebca1ef000..1b95a1cce7 100644 --- 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 index 4d1bb21cbb..8d014234f6 100644 --- 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 index 583ba2f4c6..414e74a532 100644 --- 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 ^_) From 30c2880656d8b1c5b926fa2c8103f8eba148b558 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 29 Aug 2024 13:20:49 +0100 Subject: [PATCH 02/12] caught two missing uses --- src/Algebra/Morphism/Construct/Composition.agda | 2 +- src/Algebra/Morphism/Construct/Identity.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Morphism/Construct/Composition.agda b/src/Algebra/Morphism/Construct/Composition.agda index 17d5f2798b..103c999ced 100644 --- a/src/Algebra/Morphism/Construct/Composition.agda +++ b/src/Algebra/Morphism/Construct/Composition.agda @@ -38,7 +38,7 @@ module _ {M₁ : RawMagma a ℓ₁} → IsMagmaHomomorphism M₁ M₃ (g ∘ f) isMagmaHomomorphism f-homo g-homo = record { isRelHomomorphism = isRelHomomorphism F.isRelHomomorphism G.isRelHomomorphism - ; homo = λ x y → ≈₃-trans (G.⟦⟧-cong (F.homo x y)) (G.homo (f x) (f y)) + ; ∙-homo = λ x y → ≈₃-trans (G.⟦⟧-cong (F.homo x y)) (G.homo (f x) (f y)) } where module F = IsMagmaHomomorphism f-homo; module G = IsMagmaHomomorphism g-homo isMagmaMonomorphism diff --git a/src/Algebra/Morphism/Construct/Identity.agda b/src/Algebra/Morphism/Construct/Identity.agda index 881a8cf15c..32ca38ce7c 100644 --- a/src/Algebra/Morphism/Construct/Identity.agda +++ b/src/Algebra/Morphism/Construct/Identity.agda @@ -41,7 +41,7 @@ module _ (M : RawMagma c ℓ) (open RawMagma M) (refl : Reflexive _≈_) where isMagmaHomomorphism : IsMagmaHomomorphism id isMagmaHomomorphism = record { isRelHomomorphism = isRelHomomorphism _ - ; homo = λ _ _ → refl + ; ∙-homo = λ _ _ → refl } isMagmaMonomorphism : IsMagmaMonomorphism id From bb5520615ad59ff1ba9b2bcd67c7448c736085bb Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 29 Aug 2024 13:36:53 +0100 Subject: [PATCH 03/12] caught two more missing uses --- src/Data/Integer/Properties.agda | 2 +- src/Data/Rational/Properties.agda | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index f89d3164f6..5f3dc03433 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -1645,7 +1645,7 @@ i*j≢0 i j rewrite abs-* i j = ℕ.m*n≢0 ∣ i ∣ ∣ j ∣ ^-isMagmaHomomorphism : ∀ i → Morphism.IsMagmaHomomorphism ℕ.+-rawMagma *-rawMagma (i ^_) ^-isMagmaHomomorphism i = record { isRelHomomorphism = record { cong = cong (i ^_) } - ; homo = ^-distribˡ-+-* i + ; ∙-homo = ^-distribˡ-+-* i } ^-isMonoidHomomorphism : ∀ i → Morphism.IsMonoidHomomorphism ℕ.+-0-rawMonoid *-1-rawMonoid (i ^_) diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index fb186be08d..92224d4a4f 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -870,7 +870,7 @@ toℚᵘ-homo-+ p@record{} q@record{} with +-nf p q ℤ.≟ 0ℤ toℚᵘ-isMagmaHomomorphism-+ : IsMagmaHomomorphism +-rawMagma ℚᵘ.+-rawMagma toℚᵘ toℚᵘ-isMagmaHomomorphism-+ = record { isRelHomomorphism = toℚᵘ-isRelHomomorphism - ; homo = toℚᵘ-homo-+ + ; ∙-homo = toℚᵘ-homo-+ } toℚᵘ-isMonoidHomomorphism-+ : IsMonoidHomomorphism +-0-rawMonoid ℚᵘ.+-0-rawMonoid toℚᵘ @@ -1085,7 +1085,7 @@ toℚᵘ-homo-1/ (mkℚ -[1+ _ ] _ _) = ℚᵘ.≃-refl toℚᵘ-isMagmaHomomorphism-* : IsMagmaHomomorphism *-rawMagma ℚᵘ.*-rawMagma toℚᵘ toℚᵘ-isMagmaHomomorphism-* = record { isRelHomomorphism = toℚᵘ-isRelHomomorphism - ; homo = toℚᵘ-homo-* + ; ∙-homo = toℚᵘ-homo-* } toℚᵘ-isMonoidHomomorphism-* : IsMonoidHomomorphism *-1-rawMonoid ℚᵘ.*-1-rawMonoid toℚᵘ From f04ff440638a8cc311773d499a1e506bfb98ec39 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 29 Aug 2024 14:07:29 +0100 Subject: [PATCH 04/12] hopefully the last occurrences --- src/Algebra/Module/Morphism/Structures.agda | 10 +++--- src/Algebra/Morphism/MagmaMonomorphism.agda | 36 ++++++++++---------- src/Algebra/Morphism/MonoidMonomorphism.agda | 16 ++++----- src/Data/Nat/Binary/Properties.agda | 4 +-- 4 files changed, 33 insertions(+), 33 deletions(-) diff --git a/src/Algebra/Module/Morphism/Structures.agda b/src/Algebra/Module/Morphism/Structures.agda index e874f4d341..6dac17e22d 100644 --- a/src/Algebra/Module/Morphism/Structures.agda +++ b/src/Algebra/Module/Morphism/Structures.agda @@ -35,7 +35,7 @@ module LeftSemimoduleMorphisms open IsMonoidHomomorphism +ᴹ-isMonoidHomomorphism public using (isRelHomomorphism; ⟦⟧-cong) - renaming (isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo) + renaming (isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; ∙-homo to +ᴹ-homo; ε-homo to 0ᴹ-homo) record IsLeftSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where field @@ -91,7 +91,7 @@ module LeftModuleMorphisms open IsGroupHomomorphism +ᴹ-isGroupHomomorphism public using (isRelHomomorphism; ⟦⟧-cong) renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism - ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo + ; ∙-homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo ) isLeftSemimoduleHomomorphism : IsLeftSemimoduleHomomorphism ⟦_⟧ @@ -162,7 +162,7 @@ module RightSemimoduleMorphisms open IsMonoidHomomorphism +ᴹ-isMonoidHomomorphism public using (isRelHomomorphism; ⟦⟧-cong) - renaming (isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo) + renaming (isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; ∙-homo to +ᴹ-homo; ε-homo to 0ᴹ-homo) record IsRightSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where field @@ -218,7 +218,7 @@ module RightModuleMorphisms open IsGroupHomomorphism +ᴹ-isGroupHomomorphism public using (isRelHomomorphism; ⟦⟧-cong) renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism - ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo + ; ∙-homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo ) isRightSemimoduleHomomorphism : IsRightSemimoduleHomomorphism ⟦_⟧ isRightSemimoduleHomomorphism = record @@ -375,7 +375,7 @@ module BimoduleMorphisms open IsGroupHomomorphism +ᴹ-isGroupHomomorphism public using (isRelHomomorphism; ⟦⟧-cong) renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism - ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo + ; ∙-homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo ) isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism ⟦_⟧ diff --git a/src/Algebra/Morphism/MagmaMonomorphism.agda b/src/Algebra/Morphism/MagmaMonomorphism.agda index fbe08a5861..88bc6171d1 100644 --- a/src/Algebra/Morphism/MagmaMonomorphism.agda +++ b/src/Algebra/Morphism/MagmaMonomorphism.agda @@ -40,56 +40,56 @@ module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where cong : Congruent₂ _≈₁_ _∙_ cong {x} {y} {u} {v} x≈y u≈v = injective (begin - ⟦ x ∙ u ⟧ ≈⟨ homo x u ⟩ - ⟦ x ⟧ ◦ ⟦ u ⟧ ≈⟨ ◦-cong (⟦⟧-cong x≈y) (⟦⟧-cong u≈v) ⟩ - ⟦ y ⟧ ◦ ⟦ v ⟧ ≈⟨ homo y v ⟨ + ⟦ x ∙ u ⟧ ≈⟨ ∙-homo x u ⟩ + ⟦ x ⟧ ◦ ⟦ u ⟧ ≈⟨ ◦-cong (⟦⟧-cong x≈y) (⟦⟧-cong u≈v) ⟩ + ⟦ y ⟧ ◦ ⟦ v ⟧ ≈⟨ ∙-homo y v ⟨ ⟦ y ∙ v ⟧ ∎) assoc : Associative _≈₂_ _◦_ → Associative _≈₁_ _∙_ assoc assoc x y z = injective (begin - ⟦ (x ∙ y) ∙ z ⟧ ≈⟨ homo (x ∙ y) z ⟩ - ⟦ x ∙ y ⟧ ◦ ⟦ z ⟧ ≈⟨ ◦-cong (homo x y) refl ⟩ - (⟦ x ⟧ ◦ ⟦ y ⟧) ◦ ⟦ z ⟧ ≈⟨ assoc ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ ⟩ + ⟦ (x ∙ y) ∙ z ⟧ ≈⟨ ∙-homo (x ∙ y) z ⟩ + ⟦ x ∙ y ⟧ ◦ ⟦ z ⟧ ≈⟨ ◦-cong (∙-homo x y) refl ⟩ + (⟦ x ⟧ ◦ ⟦ y ⟧) ◦ ⟦ z ⟧ ≈⟨ assoc ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ ⟩ ⟦ x ⟧ ◦ (⟦ y ⟧ ◦ ⟦ z ⟧) ≈⟨ ◦-cong refl (homo y z) ⟨ - ⟦ x ⟧ ◦ ⟦ y ∙ z ⟧ ≈⟨ homo x (y ∙ z) ⟨ + ⟦ x ⟧ ◦ ⟦ y ∙ z ⟧ ≈⟨ ∙-homo x (y ∙ z) ⟨ ⟦ x ∙ (y ∙ z) ⟧ ∎) comm : Commutative _≈₂_ _◦_ → Commutative _≈₁_ _∙_ comm comm x y = injective (begin - ⟦ x ∙ y ⟧ ≈⟨ homo x y ⟩ - ⟦ x ⟧ ◦ ⟦ y ⟧ ≈⟨ comm ⟦ x ⟧ ⟦ y ⟧ ⟩ - ⟦ y ⟧ ◦ ⟦ x ⟧ ≈⟨ homo y x ⟨ + ⟦ x ∙ y ⟧ ≈⟨ ∙-homo x y ⟩ + ⟦ x ⟧ ◦ ⟦ y ⟧ ≈⟨ comm ⟦ x ⟧ ⟦ y ⟧ ⟩ + ⟦ y ⟧ ◦ ⟦ x ⟧ ≈⟨ ∙-homo y x ⟨ ⟦ y ∙ x ⟧ ∎) idem : Idempotent _≈₂_ _◦_ → Idempotent _≈₁_ _∙_ idem idem x = injective (begin - ⟦ x ∙ x ⟧ ≈⟨ homo x x ⟩ + ⟦ x ∙ x ⟧ ≈⟨ ∙-homo x x ⟩ ⟦ x ⟧ ◦ ⟦ x ⟧ ≈⟨ idem ⟦ x ⟧ ⟩ ⟦ x ⟧ ∎) sel : Selective _≈₂_ _◦_ → Selective _≈₁_ _∙_ sel sel x y with sel ⟦ x ⟧ ⟦ y ⟧ ... | inj₁ x◦y≈x = inj₁ (injective (begin - ⟦ x ∙ y ⟧ ≈⟨ homo x y ⟩ + ⟦ x ∙ y ⟧ ≈⟨ ∙-homo x y ⟩ ⟦ x ⟧ ◦ ⟦ y ⟧ ≈⟨ x◦y≈x ⟩ ⟦ x ⟧ ∎)) ... | inj₂ x◦y≈y = inj₂ (injective (begin - ⟦ x ∙ y ⟧ ≈⟨ homo x y ⟩ + ⟦ x ∙ y ⟧ ≈⟨ ∙-homo x y ⟩ ⟦ x ⟧ ◦ ⟦ y ⟧ ≈⟨ x◦y≈y ⟩ ⟦ y ⟧ ∎)) cancelˡ : LeftCancellative _≈₂_ _◦_ → LeftCancellative _≈₁_ _∙_ cancelˡ cancelˡ x y z x∙y≈x∙z = injective (cancelˡ ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ (begin - ⟦ x ⟧ ◦ ⟦ y ⟧ ≈⟨ homo x y ⟨ + ⟦ x ⟧ ◦ ⟦ y ⟧ ≈⟨ ∙-homo x y ⟨ ⟦ x ∙ y ⟧ ≈⟨ ⟦⟧-cong x∙y≈x∙z ⟩ - ⟦ x ∙ z ⟧ ≈⟨ homo x z ⟩ + ⟦ x ∙ z ⟧ ≈⟨ ∙-homo x z ⟩ ⟦ x ⟧ ◦ ⟦ z ⟧ ∎)) cancelʳ : RightCancellative _≈₂_ _◦_ → RightCancellative _≈₁_ _∙_ cancelʳ cancelʳ x y z y∙x≈z∙x = injective (cancelʳ ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ (begin - ⟦ y ⟧ ◦ ⟦ x ⟧ ≈⟨ homo y x ⟨ - ⟦ y ∙ x ⟧ ≈⟨ ⟦⟧-cong y∙x≈z∙x ⟩ - ⟦ z ∙ x ⟧ ≈⟨ homo z x ⟩ + ⟦ y ⟧ ◦ ⟦ x ⟧ ≈⟨ ∙-homo y x ⟨ + ⟦ y ∙ x ⟧ ≈⟨ ⟦⟧-cong y∙x≈z∙x ⟩ + ⟦ z ∙ x ⟧ ≈⟨ ∙-homo z x ⟩ ⟦ z ⟧ ◦ ⟦ x ⟧ ∎)) cancel : Cancellative _≈₂_ _◦_ → Cancellative _≈₁_ _∙_ diff --git a/src/Algebra/Morphism/MonoidMonomorphism.agda b/src/Algebra/Morphism/MonoidMonomorphism.agda index 1b918295af..b720360cad 100644 --- a/src/Algebra/Morphism/MonoidMonomorphism.agda +++ b/src/Algebra/Morphism/MonoidMonomorphism.agda @@ -43,14 +43,14 @@ module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where identityˡ : LeftIdentity _≈₂_ ε₂ _◦_ → LeftIdentity _≈₁_ ε₁ _∙_ identityˡ idˡ x = injective (begin - ⟦ ε₁ ∙ x ⟧ ≈⟨ homo ε₁ x ⟩ + ⟦ ε₁ ∙ x ⟧ ≈⟨ ∙-homo ε₁ x ⟩ ⟦ ε₁ ⟧ ◦ ⟦ x ⟧ ≈⟨ ◦-cong ε-homo refl ⟩ ε₂ ◦ ⟦ x ⟧ ≈⟨ idˡ ⟦ x ⟧ ⟩ ⟦ x ⟧ ∎) identityʳ : RightIdentity _≈₂_ ε₂ _◦_ → RightIdentity _≈₁_ ε₁ _∙_ identityʳ idʳ x = injective (begin - ⟦ x ∙ ε₁ ⟧ ≈⟨ homo x ε₁ ⟩ + ⟦ x ∙ ε₁ ⟧ ≈⟨ ∙-homo x ε₁ ⟩ ⟦ x ⟧ ◦ ⟦ ε₁ ⟧ ≈⟨ ◦-cong refl ε-homo ⟩ ⟦ x ⟧ ◦ ε₂ ≈⟨ idʳ ⟦ x ⟧ ⟩ ⟦ x ⟧ ∎) @@ -60,17 +60,17 @@ module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where zeroˡ : LeftZero _≈₂_ ε₂ _◦_ → LeftZero _≈₁_ ε₁ _∙_ zeroˡ zeˡ x = injective (begin - ⟦ ε₁ ∙ x ⟧ ≈⟨ homo ε₁ x ⟩ - ⟦ ε₁ ⟧ ◦ ⟦ x ⟧ ≈⟨ ◦-cong ε-homo refl ⟩ - ε₂ ◦ ⟦ x ⟧ ≈⟨ zeˡ ⟦ x ⟧ ⟩ + ⟦ ε₁ ∙ x ⟧ ≈⟨ ∙-homo ε₁ x ⟩ + ⟦ ε₁ ⟧ ◦ ⟦ x ⟧ ≈⟨ ◦-cong ε-homo refl ⟩ + ε₂ ◦ ⟦ x ⟧ ≈⟨ zeˡ ⟦ x ⟧ ⟩ ε₂ ≈⟨ ε-homo ⟨ ⟦ ε₁ ⟧ ∎) zeroʳ : RightZero _≈₂_ ε₂ _◦_ → RightZero _≈₁_ ε₁ _∙_ zeroʳ zeʳ x = injective (begin - ⟦ x ∙ ε₁ ⟧ ≈⟨ homo x ε₁ ⟩ - ⟦ x ⟧ ◦ ⟦ ε₁ ⟧ ≈⟨ ◦-cong refl ε-homo ⟩ - ⟦ x ⟧ ◦ ε₂ ≈⟨ zeʳ ⟦ x ⟧ ⟩ + ⟦ x ∙ ε₁ ⟧ ≈⟨ ∙-homo x ε₁ ⟩ + ⟦ x ⟧ ◦ ⟦ ε₁ ⟧ ≈⟨ ◦-cong refl ε-homo ⟩ + ⟦ x ⟧ ◦ ε₂ ≈⟨ zeʳ ⟦ x ⟧ ⟩ ε₂ ≈⟨ ε-homo ⟨ ⟦ ε₁ ⟧ ∎) diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 4669e479d9..4ed02a9dca 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -699,7 +699,7 @@ toℕ-homo-+ 1+[2 x ] 1+[2 y ] = begin toℕ-isMagmaHomomorphism-+ : IsMagmaHomomorphism +-rawMagma ℕ.+-rawMagma toℕ toℕ-isMagmaHomomorphism-+ = record { isRelHomomorphism = toℕ-isRelHomomorphism - ; homo = toℕ-homo-+ + ; ∙-homo = toℕ-homo-+ } toℕ-isMonoidHomomorphism-+ : IsMonoidHomomorphism +-0-rawMonoid ℕ.+-0-rawMonoid toℕ @@ -1012,7 +1012,7 @@ toℕ-homo-* x y = aux x y (size x ℕ.+ size y) ℕ.≤-refl toℕ-isMagmaHomomorphism-* : IsMagmaHomomorphism *-rawMagma ℕ.*-rawMagma toℕ toℕ-isMagmaHomomorphism-* = record { isRelHomomorphism = toℕ-isRelHomomorphism - ; homo = toℕ-homo-* + ; ∙-homo = toℕ-homo-* } toℕ-isMonoidHomomorphism-* : IsMonoidHomomorphism *-1-rawMonoid ℕ.*-1-rawMonoid toℕ From 11e036300a0e654baee63b0e61822f69896e784d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 29 Aug 2024 16:39:19 +0100 Subject: [PATCH 05/12] fix indentation; what about the deprecation? --- src/Algebra/Morphism/Structures.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index ed9c7cffed..90fc75ca3b 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -85,7 +85,7 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧ ∙-homo : Homomorphic₂ ⟦_⟧ _∙_ _◦_ - -- Deprecated. + -- Deprecated. homo = ∙-homo {-# WARNING_ON_USAGE homo "Warning: homo was deprecated in v2.2. From 54add532993e99324cf70b0e039ca762dff66218 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 4 Sep 2024 21:11:28 +0100 Subject: [PATCH 06/12] last occurrence of `homo`; plus indentation... --- src/Algebra/Morphism/MagmaMonomorphism.agda | 2 +- src/Algebra/Morphism/Structures.agda | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Morphism/MagmaMonomorphism.agda b/src/Algebra/Morphism/MagmaMonomorphism.agda index 88bc6171d1..fdf792c67a 100644 --- a/src/Algebra/Morphism/MagmaMonomorphism.agda +++ b/src/Algebra/Morphism/MagmaMonomorphism.agda @@ -50,7 +50,7 @@ module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where ⟦ (x ∙ y) ∙ z ⟧ ≈⟨ ∙-homo (x ∙ y) z ⟩ ⟦ x ∙ y ⟧ ◦ ⟦ z ⟧ ≈⟨ ◦-cong (∙-homo x y) refl ⟩ (⟦ x ⟧ ◦ ⟦ y ⟧) ◦ ⟦ z ⟧ ≈⟨ assoc ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ ⟩ - ⟦ x ⟧ ◦ (⟦ y ⟧ ◦ ⟦ z ⟧) ≈⟨ ◦-cong refl (homo y z) ⟨ + ⟦ x ⟧ ◦ (⟦ y ⟧ ◦ ⟦ z ⟧) ≈⟨ ◦-cong refl (∙-homo y z) ⟨ ⟦ x ⟧ ◦ ⟦ y ∙ z ⟧ ≈⟨ ∙-homo x (y ∙ z) ⟨ ⟦ x ∙ (y ∙ z) ⟧ ∎) diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index 90fc75ca3b..db6cebf627 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -83,7 +83,7 @@ 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 @@ -277,7 +277,7 @@ module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSe record IsNearSemiringMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧ - injective : Injective _≈₁_ _≈₂_ ⟦_⟧ + injective : Injective _≈₁_ _≈₂_ ⟦_⟧ open IsNearSemiringHomomorphism isNearSemiringHomomorphism public @@ -449,7 +449,7 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi +-isGroupMonomorphism : +.IsGroupMonomorphism ⟦_⟧ +-isGroupMonomorphism = record { isGroupHomomorphism = +-isGroupHomomorphism - ; injective = injective + ; injective = injective } open +.IsGroupMonomorphism +-isGroupMonomorphism public @@ -472,7 +472,7 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi +-isGroupIsomorphism : +.IsGroupIsomorphism ⟦_⟧ +-isGroupIsomorphism = record { isGroupMonomorphism = +-isGroupMonomorphism - ; surjective = surjective + ; surjective = surjective } open +.IsGroupIsomorphism +-isGroupIsomorphism public From 6184200d53c4d4a74245879c1f4e1a3dc1798ed4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 4 Sep 2024 21:13:07 +0100 Subject: [PATCH 07/12] more indentation... --- src/Algebra/Morphism/MagmaMonomorphism.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Morphism/MagmaMonomorphism.agda b/src/Algebra/Morphism/MagmaMonomorphism.agda index fdf792c67a..a55c5d80a1 100644 --- a/src/Algebra/Morphism/MagmaMonomorphism.agda +++ b/src/Algebra/Morphism/MagmaMonomorphism.agda @@ -81,8 +81,8 @@ module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where cancelˡ : LeftCancellative _≈₂_ _◦_ → LeftCancellative _≈₁_ _∙_ cancelˡ cancelˡ x y z x∙y≈x∙z = injective (cancelˡ ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ (begin ⟦ x ⟧ ◦ ⟦ y ⟧ ≈⟨ ∙-homo x y ⟨ - ⟦ x ∙ y ⟧ ≈⟨ ⟦⟧-cong x∙y≈x∙z ⟩ - ⟦ x ∙ z ⟧ ≈⟨ ∙-homo x z ⟩ + ⟦ x ∙ y ⟧ ≈⟨ ⟦⟧-cong x∙y≈x∙z ⟩ + ⟦ x ∙ z ⟧ ≈⟨ ∙-homo x z ⟩ ⟦ x ⟧ ◦ ⟦ z ⟧ ∎)) cancelʳ : RightCancellative _≈₂_ _◦_ → RightCancellative _≈₁_ _∙_ From 7fb2d88a04d43638d8c24824de49df2c9390680e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 7 Dec 2024 06:11:23 +0000 Subject: [PATCH 08/12] fix `import`s at top-level and exports from `KleeneAlgebraHomomorphism` --- src/Algebra/Morphism/Bundles.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda index 62f7287d0d..5ce7ec3945 100644 --- a/src/Algebra/Morphism/Bundles.agda +++ b/src/Algebra/Morphism/Bundles.agda @@ -13,8 +13,6 @@ module Algebra.Morphism.Bundles where open import Algebra.Bundles.Raw open import Algebra.Morphism.Structures open import Level using (Level; suc; _⊔_) ---open import Relation.Binary.Morphism using (IsRelHomomorphism) ---open import Relation.Binary.Morphism.Bundles using (SetoidHomomorphism) private variable @@ -160,7 +158,9 @@ record KleeneAlgebraHomomorphism semiringHomomorphism = record { isSemiringHomomorphism = isSemiringHomomorphism } open SemiringHomomorphism semiringHomomorphism public - hiding (*-isMagmaHomomorphism; *-isMonoidHomomorphism) + using ( nearSemiringHomomorphism + ; *-monoidHomomorphism; *-magmaHomomorphism + ; +-monoidHomomorphism; +-magmaHomomorphism) ------------------------------------------------------------------------ -- Morphisms between RingWithoutOnes From a56664476b331e31311eb63c83a54f6107ea8cbc Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 9 Dec 2024 17:31:37 +0000 Subject: [PATCH 09/12] knock-on --- src/Data/List/Effectful/Foldable.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/Effectful/Foldable.agda b/src/Data/List/Effectful/Foldable.agda index 188c885d10..fbdcbf477f 100644 --- a/src/Data/List/Effectful/Foldable.agda +++ b/src/Data/List/Effectful/Foldable.agda @@ -72,7 +72,7 @@ module _ (M : Monoid c ℓ) (f : A → Monoid.Carrier M) where { isMagmaHomomorphism = record { isRelHomomorphism = record { cong = reflexive ∘ ≡.cong h } - ; homo = λ xs _ → ++-homo xs + ; ∙-homo = λ xs _ → ++-homo xs } ; ε-homo = []-homo } From 57f2d24cd4971883da687f6f1df2021cae62b6e9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 18 Jan 2025 08:36:37 +0000 Subject: [PATCH 10/12] updated `CHANGELOG` to v2.3 --- CHANGELOG.md | 545 +-------------------------------------------------- 1 file changed, 2 insertions(+), 543 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2e945c3c09..f5fa12a54e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,7 +1,7 @@ -Version 2.2-dev +Version 2.3-dev =============== -The library has been tested using Agda 2.7.0. +The library has been tested using Agda 2.7.0 and 2.7.0.1. Highlights ---------- @@ -9,20 +9,9 @@ Highlights Bug-fixes --------- -* Removed unnecessary parameter `#-trans : Transitive _#_` from - `Relation.Binary.Reasoning.Base.Apartness`. -* Relax the types for `≡-syntax` in `Relation.Binary.HeterogeneousEquality`. - These operators are used for equational reasoning of heterogeneous equality - `x ≅ y`, but previously the three operators in `≡-syntax` unnecessarily require - `x` and `y` to have the same type, making them unusable in most situations. - Non-backwards compatible changes -------------------------------- -* In `Function.Related.TypeIsomorphisms`, the unprimed versions are more level polymorphic; and the primed versions retain `Level` homogeneous types for the `Semiring` axioms to hold. - -* In `Data.List.Relation.Binary.Sublist.Propositional.Properties` the implicit module parameters `a` and `A` have been replaced with `variable`s. This should be a backwards compatible change for the overwhelming majority of uses, and would only be non-backwards compatible if you were explicitly supplying these implicit parameters for some reason when importing the module. Explicitly supplying the implicit parameters for functions exported from the module should not be affected. - Minor improvements ------------------ @@ -37,538 +26,8 @@ Deprecated names homo ↦ ∙-homo ``` -* In `Algebra.Properties.CommutativeMagma.Divisibility`: - ```agda - ∣-factors ↦ x|xy∧y|xy - ∣-factors-≈ ↦ xy≈z⇒x|z∧y|z - ``` - -* In `Algebra.Properties.Magma.Divisibility`: - ```agda - ∣-respˡ ↦ ∣-respˡ-≈ - ∣-respʳ ↦ ∣-respʳ-≈ - ∣-resp ↦ ∣-resp-≈ - ``` - -* In `Algebra.Solver.CommutativeMonoid`: - ```agda - normalise-correct ↦ Algebra.Solver.CommutativeMonoid.Normal.correct - sg ↦ Algebra.Solver.CommutativeMonoid.Normal.singleton - sg-correct ↦ Algebra.Solver.CommutativeMonoid.Normal.singleton-correct - ``` - -* In `Algebra.Solver.IdempotentCommutativeMonoid`: - ```agda - flip12 ↦ Algebra.Properties.CommutativeSemigroup.xy∙z≈y∙xz - distr ↦ Algebra.Properties.IdempotentCommutativeMonoid.∙-distrˡ-∙ - normalise-correct ↦ Algebra.Solver.IdempotentCommutativeMonoid.Normal.correct - sg ↦ Algebra.Solver.IdempotentCommutativeMonoid.Normal.singleton - sg-correct ↦ Algebra.Solver.IdempotentCommutativeMonoid.Normal.singleton-correct - ``` - -* In `Algebra.Solver.Monoid`: - ```agda - homomorphic ↦ Algebra.Solver.Monoid.Normal.comp-correct - normalise-correct ↦ Algebra.Solver.Monoid.Normal.correct - ``` - -* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`: - ```agda - split ↦ ↭-split - ``` - with a more informative type (see below). - ``` - -* In `Data.Vec.Properties`: - ```agda - ++-assoc _ ↦ ++-assoc-eqFree - ++-identityʳ _ ↦ ++-identityʳ-eqFree - unfold-∷ʳ _ ↦ unfold-∷ʳ-eqFree - ++-∷ʳ _ ↦ ++-∷ʳ-eqFree - ∷ʳ-++ _ ↦ ∷ʳ-++-eqFree - reverse-++ _ ↦ reverse-++-eqFree - ∷-ʳ++ _ ↦ ∷-ʳ++-eqFree - ++-ʳ++ _ ↦ ++-ʳ++-eqFree - ʳ++-ʳ++ _ ↦ ʳ++-ʳ++-eqFree - ``` - New modules ----------- -* Bundled morphisms between (raw) algebraic structures: - ``` - Algebra.Morphism.Bundles - ``` - -* Properties of `IdempotentCommutativeMonoid`s refactored out from `Algebra.Solver.IdempotentCommutativeMonoid`: - ```agda - Algebra.Properties.IdempotentCommutativeMonoid - ``` - -* Consequences of module monomorphisms - ```agda - Algebra.Module.Morphism.BimoduleMonomorphism - Algebra.Module.Morphism.BisemimoduleMonomorphism - Algebra.Module.Morphism.LeftModuleMonomorphism - Algebra.Module.Morphism.LeftSemimoduleMonomorphism - Algebra.Module.Morphism.ModuleMonomorphism - Algebra.Module.Morphism.RightModuleMonomorphism - Algebra.Module.Morphism.RightSemimoduleMonomorphism - Algebra.Module.Morphism.SemimoduleMonomorphism - ``` - -* Refactoring of the `Algebra.Solver.*Monoid` implementations, via - a single `Solver` module API based on the existing `Expr`, and - a common `Normal`-form API: - ```agda - Algebra.Solver.CommutativeMonoid.Normal - Algebra.Solver.IdempotentCommutativeMonoid.Normal - Algebra.Solver.Monoid.Expression - Algebra.Solver.Monoid.Normal - Algebra.Solver.Monoid.Solver - ``` - - NB Imports of the existing proof procedures `solve` and `prove` etc. should still be via the top-level interfaces in `Algebra.Solver.*Monoid`. - -* Refactored out from `Data.List.Relation.Unary.All.Properties` in order to break a dependency cycle with `Data.List.Membership.Setoid.Properties`: - ```agda - Data.List.Relation.Unary.All.Properties.Core - ``` - -* `Data.List.Relation.Binary.Disjoint.Propositional.Properties`: - Propositional counterpart to `Data.List.Relation.Binary.Disjoint.Setoid.Properties` - ```agda - sum-↭ : sum Preserves _↭_ ⟶ _≡_ - ``` - -* `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK` - -* Refactored `Data.Refinement` into: - ```agda - Data.Refinement.Base - Data.Refinement.Properties - ``` - -* Raw bundles for the `Relation.Binary.Bundles` hierarchy: - ```agda - Relation.Binary.Bundles.Raw - ``` - plus adding `rawX` fields to each of `Relation.Binary.Bundles.X`. - -* `Data.List.Effectful.Foldable`: `List` is `Foldable` - -* `Data.Vec.Effectful.Foldable`: `Vec` is `Foldable` - -* `Effect.Foldable`: implementation of haskell-like `Foldable` - Additions to existing modules ----------------------------- - -* In `Algebra.Bundles.KleeneAlgebra`: - ```agda - rawKleeneAlgebra : RawKleeneAlgebra _ _ - ``` - -* In `Algebra.Bundles.Raw.RawRingWithoutOne` - ```agda - rawNearSemiring : RawNearSemiring c ℓ - ``` - -* Exporting more `Raw` substructures from `Algebra.Bundles.Ring`: - ```agda - rawNearSemiring : RawNearSemiring _ _ - rawRingWithoutOne : RawRingWithoutOne _ _ - +-rawGroup : RawGroup _ _ - ``` - -* Exporting `RawRingWithoutOne` and `(Raw)NearSemiring` subbundles from - `Algebra.Bundles.RingWithoutOne`: - ```agda - nearSemiring : NearSemiring _ _ - rawNearSemiring : RawNearSemiring _ _ - rawRingWithoutOne : RawRingWithoutOne _ _ - ``` - -* In `Algebra.Morphism.Construct.Composition`: - ```agda - magmaHomomorphism : MagmaHomomorphism M₁.rawMagma M₂.rawMagma → - MagmaHomomorphism M₂.rawMagma M₃.rawMagma → - MagmaHomomorphism M₁.rawMagma M₃.rawMagma - monoidHomomorphism : MonoidHomomorphism M₁.rawMonoid M₂.rawMonoid → - MonoidHomomorphism M₂.rawMonoid M₃.rawMonoid → - MonoidHomomorphism M₁.rawMonoid M₃.rawMonoid - groupHomomorphism : GroupHomomorphism M₁.rawGroup M₂.rawGroup → - GroupHomomorphism M₂.rawGroup M₃.rawGroup → - GroupHomomorphism M₁.rawGroup M₃.rawGroup - nearSemiringHomomorphism : NearSemiringHomomorphism M₁.rawNearSemiring M₂.rawNearSemiring → - NearSemiringHomomorphism M₂.rawNearSemiring M₃.rawNearSemiring → - NearSemiringHomomorphism M₁.rawNearSemiring M₃.rawNearSemiring - semiringHomomorphism : SemiringHomomorphism M₁.rawSemiring M₂.rawSemiring → - SemiringHomomorphism M₂.rawSemiring M₃.rawSemiring → - SemiringHomomorphism M₁.rawSemiring M₃.rawSemiring - kleeneAlgebraHomomorphism : KleeneAlgebraHomomorphism M₁.rawKleeneAlgebra M₂.rawKleeneAlgebra → - KleeneAlgebraHomomorphism M₂.rawKleeneAlgebra M₃.rawKleeneAlgebra → - KleeneAlgebraHomomorphism M₁.rawKleeneAlgebra M₃.rawKleeneAlgebra - nearSemiringHomomorphism : NearSemiringHomomorphism M₁.rawNearSemiring M₂.rawNearSemiring → - NearSemiringHomomorphism M₂.rawNearSemiring M₃.rawNearSemiring → - NearSemiringHomomorphism M₁.rawNearSemiring M₃.rawNearSemiring - ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₂.rawRingWithoutOne → - RingWithoutOneHomomorphism M₂.rawRingWithoutOne M₃.rawRingWithoutOne → - RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₃.rawRingWithoutOne - ringHomomorphism : RingHomomorphism M₁.rawRing M₂.rawRing → - RingHomomorphism M₂.rawRing M₃.rawRing → - RingHomomorphism M₁.rawRing M₃.rawRing - quasigroupHomomorphism : QuasigroupHomomorphism M₁.rawQuasigroup M₂.rawQuasigroup → - QuasigroupHomomorphism M₂.rawQuasigroup M₃.rawQuasigroup → - QuasigroupHomomorphism M₁.rawQuasigroup M₃.rawQuasigroup - loopHomomorphism : LoopHomomorphism M₁.rawLoop M₂.rawLoop → - LoopHomomorphism M₂.rawLoop M₃.rawLoop → - LoopHomomorphism M₁.rawLoop M₃.rawLoop - ``` - -* In `Algebra.Morphism.Construct.Identity`: - ```agda - magmaHomomorphism : MagmaHomomorphism M.rawMagma M.rawMagma - monoidHomomorphism : MonoidHomomorphism M.rawMonoid M.rawMonoid - groupHomomorphism : GroupHomomorphism M.rawGroup M.rawGroup - nearSemiringHomomorphism : NearSemiringHomomorphism M.raw M.raw - semiringHomomorphism : SemiringHomomorphism M.rawNearSemiring M.rawNearSemiring - kleeneAlgebraHomomorphism : KleeneAlgebraHomomorphism M.rawKleeneAlgebra M.rawKleeneAlgebra - nearSemiringHomomorphism : NearSemiringHomomorphism M.rawNearSemiring M.rawNearSemiring - ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M.rawRingWithoutOne M.rawRingWithoutOne - ringHomomorphism : RingHomomorphism M.rawRing M.rawRing - quasigroupHomomorphism : QuasigroupHomomorphism M.rawQuasigroup M.rawQuasigroup - loopHomomorphism : LoopHomomorphism M.rawLoop M.rawLoop - ``` - -* In `Algebra.Morphism.Structures.RingMorphisms` - ```agda - isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧ - ``` - -* In `Algebra.Morphism.Structures.RingWithoutOneMorphisms` - ```agda - isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧ - ``` - -* Properties of non-divisibility in `Algebra.Properties.Magma.Divisibility`: - ```agda - ∤-respˡ-≈ : _∤_ Respectsˡ _≈_ - ∤-respʳ-≈ : _∤_ Respectsʳ _≈_ - ∤-resp-≈ : _∤_ Respects₂ _≈_ - ∤∤-sym : Symmetric _∤∤_ - ∤∤-respˡ-≈ : _∤∤_ Respectsˡ _≈_ - ∤∤-respʳ-≈ : _∤∤_ Respectsʳ _≈_ - ∤∤-resp-≈ : _∤∤_ Respects₂ _≈_ - ``` - -* In `Algebra.Solver.Ring` - ```agda - Env : ℕ → Set _ - Env = Vec Carrier - ``` - -* In `Algebra.Structures.RingWithoutOne`: - ```agda - isNearSemiring : IsNearSemiring _ _ - ``` - -* In `Data.List.Membership.Setoid.Properties`: - ```agda - ∉⇒All[≉] : x ∉ xs → All (x ≉_) xs - All[≉]⇒∉ : All (x ≉_) xs → x ∉ xs - Any-∈-swap : Any (_∈ ys) xs → Any (_∈ xs) ys - All-∉-swap : All (_∉ ys) xs → All (_∉ xs) ys - ∈-map∘filter⁻ : y ∈₂ map f (filter P? xs) → ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x - ∈-map∘filter⁺ : f Preserves _≈₁_ ⟶ _≈₂_ → - ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x → - y ∈₂ map f (filter P? xs) - ∈-concatMap⁺ : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs - ∈-concatMap⁻ : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs - ∉[] : x ∉ [] - deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → z ∈ xs ⇔ z ∈ deduplicate R? xs - ``` - -* In `Data.List.Membership.Propositional.Properties`: - ```agda - ∈-AllPairs₂ : AllPairs R xs → x ∈ xs → y ∈ xs → x ≡ y ⊎ R x y ⊎ R y x - ∈-map∘filter⁻ : y ∈ map f (filter P? xs) → (∃[ x ] x ∈ xs × y ≡ f x × P x) - ∈-map∘filter⁺ : (∃[ x ] x ∈ xs × y ≡ f x × P x) → y ∈ map f (filter P? xs) - ∈-concatMap⁺ : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs - ∈-concatMap⁻ : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs - ++-∈⇔ : v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys) - []∉map∷ : [] ∉ map (x ∷_) xss - map∷⁻ : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × xs ≡ y ∷ ys - map∷-decomp∈ : (x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss - ∈-map∷⁻ : xs ∈ map (x ∷_) xss → x ∈ xs - ∉[] : x ∉ [] - deduplicate-∈⇔ : z ∈ xs ⇔ z ∈ deduplicate _≈?_ xs - ``` - -* In `Data.List.Membership.Propositional.Properties.WithK`: - ```agda - unique∧set⇒bag : Unique xs → Unique ys → xs ∼[ set ] ys → xs ∼[ bag ] ys - ``` - -* In `Data.List.Properties`: - ```agda - product≢0 : All NonZero ns → NonZero (product ns) - ∈⇒≤product : All NonZero ns → n ∈ ns → n ≤ product ns - concatMap-++ : concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys - filter-≐ : P ≐ Q → filter P? ≗ filter Q? - - partition-is-foldr : partition P? ≗ foldr (λ x → if does (P? x) then Product.map₁ (x ∷_) - else Product.map₂ (x ∷_)) - ([] , []) - ``` - -* In `Data.List.Relation.Unary.All.Properties`: - ```agda - all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss - ``` - -* In `Data.List.Relation.Unary.Any.Properties`: - ```agda - concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs) - concatMap⁻ : Any P (concatMap f xs) → Any (Any P ∘ f) xs - ``` - -* In `Data.List.Relation.Unary.Unique.Setoid.Properties`: - ```agda - Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs - ``` - -* In `Data.List.Relation.Unary.Unique.Propositional.Properties`: - ```agda - Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs - ``` - -* In `Data.List.Relation.Binary.Equality.Setoid`: - ```agda - ++⁺ʳ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs - ++⁺ˡ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs - ``` - -* In `Data.List.Relation.Binary.Permutation.Homogeneous`: - ```agda - steps : Permutation R xs ys → ℕ - ``` - -* In `Data.List.Relation.Binary.Permutation.Propositional`: - constructor aliases - ```agda - ↭-refl : Reflexive _↭_ - ↭-prep : ∀ x → xs ↭ ys → x ∷ xs ↭ x ∷ ys - ↭-swap : ∀ x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys - ``` - and properties - ```agda - ↭-reflexive-≋ : _≋_ ⇒ _↭_ - ↭⇒↭ₛ : _↭_ ⇒ _↭ₛ_ - ↭ₛ⇒↭ : _↭ₛ_ ⇒ _↭_ - ``` - where `_↭ₛ_` is the `Setoid (setoid _)` instance of `Permutation` - -* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`: - ```agda - Any-resp-[σ∘σ⁻¹] : (σ : xs ↭ ys) (iy : Any P ys) → - Any-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy - ∈-resp-[σ∘σ⁻¹] : (σ : xs ↭ ys) (iy : y ∈ ys) → - ∈-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy - product-↭ : product Preserves _↭_ ⟶ _≡_ - ``` - -* In `Data.List.Relation.Binary.Permutation.Setoid`: - ```agda - ↭-reflexive-≋ : _≋_ ⇒ _↭_ - ↭-transˡ-≋ : LeftTrans _≋_ _↭_ - ↭-transʳ-≋ : RightTrans _↭_ _≋_ - ↭-trans′ : Transitive _↭_ - ``` - -* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`: - ```agda - ↭-split : xs ↭ (as ++ [ v ] ++ bs) → - ∃₂ λ ps qs → xs ≋ (ps ++ [ v ] ++ qs) × (ps ++ qs) ↭ (as ++ bs) - drop-∷ : x ∷ xs ↭ x ∷ ys → xs ↭ ys - ``` - -* In `Data.List.Relation.Binary.Pointwise`: - ```agda - ++⁺ʳ : Reflexive R → ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R) - ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R) - ``` - -* In `Data.List.Relation.Unary.All`: - ```agda - search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs - -* In `Data.List.Relation.Binary.Subset.Setoid.Properties`: - ```agda - ∷⊈[] : x ∷ xs ⊈ [] - ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys - ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys - ``` - -* In `Data.List.Relation.Binary.Subset.Propositional.Properties`: - ```agda - ∷⊈[] : x ∷ xs ⊈ [] - ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys - ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys - ``` - -* In `Data.List.Relation.Binary.Subset.Propositional.Properties`: - ```agda - concatMap⁺ : xs ⊆ ys → concatMap f xs ⊆ concatMap f ys - ``` - -* In `Data.List.Relation.Binary.Sublist.Heterogeneous.Properties`: - ```agda - Sublist-[]-universal : Universal (Sublist R []) - ``` - -* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`: - ```agda - []⊆-universal : Universal ([] ⊆_) - ``` - -* In `Data.List.Relation.Binary.Disjoint.Setoid.Properties`: - ```agda - deduplicate⁺ : Disjoint S xs ys → Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys) - ``` - -* In `Data.List.Relation.Binary.Disjoint.Propositional.Properties`: - ```agda - deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys) - ``` - -* In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`: - ```agda - dedup-++-↭ : Disjoint xs ys → - deduplicate _≟_ (xs ++ ys) ↭ deduplicate _≟_ xs ++ deduplicate _≟_ ys - ``` - -* In `Data.List.Relation.Unary.First.Properties`: - ```agda - ¬First⇒All : ∁ Q ⊆ P → ∁ (First P Q) ⊆ All P - ¬All⇒First : Decidable P → ∁ P ⊆ Q → ∁ (All P) ⊆ First P Q - ``` - -* In `Data.Maybe.Properties`: - ```agda - maybe′-∘ : ∀ f g → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b) - ``` - -* New lemmas in `Data.Nat.Properties`: - ```agda - m≤n⇒m≤n*o : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ n * o - m≤n⇒m≤o*n : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ o * n - <‴-irrefl : Irreflexive _≡_ _<‴_ - ≤‴-irrelevant : Irrelevant {A = ℕ} _≤‴_ - <‴-irrelevant : Irrelevant {A = ℕ} _<‴_ - >‴-irrelevant : Irrelevant {A = ℕ} _>‴_ - ≥‴-irrelevant : Irrelevant {A = ℕ} _≥‴_ - ``` - - adjunction between `suc` and `pred` - ```agda - suc[m]≤n⇒m≤pred[n] : suc m ≤ n → m ≤ pred n - m≤pred[n]⇒suc[m]≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n - ``` - -* In `Data.Product.Function.Dependent.Propositional`: - ```agda - congˡ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B - ``` - -* New lemmas in `Data.Rational.Properties`: - ```agda - nonNeg+nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p + q) - nonPos+nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonPositive (p + q) - pos+nonNeg⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : NonNegative q}} → Positive (p + q) - nonNeg+pos⇒pos : ∀ p .{{_ : NonNegative p}} q .{{_ : Positive q}} → Positive (p + q) - pos+pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p + q) - neg+nonPos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : NonPositive q}} → Negative (p + q) - nonPos+neg⇒neg : ∀ p .{{_ : NonPositive p}} q .{{_ : Negative q}} → Negative (p + q) - neg+neg⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Negative (p + q) - nonNeg*nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p * q) - nonPos*nonNeg⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonNegative q}} → NonPositive (p * q) - nonNeg*nonPos⇒nonPos : ∀ p .{{_ : NonNegative p}} q .{{_ : NonPositive q}} → NonPositive (p * q) - nonPos*nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonNegative (p * q) - pos*pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p * q) - neg*pos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Positive q}} → Negative (p * q) - pos*neg⇒neg : ∀ p .{{_ : Positive p}} q .{{_ : Negative q}} → Negative (p * q) - neg*neg⇒pos : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Positive (p * q) - ``` - -* New properties re-exported from `Data.Refinement`: - ```agda - value-injective : value v ≡ value w → v ≡ w - _≟_ : DecidableEquality A → DecidableEquality [ x ∈ A ∣ P x ] - ``` - -* New lemma in `Data.Vec.Properties`: - ```agda - map-concat : map f (concat xss) ≡ concat (map (map f) xss) - ``` - -* In `Data.Vec.Relation.Binary.Equality.DecPropositional`: - ```agda - _≡?_ : DecidableEquality (Vec A n) - ``` - -* In `Function.Related.TypeIsomorphisms`: - ```agda - Σ-distribˡ-⊎ : (∃ λ a → P a ⊎ Q a) ↔ (∃ P ⊎ ∃ Q) - Σ-distribʳ-⊎ : (Σ (A ⊎ B) P) ↔ (Σ A (P ∘ inj₁) ⊎ Σ B (P ∘ inj₂)) - ×-distribˡ-⊎ : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C) - ×-distribʳ-⊎ : ((A ⊎ B) × C) ↔ (A × C ⊎ B × C) - ∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y) - ``` - -* In `Relation.Binary.Bundles`: - ```agda - record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) - ``` - plus associated sub-bundles. - -* In `Relation.Binary.Construct.Interior.Symmetric`: - ```agda - decidable : Decidable R → Decidable (SymInterior R) - ``` - and for `Reflexive` and `Transitive` relations `R`: - ```agda - isDecEquivalence : Decidable R → IsDecEquivalence (SymInterior R) - isDecPreorder : Decidable R → IsDecPreorder (SymInterior R) R - isDecPartialOrder : Decidable R → IsDecPartialOrder (SymInterior R) R - decPreorder : Decidable R → DecPreorder _ _ _ - decPoset : Decidable R → DecPoset _ _ _ - ``` - -* In `Relation.Binary.Structures`: - ```agda - record IsDecPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where - field - isPreorder : IsPreorder _≲_ - _≟_ : Decidable _≈_ - _≲?_ : Decidable _≲_ - ``` - plus associated `isDecPreorder` fields in each higher `IsDec*Order` structure. - -* In `Relation.Nullary.Decidable`: - ```agda - does-⇔ : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b? - does-≡ : (a? b? : Dec A) → does a? ≡ does b? - ``` - -* In `Relation.Nullary.Recomputable`: - ```agda - irrelevant-recompute : Recomputable (Irrelevant A) - ``` - -* In `Relation.Unary.Properties`: - ```agda - map : P ≐ Q → Decidable P → Decidable Q - does-≐ : P ≐ Q → (P? : Decidable P) → (Q? : Decidable Q) → does ∘ P? ≗ does ∘ Q? - does-≡ : (P? P?′ : Decidable P) → does ∘ P? ≗ does ∘ P?′ - ``` From 167085f647c339fcad8fa53a61bf2f88b6fd2227 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 11 Feb 2025 10:36:22 +0000 Subject: [PATCH 11/12] fix: `CHANGELOG` entry --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9bdf662709..45bd9bbffb 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,8 @@ Bug-fixes Non-backwards compatible changes -------------------------------- +* [Issue #2548](https://github.com/agda/agda-stdlib/issues/2458) Consistent with other names (such as `∙-cong`, `ε-homo` etc.) in `Algebra.*`, the field name of the basic homomorphism property in `Algebra.Morphism.Structures.IsMagmaHomomorphism` has been renamed from `homo` to `∙-homo`. + Minor improvements ------------------ From ba06eca0e947d5c73af3a5513be5b2e4da7dec5a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 11 Feb 2025 10:55:13 +0000 Subject: [PATCH 12/12] fix: version number in the warning --- src/Algebra/Morphism/Structures.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index 70c8084159..55a2a1cd93 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -88,7 +88,7 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher -- Deprecated. homo = ∙-homo {-# WARNING_ON_USAGE homo - "Warning: homo was deprecated in v2.2. + "Warning: homo was deprecated in v3.0. Please use ∙-homo instead. " #-}