From fe3fea040fef67b3cfdf6e98a7fe9c360fd3c6ba Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 7 May 2024 16:56:35 +0100 Subject: [PATCH 01/27] Bundle `Algebra.Morphism`s --- CHANGELOG.md | 5 ++++ src/Algebra/Morphism/Bundles.agda | 40 +++++++++++++++++++++++++++++++ 2 files changed, 45 insertions(+) create mode 100644 src/Algebra/Morphism/Bundles.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 5c9cc9037b..717a0cf1f3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -83,6 +83,11 @@ New modules Algebra.Module.Bundles.Raw ``` +* Bundled morphisms between algebraic structures: + ``` + Algebra.Morphism.Bundles + ``` + * Prime factorisation of natural numbers. ``` Data.Nat.Primality.Factorisation diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda new file mode 100644 index 0000000000..bcb777795f --- /dev/null +++ b/src/Algebra/Morphism/Bundles.agda @@ -0,0 +1,40 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Bundled definitions of homomorphisms between algebras +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Algebra.Morphism.Bundles where + +open import Algebra.Bundles using (Magma) +open import Algebra.Morphism.Structures using (IsMagmaHomomorphism) +open import Level using (Level; suc; _⊔_) +open import Relation.Binary.Morphism using (IsRelHomomorphism) +open import Relation.Binary.Morphism.Bundles using (SetoidHomomorphism) + +private + variable + ℓ m ℓm n ℓn : Level + + +------------------------------------------------------------------------ +-- Morphisms between Magmas +------------------------------------------------------------------------ + +record MagmaHomomorphism (M : Magma m ℓm) (N : Magma n ℓn) : Set (m ⊔ n ⊔ ℓm ⊔ ℓn) where + private + module M = Magma M + module N = Magma N + + field + ⟦_⟧ : M.Carrier → N.Carrier + + isMagmaHomomorphism : IsMagmaHomomorphism M.rawMagma N.rawMagma ⟦_⟧ + + open IsMagmaHomomorphism isMagmaHomomorphism public + + setoidHomomorphism : SetoidHomomorphism M.setoid N.setoid + setoidHomomorphism = record { ⟦_⟧ = ⟦_⟧ ; isRelHomomorphism = isRelHomomorphism } + From a33cff668bdae483fa881b02687954648bb568cc Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 8 May 2024 10:17:16 +0100 Subject: [PATCH 02/27] more bundles! --- src/Algebra/Morphism/Bundles.agda | 158 ++++++++++++++++++++++++++++-- 1 file changed, 148 insertions(+), 10 deletions(-) diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda index bcb777795f..f215807ff3 100644 --- a/src/Algebra/Morphism/Bundles.agda +++ b/src/Algebra/Morphism/Bundles.agda @@ -8,33 +8,171 @@ module Algebra.Morphism.Bundles where -open import Algebra.Bundles using (Magma) -open import Algebra.Morphism.Structures using (IsMagmaHomomorphism) +open import Algebra.Bundles -- using (Magma) +open import Algebra.Morphism.Structures -- using (IsMagmaHomomorphism) open import Level using (Level; suc; _⊔_) open import Relation.Binary.Morphism using (IsRelHomomorphism) open import Relation.Binary.Morphism.Bundles using (SetoidHomomorphism) private variable - ℓ m ℓm n ℓn : Level + ℓ a ℓa b ℓb : Level ------------------------------------------------------------------------ -- Morphisms between Magmas ------------------------------------------------------------------------ -record MagmaHomomorphism (M : Magma m ℓm) (N : Magma n ℓn) : Set (m ⊔ n ⊔ ℓm ⊔ ℓn) where +record MagmaHomomorphism (A : Magma a ℓa) (B : Magma b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where private - module M = Magma M - module N = Magma N + module A = Magma A + module B = Magma B field - ⟦_⟧ : M.Carrier → N.Carrier + ⟦_⟧ : A.Carrier → B.Carrier - isMagmaHomomorphism : IsMagmaHomomorphism M.rawMagma N.rawMagma ⟦_⟧ + isMagmaHomomorphism : IsMagmaHomomorphism A.rawMagma B.rawMagma ⟦_⟧ open IsMagmaHomomorphism isMagmaHomomorphism public - setoidHomomorphism : SetoidHomomorphism M.setoid N.setoid - setoidHomomorphism = record { ⟦_⟧ = ⟦_⟧ ; isRelHomomorphism = isRelHomomorphism } + setoidHomomorphism : SetoidHomomorphism A.setoid B.setoid + setoidHomomorphism = record { isRelHomomorphism = isRelHomomorphism } + +------------------------------------------------------------------------ +-- Morphisms between Monoids +------------------------------------------------------------------------ + +record MonoidHomomorphism (A : Monoid a ℓa) (B : Monoid b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where + private + module A = Monoid A + module B = Monoid B + + field + ⟦_⟧ : A.Carrier → B.Carrier + + isMonoidHomomorphism : IsMonoidHomomorphism A.rawMonoid B.rawMonoid ⟦_⟧ + + open IsMonoidHomomorphism isMonoidHomomorphism public + + magmaHomomorphism : MagmaHomomorphism A.magma B.magma + magmaHomomorphism = record { isMagmaHomomorphism = isMagmaHomomorphism } + + open MagmaHomomorphism magmaHomomorphism public + +------------------------------------------------------------------------ +-- Morphisms between Groups +------------------------------------------------------------------------ + +record GroupHomomorphism (A : Group a ℓa) (B : Group b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where + private + module A = Group A + module B = Group B + + field + ⟦_⟧ : A.Carrier → B.Carrier + + isGroupHomomorphism : IsGroupHomomorphism A.rawGroup B.rawGroup ⟦_⟧ + + open IsGroupHomomorphism isGroupHomomorphism public + + monoidHomomorphism : MonoidHomomorphism A.monoid B.monoid + monoidHomomorphism = record { isMonoidHomomorphism = isMonoidHomomorphism } + + open MonoidHomomorphism monoidHomomorphism public + +------------------------------------------------------------------------ +-- Morphisms between NearSemirings +------------------------------------------------------------------------ + +record NearSemiringHomomorphism (A : NearSemiring a ℓa) (B : NearSemiring b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where + private + module A = NearSemiring A + module B = NearSemiring B + + field + ⟦_⟧ : A.Carrier → B.Carrier + + isNearSemiringHomomorphism : IsNearSemiringHomomorphism A.rawNearSemiring B.rawNearSemiring ⟦_⟧ + + open IsNearSemiringHomomorphism isNearSemiringHomomorphism public + + +-monoidHomomorphism : MonoidHomomorphism A.+-monoid B.+-monoid + +-monoidHomomorphism = record { isMonoidHomomorphism = +-isMonoidHomomorphism } + + open MonoidHomomorphism +-monoidHomomorphism public + + *-magmaHomomorphism : MagmaHomomorphism A.*-magma B.*-magma + *-magmaHomomorphism = record { isMagmaHomomorphism = *-isMagmaHomomorphism } + +------------------------------------------------------------------------ +-- Morphisms between Semirings +------------------------------------------------------------------------ + +record SemiringHomomorphism (A : Semiring a ℓa) (B : Semiring b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where + private + module A = Semiring A + module B = Semiring B + + field + ⟦_⟧ : A.Carrier → B.Carrier + + isSemiringHomomorphism : IsSemiringHomomorphism A.rawSemiring B.rawSemiring ⟦_⟧ + + open IsSemiringHomomorphism isSemiringHomomorphism public + + *-monoidHomomorphism : MonoidHomomorphism A.*-monoid B.*-monoid + *-monoidHomomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism } + + open MonoidHomomorphism *-monoidHomomorphism public + +------------------------------------------------------------------------ +-- Morphisms between RingWithoutOnes +------------------------------------------------------------------------ +{- + +Problem: bundle RingWithoutOne doesn't re-export its underlying RawRingWithoutOne! + +record RingWithoutOneHomomorphism (A : RingWithoutOne a ℓa) (B : RingWithoutOne b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where + private + module A = RingWithoutOne A + module B = RingWithoutOne B + + field + ⟦_⟧ : A.Carrier → B.Carrier + isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism A.rawRingWithoutOne B.rawRingWithoutOne ⟦_⟧ + + open IsRingWithoutOneHomomorphism isRingWithoutOneHomomorphism public + + +-groupHomomorphism : GroupHomomorphism A.+-group B.+-group + +-groupHomomorphism = record { isGroupHomomorphism = +-isGroupHomomorphism } + + open GroupHomomorphism +-groupHomomorphism public + + *-monoidHomomorphism : MonoidHomomorphism A.*-monoid B.*-monoid + *-monoidHomomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism } + + open MonoidHomomorphism *-monoidHomomorphism public +-} +------------------------------------------------------------------------ +-- Morphisms between Rings +------------------------------------------------------------------------ + +record RingHomomorphism (A : Ring a ℓa) (B : Ring b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where + private + module A = Ring A + module B = Ring B + + field + ⟦_⟧ : A.Carrier → B.Carrier + isRingHomomorphism : IsRingHomomorphism A.rawRing B.rawRing ⟦_⟧ + + open IsRingHomomorphism isRingHomomorphism public + + +-groupHomomorphism : GroupHomomorphism A.+-group B.+-group + +-groupHomomorphism = record { isGroupHomomorphism = +-isGroupHomomorphism } + + open GroupHomomorphism +-groupHomomorphism public + + *-monoidHomomorphism : MonoidHomomorphism A.*-monoid B.*-monoid + *-monoidHomomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism } From ca14ed90e62133f07f114792036214797a6c9ea1 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 15 May 2024 19:11:44 +0100 Subject: [PATCH 03/27] `RingWithoutOne` now exports a `RawRingWithoutOne` field --- src/Algebra/Bundles.agda | 23 ++++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 1969731c2c..7deadc64c0 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -868,6 +868,17 @@ record RingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where open IsRingWithoutOne isRingWithoutOne public + rawRingWithoutOne : RawRingWithoutOne _ _ + rawRingWithoutOne = record + { _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = 0# + } + + open RawRingWithoutOne rawRingWithoutOne public + +-abelianGroup : AbelianGroup _ _ +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup } @@ -875,13 +886,15 @@ record RingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where *-semigroup = record { isSemigroup = *-isSemigroup } open AbelianGroup +-abelianGroup public - using () renaming (group to +-group; invertibleMagma to +-invertibleMagma; invertibleUnitalMagma to +-invertibleUnitalMagma) + using () + renaming (group to +-group; + invertibleMagma to +-invertibleMagma; + invertibleUnitalMagma to +-invertibleUnitalMagma) open Semigroup *-semigroup public - using () renaming - ( rawMagma to *-rawMagma - ; magma to *-magma - ) + using () + renaming (magma to *-magma) + ------------------------------------------------------------------------ -- Bundles with 2 binary operations, 1 unary operation & 2 elements From a5f8c0e7484334386b36b5f9c38fd4feca9841bc Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 15 May 2024 19:27:07 +0100 Subject: [PATCH 04/27] disambiguation error when trying to add `RingWithoutOneHomomorphism` record --- CHANGELOG.md | 5 +++++ src/Algebra/Bundles.agda | 3 ++- src/Algebra/Morphism/Bundles.agda | 14 ++++++-------- 3 files changed, 13 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 717a0cf1f3..4e5bea0492 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -190,6 +190,11 @@ Additions to existing modules +-rawGroup : RawGroup _ _ ``` +* Exporting `RawRingWithoutOne` substructure from `Algebra.Bundles.RingWithoutOne`: + ```agda + rawRingWithoutOne : RawRingWithoutOne _ _ + ``` + * In `Algebra.Construct.Terminal`: ```agda rawNearSemiring : RawNearSemiring c ℓ diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 7deadc64c0..effba2bdce 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -870,7 +870,8 @@ record RingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where rawRingWithoutOne : RawRingWithoutOne _ _ rawRingWithoutOne = record - { _≈_ = _≈_ + { Carrier = Carrier + ; _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; -_ = -_ diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda index f215807ff3..b9a1595b57 100644 --- a/src/Algebra/Morphism/Bundles.agda +++ b/src/Algebra/Morphism/Bundles.agda @@ -128,9 +128,6 @@ record SemiringHomomorphism (A : Semiring a ℓa) (B : Semiring b ℓb) : Set (a ------------------------------------------------------------------------ -- Morphisms between RingWithoutOnes ------------------------------------------------------------------------ -{- - -Problem: bundle RingWithoutOne doesn't re-export its underlying RawRingWithoutOne! record RingWithoutOneHomomorphism (A : RingWithoutOne a ℓa) (B : RingWithoutOne b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where private @@ -138,7 +135,7 @@ record RingWithoutOneHomomorphism (A : RingWithoutOne a ℓa) (B : RingWithoutOn module B = RingWithoutOne B field - ⟦_⟧ : A.Carrier → B.Carrier + ⟦_⟧ : _ → _ -- A.Carrier → B.Carrier causes an disambiguation error!? isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism A.rawRingWithoutOne B.rawRingWithoutOne ⟦_⟧ open IsRingWithoutOneHomomorphism isRingWithoutOneHomomorphism public @@ -148,11 +145,12 @@ record RingWithoutOneHomomorphism (A : RingWithoutOne a ℓa) (B : RingWithoutOn open GroupHomomorphism +-groupHomomorphism public - *-monoidHomomorphism : MonoidHomomorphism A.*-monoid B.*-monoid - *-monoidHomomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism } + *-magmaHomomorphism : MagmaHomomorphism A.*-magma B.*-magma + *-magmaHomomorphism = record { isMagmaHomomorphism = *-isMagmaHomomorphism } + + open MagmaHomomorphism *-magmaHomomorphism public + hiding (setoidHomomorphism) - open MonoidHomomorphism *-monoidHomomorphism public --} ------------------------------------------------------------------------ -- Morphisms between Rings ------------------------------------------------------------------------ From 7d9649c59fc0d19692ea727ed5a2a81cb7294b34 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 15 May 2024 19:42:20 +0100 Subject: [PATCH 05/27] FIXED: disambiguation error when trying to add `RingWithoutOneHomomorphism` --- src/Algebra/Bundles.agda | 24 ++++++++++++------------ src/Algebra/Morphism/Bundles.agda | 2 +- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index effba2bdce..0680068bfd 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -868,18 +868,6 @@ record RingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where open IsRingWithoutOne isRingWithoutOne public - rawRingWithoutOne : RawRingWithoutOne _ _ - rawRingWithoutOne = record - { Carrier = Carrier - ; _≈_ = _≈_ - ; _+_ = _+_ - ; _*_ = _*_ - ; -_ = -_ - ; 0# = 0# - } - - open RawRingWithoutOne rawRingWithoutOne public - +-abelianGroup : AbelianGroup _ _ +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup } @@ -896,6 +884,18 @@ record RingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where using () renaming (magma to *-magma) + rawRingWithoutOne : RawRingWithoutOne _ _ + rawRingWithoutOne = record + { _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = 0# + } + + open RawRingWithoutOne rawRingWithoutOne public + using (+-rawGroup; *-rawMagma) + ------------------------------------------------------------------------ -- Bundles with 2 binary operations, 1 unary operation & 2 elements diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda index b9a1595b57..5308bd4feb 100644 --- a/src/Algebra/Morphism/Bundles.agda +++ b/src/Algebra/Morphism/Bundles.agda @@ -135,7 +135,7 @@ record RingWithoutOneHomomorphism (A : RingWithoutOne a ℓa) (B : RingWithoutOn module B = RingWithoutOne B field - ⟦_⟧ : _ → _ -- A.Carrier → B.Carrier causes an disambiguation error!? + ⟦_⟧ : A.Carrier → B.Carrier isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism A.rawRingWithoutOne B.rawRingWithoutOne ⟦_⟧ open IsRingWithoutOneHomomorphism isRingWithoutOneHomomorphism public From a4a154957cea8e7f5f9fd774070d03945ce25849 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 16 May 2024 08:52:28 +0100 Subject: [PATCH 06/27] add `rawKleeneAlgebra` --- CHANGELOG.md | 5 +++++ src/Algebra/Bundles.agda | 10 ++++++++++ 2 files changed, 15 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4e5bea0492..92612e2de7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -183,6 +183,11 @@ Additions to existing modules record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) ``` +* Exporting `RawKleeneAlgebra` substructure from `Algebra.Bundles.KleeneAlgebra`: + ```agda + rawKleeneAlgebra : RawKleeneAlgebra _ _ + ``` + * Exporting more `Raw` substructures from `Algebra.Bundles.Ring`: ```agda rawNearSemiring : RawNearSemiring _ _ diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 0680068bfd..7eb34a72e6 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -810,6 +810,16 @@ record KleeneAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where ; rawSemiring; semiring ) + rawKleeneAlgebra : RawKleeneAlgebra _ _ + rawKleeneAlgebra = record + { _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; _⋆ = _⋆ + ; 0# = 0# + ; 1# = 1# + } + record Quasiring c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _*_ infixl 6 _+_ From 32682ceb3a9bc53c53edbddd5ac41c9df7819f73 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 16 May 2024 09:45:22 +0100 Subject: [PATCH 07/27] add `KleeneAlgebra`, `Quasigroup`, and `Lopp` homomorphisms --- src/Algebra/Morphism/Bundles.agda | 58 +++++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda index 5308bd4feb..d5b751893f 100644 --- a/src/Algebra/Morphism/Bundles.agda +++ b/src/Algebra/Morphism/Bundles.agda @@ -125,6 +125,27 @@ record SemiringHomomorphism (A : Semiring a ℓa) (B : Semiring b ℓb) : Set (a open MonoidHomomorphism *-monoidHomomorphism public +------------------------------------------------------------------------ +-- Morphisms between KleeneAlgebras +------------------------------------------------------------------------ + +record KleeneAlgebraHomomorphism (A : KleeneAlgebra a ℓa) (B : KleeneAlgebra b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where + private + module A = KleeneAlgebra A + module B = KleeneAlgebra B + + field + ⟦_⟧ : A.Carrier → B.Carrier + isKleeneAlgebraHomomorphism : IsKleeneAlgebraHomomorphism A.rawKleeneAlgebra B.rawKleeneAlgebra ⟦_⟧ + + open IsKleeneAlgebraHomomorphism isKleeneAlgebraHomomorphism public + + semiringHomomorphism : SemiringHomomorphism A.semiring B.semiring + semiringHomomorphism = record { isSemiringHomomorphism = isSemiringHomomorphism } + + open SemiringHomomorphism semiringHomomorphism public + hiding (*-isMagmaHomomorphism; *-isMonoidHomomorphism) + ------------------------------------------------------------------------ -- Morphisms between RingWithoutOnes ------------------------------------------------------------------------ @@ -174,3 +195,40 @@ record RingHomomorphism (A : Ring a ℓa) (B : Ring b ℓb) : Set (a ⊔ b ⊔ *-monoidHomomorphism : MonoidHomomorphism A.*-monoid B.*-monoid *-monoidHomomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism } +------------------------------------------------------------------------ +-- Morphisms between Quasigroups +------------------------------------------------------------------------ + +record QuasigroupHomomorphism (A : Quasigroup a ℓa) (B : Quasigroup b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where + private + module A = Quasigroup A + module B = Quasigroup B + + field + ⟦_⟧ : A.Carrier → B.Carrier + isQuasigroupHomomorphism : IsQuasigroupHomomorphism A.rawQuasigroup B.rawQuasigroup ⟦_⟧ + + open IsQuasigroupHomomorphism isQuasigroupHomomorphism public + + magmaHomomorphism : MagmaHomomorphism A.magma B.magma + magmaHomomorphism = record { isMagmaHomomorphism = ∙-isMagmaHomomorphism } + + open MagmaHomomorphism magmaHomomorphism public + +------------------------------------------------------------------------ +-- Morphisms between Loops +------------------------------------------------------------------------ + +record LoopHomomorphism (A : Loop a ℓa) (B : Loop b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where + private + module A = Loop A + module B = Loop B + + field + ⟦_⟧ : A.Carrier → B.Carrier + isLoopHomomorphism : IsLoopHomomorphism A.rawLoop B.rawLoop ⟦_⟧ + + open IsLoopHomomorphism isLoopHomomorphism public + + quasigroupHomomorphism : QuasigroupHomomorphism A.quasigroup B.quasigroup + quasigroupHomomorphism = record { isQuasigroupHomomorphism = isQuasigroupHomomorphism } From 59474ace4f9ab688b4c47b5b6ba0d1736d174c9b Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 16 May 2024 10:00:38 +0100 Subject: [PATCH 08/27] add bundled `Identity` homomorphisms --- src/Algebra/Morphism/Construct/Identity.agda | 135 +++++++++++++++++++ 1 file changed, 135 insertions(+) diff --git a/src/Algebra/Morphism/Construct/Identity.agda b/src/Algebra/Morphism/Construct/Identity.agda index 881a8cf15c..fc1a7d1b2c 100644 --- a/src/Algebra/Morphism/Construct/Identity.agda +++ b/src/Algebra/Morphism/Construct/Identity.agda @@ -9,6 +9,7 @@ module Algebra.Morphism.Construct.Identity where open import Algebra.Bundles +open import Algebra.Morphism.Bundles open import Algebra.Morphism.Structures using ( module MagmaMorphisms ; module MonoidMorphisms @@ -274,3 +275,137 @@ module _ (K : RawKleeneAlgebra c ℓ) (open RawKleeneAlgebra K) (refl : Reflexiv ; surjective = Id.surjective _ } + +------------------------------------------------------------------------ +--- Bundled morphisms between algebras +----------------------------------------------------------------------- + +-- Magma + +module _ (M : Magma c ℓ) where + + open Magma M using (rawMagma; refl) + open MagmaMorphisms rawMagma rawMagma + + magmaHomomorphism : MagmaHomomorphism M M + magmaHomomorphism = record + { ⟦_⟧ = id + ; isMagmaHomomorphism = isMagmaHomomorphism rawMagma refl + } + +-- Monoid + +module _ (M : Monoid c ℓ) where + + open Monoid M using (rawMonoid; refl) + open MonoidMorphisms rawMonoid rawMonoid + + monoidHomomorphism : MonoidHomomorphism M M + monoidHomomorphism = record + { ⟦_⟧ = id + ; isMonoidHomomorphism = isMonoidHomomorphism rawMonoid refl + } + +-- Group + +module _ (M : Group c ℓ) where + + open Group M using (rawGroup; refl) + open GroupMorphisms rawGroup rawGroup + + groupHomomorphism : GroupHomomorphism M M + groupHomomorphism = record + { ⟦_⟧ = id + ; isGroupHomomorphism = isGroupHomomorphism rawGroup refl + } + +-- NearSemiring + +module _ (M : NearSemiring c ℓ) where + + open NearSemiring M using (rawNearSemiring; refl) + open NearSemiringMorphisms rawNearSemiring rawNearSemiring + + nearSemiringHomomorphism : NearSemiringHomomorphism M M + nearSemiringHomomorphism = record + { ⟦_⟧ = id + ; isNearSemiringHomomorphism = isNearSemiringHomomorphism rawNearSemiring refl + } + +-- Semiring + +module _ (M : Semiring c ℓ) where + + open Semiring M using (rawSemiring; refl) + open SemiringMorphisms rawSemiring rawSemiring + + semiringHomomorphism : SemiringHomomorphism M M + semiringHomomorphism = record + { ⟦_⟧ = id + ; isSemiringHomomorphism = isSemiringHomomorphism rawSemiring refl + } + +-- KleeneAlgebra + +module _ (M : KleeneAlgebra c ℓ) where + + open KleeneAlgebra M using (rawKleeneAlgebra; refl) + open KleeneAlgebraMorphisms rawKleeneAlgebra rawKleeneAlgebra + + kleeneAlgebraHomomorphism : KleeneAlgebraHomomorphism M M + kleeneAlgebraHomomorphism = record + { ⟦_⟧ = id + ; isKleeneAlgebraHomomorphism = isKleeneAlgebraHomomorphism rawKleeneAlgebra refl + } + +-- RingWithoutOne + +module _ (M : RingWithoutOne c ℓ) where + + open RingWithoutOne M using (rawRingWithoutOne; refl) + open RingWithoutOneMorphisms rawRingWithoutOne rawRingWithoutOne + + ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M M + ringWithoutOneHomomorphism = record + { ⟦_⟧ = id + ; isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism rawRingWithoutOne refl + } + +-- Ring + +module _ (M : Ring c ℓ) where + + open Ring M using (rawRing; refl) + open RingMorphisms rawRing rawRing + + ringHomomorphism : RingHomomorphism M M + ringHomomorphism = record + { ⟦_⟧ = id + ; isRingHomomorphism = isRingHomomorphism rawRing refl + } + +-- Quasigroup + +module _ (M : Quasigroup c ℓ) where + + open Quasigroup M using (rawQuasigroup; refl) + open QuasigroupMorphisms rawQuasigroup rawQuasigroup + + quasigroupHomomorphism : QuasigroupHomomorphism M M + quasigroupHomomorphism = record + { ⟦_⟧ = id + ; isQuasigroupHomomorphism = isQuasigroupHomomorphism rawQuasigroup refl + } + +-- Loop + +module _ (M : Loop c ℓ) where + + open Loop M using (rawLoop; refl) + open LoopMorphisms rawLoop rawLoop + + loopHomomorphism : LoopHomomorphism M M + loopHomomorphism = record + { ⟦_⟧ = id + ; isLoopHomomorphism = isLoopHomomorphism rawLoop refl + } From 6c8459f6697e34b0acf839ecc21c3f85706c131b Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 16 May 2024 10:25:05 +0100 Subject: [PATCH 09/27] avoid name clash: remove `open`ing of sub-homomorphism bundles --- src/Algebra/Morphism/Bundles.agda | 17 ----------------- 1 file changed, 17 deletions(-) diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda index d5b751893f..c774bf695e 100644 --- a/src/Algebra/Morphism/Bundles.agda +++ b/src/Algebra/Morphism/Bundles.agda @@ -57,8 +57,6 @@ record MonoidHomomorphism (A : Monoid a ℓa) (B : Monoid b ℓb) : Set (a ⊔ b magmaHomomorphism : MagmaHomomorphism A.magma B.magma magmaHomomorphism = record { isMagmaHomomorphism = isMagmaHomomorphism } - open MagmaHomomorphism magmaHomomorphism public - ------------------------------------------------------------------------ -- Morphisms between Groups ------------------------------------------------------------------------ @@ -78,8 +76,6 @@ record GroupHomomorphism (A : Group a ℓa) (B : Group b ℓb) : Set (a ⊔ b monoidHomomorphism : MonoidHomomorphism A.monoid B.monoid monoidHomomorphism = record { isMonoidHomomorphism = isMonoidHomomorphism } - open MonoidHomomorphism monoidHomomorphism public - ------------------------------------------------------------------------ -- Morphisms between NearSemirings ------------------------------------------------------------------------ @@ -99,8 +95,6 @@ record NearSemiringHomomorphism (A : NearSemiring a ℓa) (B : NearSemiring b +-monoidHomomorphism : MonoidHomomorphism A.+-monoid B.+-monoid +-monoidHomomorphism = record { isMonoidHomomorphism = +-isMonoidHomomorphism } - open MonoidHomomorphism +-monoidHomomorphism public - *-magmaHomomorphism : MagmaHomomorphism A.*-magma B.*-magma *-magmaHomomorphism = record { isMagmaHomomorphism = *-isMagmaHomomorphism } @@ -123,8 +117,6 @@ record SemiringHomomorphism (A : Semiring a ℓa) (B : Semiring b ℓb) : Set (a *-monoidHomomorphism : MonoidHomomorphism A.*-monoid B.*-monoid *-monoidHomomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism } - open MonoidHomomorphism *-monoidHomomorphism public - ------------------------------------------------------------------------ -- Morphisms between KleeneAlgebras ------------------------------------------------------------------------ @@ -164,14 +156,9 @@ record RingWithoutOneHomomorphism (A : RingWithoutOne a ℓa) (B : RingWithoutOn +-groupHomomorphism : GroupHomomorphism A.+-group B.+-group +-groupHomomorphism = record { isGroupHomomorphism = +-isGroupHomomorphism } - open GroupHomomorphism +-groupHomomorphism public - *-magmaHomomorphism : MagmaHomomorphism A.*-magma B.*-magma *-magmaHomomorphism = record { isMagmaHomomorphism = *-isMagmaHomomorphism } - open MagmaHomomorphism *-magmaHomomorphism public - hiding (setoidHomomorphism) - ------------------------------------------------------------------------ -- Morphisms between Rings ------------------------------------------------------------------------ @@ -190,8 +177,6 @@ record RingHomomorphism (A : Ring a ℓa) (B : Ring b ℓb) : Set (a ⊔ b ⊔ +-groupHomomorphism : GroupHomomorphism A.+-group B.+-group +-groupHomomorphism = record { isGroupHomomorphism = +-isGroupHomomorphism } - open GroupHomomorphism +-groupHomomorphism public - *-monoidHomomorphism : MonoidHomomorphism A.*-monoid B.*-monoid *-monoidHomomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism } @@ -213,8 +198,6 @@ record QuasigroupHomomorphism (A : Quasigroup a ℓa) (B : Quasigroup b ℓb) : magmaHomomorphism : MagmaHomomorphism A.magma B.magma magmaHomomorphism = record { isMagmaHomomorphism = ∙-isMagmaHomomorphism } - open MagmaHomomorphism magmaHomomorphism public - ------------------------------------------------------------------------ -- Morphisms between Loops ------------------------------------------------------------------------ From df9b2da61c0506e5ef982e7f143a58ab16d206da Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 16 May 2024 10:35:21 +0100 Subject: [PATCH 10/27] add bundled `Composition` of homomorphisms --- CHANGELOG.md | 49 ++++++ .../Morphism/Construct/Composition.agda | 166 ++++++++++++++++++ 2 files changed, 215 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 92612e2de7..564318d897 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -244,6 +244,55 @@ Additions to existing modules rawModule : RawModule R c ℓ ``` +* In `Algebra.Morphism.Construct.Composition`: + ``` + magmaHomomorphism : MagmaHomomorphism M₁ M₂ → + MagmaHomomorphism M₂ M₃ → + MagmaHomomorphism M₁ M₃ + monoidHomomorphism : MonoidHomomorphism M₁ M₂ → + MagmaHomomorphism M₂ M₃ → + MagmaHomomorphism M₁ M₃ + groupHomomorphism : GroupHomomorphism M₁ M₂ → + MagmaHomomorphism M₂ M₃ → + MagmaHomomorphism M₁ M₃ + nearSemiringHomomorphism : NearSemiringHomomorphism M₁ M₂ → + NearSemiringHomomorphism M₂ M₃ → + NearSemiringHomomorphism M₁ M₃ + semiringHomomorphism : SemiringHomomorphism M₁ M₂ → + SemiringHomomorphism M₂ M₃ → + SemiringHomomorphism M₁ M₃ + kleeneAlgebraHomomorphism : KleeneAlgebraHomomorphism M₁ M₂ → + KleeneAlgebraHomomorphism M₂ M₃ → + KleeneAlgebraHomomorphism M₁ M₃ + ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M₁ M₂ → + RingWithoutOneHomomorphism M₂ M₃ → + RingWithoutOneHomomorphism M₁ M₃ + ringHomomorphism : RingHomomorphism M₁ M₂ → + RingHomomorphism M₂ M₃ → + RingHomomorphism M₁ M₃ + quasigroupHomomorphism : QuasigroupHomomorphism M₁ M₂ → + QuasigroupHomomorphism M₂ M₃ → + QuasigroupHomomorphism M₁ M₃ + loopHomomorphism : LoopHomomorphism M₁ M₂ → + LoopHomomorphism M₂ M₃ → + LoopHomomorphism M₁ M₃ + ``` + +* In `Algebra.Morphism.Construct.Identity`: + ``` + magmaHomomorphism : MagmaHomomorphism M M + monoidHomomorphism : MonoidHomomorphism M M + groupHomomorphism : GroupHomomorphism M M + nearSemiringHomomorphism : NearSemiringHomomorphism M M + semiringHomomorphism : SemiringHomomorphism M M + kleeneAlgebraHomomorphism : KleeneAlgebraHomomorphism M M + nearSemiringHomomorphism : NearSemiringHomomorphism M M + ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M M + ringHomomorphism : RingHomomorphism M M + quasigroupHomomorphism : QuasigroupHomomorphism M M + loopHomomorphism : LoopHomomorphism M M + ``` + * In `Algebra.Morphism.Structures` ```agda module SuccessorSetMorphisms (N₁ : RawSuccessorSet a ℓ₁) (N₂ : RawSuccessorSet b ℓ₂) where diff --git a/src/Algebra/Morphism/Construct/Composition.agda b/src/Algebra/Morphism/Construct/Composition.agda index 17d5f2798b..d16180bd98 100644 --- a/src/Algebra/Morphism/Construct/Composition.agda +++ b/src/Algebra/Morphism/Construct/Composition.agda @@ -9,6 +9,7 @@ module Algebra.Morphism.Construct.Composition where open import Algebra.Bundles +open import Algebra.Morphism.Bundles open import Algebra.Morphism.Structures open import Function.Base using (_∘_) import Function.Construct.Composition as Func @@ -423,3 +424,168 @@ module _ {K₁ : RawKleeneAlgebra a ℓ₁} ; surjective = Func.surjective (_≈_ K₁) (_≈_ K₂) (_≈_ K₃) F.surjective G.surjective } where module F = IsKleeneAlgebraIsomorphism f-iso; module G = IsKleeneAlgebraIsomorphism g-iso +----------------------------------------------------------------------- +-- Bundled morphisms between algebras +------------------------------------------------------------------------ + +-- Magma + +module _ {M₁ : Magma a ℓ₁} + {M₂ : Magma b ℓ₂} + {M₃ : Magma c ℓ₃} + (h : MagmaHomomorphism M₁ M₂) + (k : MagmaHomomorphism M₂ M₃) + where + + private + module H = MagmaHomomorphism h + module K = MagmaHomomorphism k + + magmaHomomorphism : MagmaHomomorphism M₁ M₃ + magmaHomomorphism = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isMagmaHomomorphism = isMagmaHomomorphism (Magma.trans M₃) H.isMagmaHomomorphism K.isMagmaHomomorphism } + +-- Monoid + +module _ {M₁ : Monoid a ℓ₁} + {M₂ : Monoid b ℓ₂} + {M₃ : Monoid c ℓ₃} + (h : MonoidHomomorphism M₁ M₂) + (k : MonoidHomomorphism M₂ M₃) + where + + private + module H = MonoidHomomorphism h + module K = MonoidHomomorphism k + + monoidHomomorphism : MonoidHomomorphism M₁ M₃ + monoidHomomorphism = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isMonoidHomomorphism = isMonoidHomomorphism (Monoid.trans M₃) H.isMonoidHomomorphism K.isMonoidHomomorphism } + +-- Group + +module _ {M₁ : Group a ℓ₁} + {M₂ : Group b ℓ₂} + {M₃ : Group c ℓ₃} + (h : GroupHomomorphism M₁ M₂) + (k : GroupHomomorphism M₂ M₃) + where + + private + module H = GroupHomomorphism h + module K = GroupHomomorphism k + + groupHomomorphism : GroupHomomorphism M₁ M₃ + groupHomomorphism = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isGroupHomomorphism = isGroupHomomorphism (Group.trans M₃) H.isGroupHomomorphism K.isGroupHomomorphism } + +-- NearSemiring + +module _ {M₁ : NearSemiring a ℓ₁} + {M₂ : NearSemiring b ℓ₂} + {M₃ : NearSemiring c ℓ₃} + (h : NearSemiringHomomorphism M₁ M₂) + (k : NearSemiringHomomorphism M₂ M₃) + where + + private + module H = NearSemiringHomomorphism h + module K = NearSemiringHomomorphism k + + nearSemiringHomomorphism : NearSemiringHomomorphism M₁ M₃ + nearSemiringHomomorphism = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isNearSemiringHomomorphism = isNearSemiringHomomorphism (NearSemiring.trans M₃) H.isNearSemiringHomomorphism K.isNearSemiringHomomorphism } + +-- Semiring + +module _ {M₁ : Semiring a ℓ₁} + {M₂ : Semiring b ℓ₂} + {M₃ : Semiring c ℓ₃} + (h : SemiringHomomorphism M₁ M₂) + (k : SemiringHomomorphism M₂ M₃) + where + + private + module H = SemiringHomomorphism h + module K = SemiringHomomorphism k + + semiringHomomorphism : SemiringHomomorphism M₁ M₃ + semiringHomomorphism = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isSemiringHomomorphism = isSemiringHomomorphism (Semiring.trans M₃) H.isSemiringHomomorphism K.isSemiringHomomorphism } + +-- RingWithoutOne + +module _ {M₁ : RingWithoutOne a ℓ₁} + {M₂ : RingWithoutOne b ℓ₂} + {M₃ : RingWithoutOne c ℓ₃} + (h : RingWithoutOneHomomorphism M₁ M₂) + (k : RingWithoutOneHomomorphism M₂ M₃) + where + + private + module H = RingWithoutOneHomomorphism h + module K = RingWithoutOneHomomorphism k + + ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M₁ M₃ + ringWithoutOneHomomorphism = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism (RingWithoutOne.trans M₃) H.isRingWithoutOneHomomorphism K.isRingWithoutOneHomomorphism } + +-- Ring + +module _ {M₁ : Ring a ℓ₁} + {M₂ : Ring b ℓ₂} + {M₃ : Ring c ℓ₃} + (h : RingHomomorphism M₁ M₂) + (k : RingHomomorphism M₂ M₃) + where + + private + module H = RingHomomorphism h + module K = RingHomomorphism k + + ringHomomorphism : RingHomomorphism M₁ M₃ + ringHomomorphism = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isRingHomomorphism = isRingHomomorphism (Ring.trans M₃) H.isRingHomomorphism K.isRingHomomorphism } + +-- Quasigroup + +module _ {M₁ : Quasigroup a ℓ₁} + {M₂ : Quasigroup b ℓ₂} + {M₃ : Quasigroup c ℓ₃} + (h : QuasigroupHomomorphism M₁ M₂) + (k : QuasigroupHomomorphism M₂ M₃) + where + + private + module H = QuasigroupHomomorphism h + module K = QuasigroupHomomorphism k + + quasigroupHomomorphism : QuasigroupHomomorphism M₁ M₃ + quasigroupHomomorphism = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isQuasigroupHomomorphism = isQuasigroupHomomorphism (Quasigroup.trans M₃) H.isQuasigroupHomomorphism K.isQuasigroupHomomorphism } + +-- Loop + +module _ {M₁ : Loop a ℓ₁} + {M₂ : Loop b ℓ₂} + {M₃ : Loop c ℓ₃} + (h : LoopHomomorphism M₁ M₂) + (k : LoopHomomorphism M₂ M₃) + where + + private + module H = LoopHomomorphism h + module K = LoopHomomorphism k + + loopHomomorphism : LoopHomomorphism M₁ M₃ + loopHomomorphism = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isLoopHomomorphism = isLoopHomomorphism (Loop.trans M₃) H.isLoopHomomorphism K.isLoopHomomorphism } From 6c44f5b5de9d4868ef4eb150c45d413e2963a9ab Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 16 May 2024 12:37:00 +0100 Subject: [PATCH 11/27] more exported sub-bundles --- src/Algebra/Morphism/Bundles.agda | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda index c774bf695e..6341e03da8 100644 --- a/src/Algebra/Morphism/Bundles.agda +++ b/src/Algebra/Morphism/Bundles.agda @@ -114,6 +114,12 @@ record SemiringHomomorphism (A : Semiring a ℓa) (B : Semiring b ℓb) : Set (a open IsSemiringHomomorphism isSemiringHomomorphism public + nearSemiringHomomorphism : NearSemiringHomomorphism A.nearSemiring B.nearSemiring + nearSemiringHomomorphism = record { isNearSemiringHomomorphism = isNearSemiringHomomorphism } + + open NearSemiringHomomorphism nearSemiringHomomorphism public + using (*-magmaHomomorphism; +-monoidHomomorphism) + *-monoidHomomorphism : MonoidHomomorphism A.*-monoid B.*-monoid *-monoidHomomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism } From 150daaa6547cbd50d64240aaab03fc83bbd63b15 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 16 May 2024 12:49:58 +0100 Subject: [PATCH 12/27] removed redundant anonymous `module`s --- src/Algebra/Morphism/Construct/Identity.agda | 139 ++++++++----------- 1 file changed, 61 insertions(+), 78 deletions(-) diff --git a/src/Algebra/Morphism/Construct/Identity.agda b/src/Algebra/Morphism/Construct/Identity.agda index fc1a7d1b2c..da043514f8 100644 --- a/src/Algebra/Morphism/Construct/Identity.agda +++ b/src/Algebra/Morphism/Construct/Identity.agda @@ -282,130 +282,113 @@ module _ (K : RawKleeneAlgebra c ℓ) (open RawKleeneAlgebra K) (refl : Reflexiv -- Magma -module _ (M : Magma c ℓ) where - +magmaHomomorphism : (M : Magma c ℓ) → MagmaHomomorphism M M +magmaHomomorphism M = record + { ⟦_⟧ = id + ; isMagmaHomomorphism = isMagmaHomomorphism rawMagma refl + } + where open Magma M using (rawMagma; refl) open MagmaMorphisms rawMagma rawMagma - magmaHomomorphism : MagmaHomomorphism M M - magmaHomomorphism = record - { ⟦_⟧ = id - ; isMagmaHomomorphism = isMagmaHomomorphism rawMagma refl - } -- Monoid -module _ (M : Monoid c ℓ) where - +monoidHomomorphism : (M : Monoid c ℓ) → MonoidHomomorphism M M +monoidHomomorphism M = record + { ⟦_⟧ = id + ; isMonoidHomomorphism = isMonoidHomomorphism rawMonoid refl + } + where open Monoid M using (rawMonoid; refl) open MonoidMorphisms rawMonoid rawMonoid - monoidHomomorphism : MonoidHomomorphism M M - monoidHomomorphism = record - { ⟦_⟧ = id - ; isMonoidHomomorphism = isMonoidHomomorphism rawMonoid refl - } - -- Group -module _ (M : Group c ℓ) where - +groupHomomorphism : (M : Group c ℓ) → GroupHomomorphism M M +groupHomomorphism M = record + { ⟦_⟧ = id + ; isGroupHomomorphism = isGroupHomomorphism rawGroup refl + } + where open Group M using (rawGroup; refl) open GroupMorphisms rawGroup rawGroup - groupHomomorphism : GroupHomomorphism M M - groupHomomorphism = record - { ⟦_⟧ = id - ; isGroupHomomorphism = isGroupHomomorphism rawGroup refl - } - -- NearSemiring -module _ (M : NearSemiring c ℓ) where - +nearSemiringHomomorphism : (M : NearSemiring c ℓ) → NearSemiringHomomorphism M M +nearSemiringHomomorphism M = record + { ⟦_⟧ = id + ; isNearSemiringHomomorphism = isNearSemiringHomomorphism rawNearSemiring refl + } + where open NearSemiring M using (rawNearSemiring; refl) open NearSemiringMorphisms rawNearSemiring rawNearSemiring - nearSemiringHomomorphism : NearSemiringHomomorphism M M - nearSemiringHomomorphism = record - { ⟦_⟧ = id - ; isNearSemiringHomomorphism = isNearSemiringHomomorphism rawNearSemiring refl - } - -- Semiring -module _ (M : Semiring c ℓ) where - +semiringHomomorphism : (M : Semiring c ℓ) → SemiringHomomorphism M M +semiringHomomorphism M = record + { ⟦_⟧ = id + ; isSemiringHomomorphism = isSemiringHomomorphism rawSemiring refl + } + where open Semiring M using (rawSemiring; refl) open SemiringMorphisms rawSemiring rawSemiring - semiringHomomorphism : SemiringHomomorphism M M - semiringHomomorphism = record - { ⟦_⟧ = id - ; isSemiringHomomorphism = isSemiringHomomorphism rawSemiring refl - } - -- KleeneAlgebra -module _ (M : KleeneAlgebra c ℓ) where - +kleeneAlgebraHomomorphism : (M : KleeneAlgebra c ℓ) → KleeneAlgebraHomomorphism M M +kleeneAlgebraHomomorphism M = record + { ⟦_⟧ = id + ; isKleeneAlgebraHomomorphism = isKleeneAlgebraHomomorphism rawKleeneAlgebra refl + } + where open KleeneAlgebra M using (rawKleeneAlgebra; refl) open KleeneAlgebraMorphisms rawKleeneAlgebra rawKleeneAlgebra - kleeneAlgebraHomomorphism : KleeneAlgebraHomomorphism M M - kleeneAlgebraHomomorphism = record - { ⟦_⟧ = id - ; isKleeneAlgebraHomomorphism = isKleeneAlgebraHomomorphism rawKleeneAlgebra refl - } - -- RingWithoutOne -module _ (M : RingWithoutOne c ℓ) where - +ringWithoutOneHomomorphism : (M : RingWithoutOne c ℓ) → RingWithoutOneHomomorphism M M +ringWithoutOneHomomorphism M = record + { ⟦_⟧ = id + ; isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism rawRingWithoutOne refl + } + where open RingWithoutOne M using (rawRingWithoutOne; refl) open RingWithoutOneMorphisms rawRingWithoutOne rawRingWithoutOne - ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M M - ringWithoutOneHomomorphism = record - { ⟦_⟧ = id - ; isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism rawRingWithoutOne refl - } - -- Ring -module _ (M : Ring c ℓ) where - +ringHomomorphism : (M : Ring c ℓ) → RingHomomorphism M M +ringHomomorphism M = record + { ⟦_⟧ = id + ; isRingHomomorphism = isRingHomomorphism rawRing refl + } + where open Ring M using (rawRing; refl) open RingMorphisms rawRing rawRing - ringHomomorphism : RingHomomorphism M M - ringHomomorphism = record - { ⟦_⟧ = id - ; isRingHomomorphism = isRingHomomorphism rawRing refl - } -- Quasigroup -module _ (M : Quasigroup c ℓ) where - +quasigroupHomomorphism : (M : Quasigroup c ℓ) → QuasigroupHomomorphism M M +quasigroupHomomorphism M = record + { ⟦_⟧ = id + ; isQuasigroupHomomorphism = isQuasigroupHomomorphism rawQuasigroup refl + } + where open Quasigroup M using (rawQuasigroup; refl) open QuasigroupMorphisms rawQuasigroup rawQuasigroup - quasigroupHomomorphism : QuasigroupHomomorphism M M - quasigroupHomomorphism = record - { ⟦_⟧ = id - ; isQuasigroupHomomorphism = isQuasigroupHomomorphism rawQuasigroup refl - } - -- Loop -module _ (M : Loop c ℓ) where - +loopHomomorphism : (M : Loop c ℓ) → LoopHomomorphism M M +loopHomomorphism M = record + { ⟦_⟧ = id + ; isLoopHomomorphism = isLoopHomomorphism rawLoop refl + } + where open Loop M using (rawLoop; refl) open LoopMorphisms rawLoop rawLoop - - loopHomomorphism : LoopHomomorphism M M - loopHomomorphism = record - { ⟦_⟧ = id - ; isLoopHomomorphism = isLoopHomomorphism rawLoop refl - } + From 454d8ed37fd50e1ff33babb31498e91500bfc4b8 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 16 May 2024 13:17:58 +0100 Subject: [PATCH 13/27] removed redundant anonymous `module`s --- .../Morphism/Construct/Composition.agda | 225 +++++++----------- src/Algebra/Morphism/Construct/Identity.agda | 2 - 2 files changed, 90 insertions(+), 137 deletions(-) diff --git a/src/Algebra/Morphism/Construct/Composition.agda b/src/Algebra/Morphism/Construct/Composition.agda index d16180bd98..fcb4ce530e 100644 --- a/src/Algebra/Morphism/Construct/Composition.agda +++ b/src/Algebra/Morphism/Construct/Composition.agda @@ -430,162 +430,117 @@ module _ {K₁ : RawKleeneAlgebra a ℓ₁} -- Magma -module _ {M₁ : Magma a ℓ₁} - {M₂ : Magma b ℓ₂} - {M₃ : Magma c ℓ₃} - (h : MagmaHomomorphism M₁ M₂) - (k : MagmaHomomorphism M₂ M₃) - where - - private - module H = MagmaHomomorphism h - module K = MagmaHomomorphism k - - magmaHomomorphism : MagmaHomomorphism M₁ M₃ - magmaHomomorphism = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isMagmaHomomorphism = isMagmaHomomorphism (Magma.trans M₃) H.isMagmaHomomorphism K.isMagmaHomomorphism } +magmaHomomorphism : {M₁ : Magma a ℓ₁} {M₂ : Magma b ℓ₂} {M₃ : Magma c ℓ₃} → + (h : MagmaHomomorphism M₁ M₂) → + (k : MagmaHomomorphism M₂ M₃) → + MagmaHomomorphism M₁ M₃ +magmaHomomorphism {M₃ = M₃} h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isMagmaHomomorphism = isMagmaHomomorphism (Magma.trans M₃) H.isMagmaHomomorphism K.isMagmaHomomorphism } + where + module H = MagmaHomomorphism h + module K = MagmaHomomorphism k -- Monoid -module _ {M₁ : Monoid a ℓ₁} - {M₂ : Monoid b ℓ₂} - {M₃ : Monoid c ℓ₃} - (h : MonoidHomomorphism M₁ M₂) - (k : MonoidHomomorphism M₂ M₃) - where - - private - module H = MonoidHomomorphism h - module K = MonoidHomomorphism k - - monoidHomomorphism : MonoidHomomorphism M₁ M₃ - monoidHomomorphism = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isMonoidHomomorphism = isMonoidHomomorphism (Monoid.trans M₃) H.isMonoidHomomorphism K.isMonoidHomomorphism } +monoidHomomorphism : {M₁ : Monoid a ℓ₁} {M₂ : Monoid b ℓ₂} {M₃ : Monoid c ℓ₃} → + (h : MonoidHomomorphism M₁ M₂) → + (k : MonoidHomomorphism M₂ M₃) → + MonoidHomomorphism M₁ M₃ +monoidHomomorphism {M₃ = M₃} h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isMonoidHomomorphism = isMonoidHomomorphism (Monoid.trans M₃) H.isMonoidHomomorphism K.isMonoidHomomorphism } + where + module H = MonoidHomomorphism h + module K = MonoidHomomorphism k -- Group -module _ {M₁ : Group a ℓ₁} - {M₂ : Group b ℓ₂} - {M₃ : Group c ℓ₃} - (h : GroupHomomorphism M₁ M₂) - (k : GroupHomomorphism M₂ M₃) - where - - private - module H = GroupHomomorphism h - module K = GroupHomomorphism k - - groupHomomorphism : GroupHomomorphism M₁ M₃ - groupHomomorphism = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isGroupHomomorphism = isGroupHomomorphism (Group.trans M₃) H.isGroupHomomorphism K.isGroupHomomorphism } +groupHomomorphism : {M₁ : Group a ℓ₁} {M₂ : Group b ℓ₂} {M₃ : Group c ℓ₃} → + (h : GroupHomomorphism M₁ M₂) → + (k : GroupHomomorphism M₂ M₃) → + GroupHomomorphism M₁ M₃ +groupHomomorphism {M₃ = M₃} h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isGroupHomomorphism = isGroupHomomorphism (Group.trans M₃) H.isGroupHomomorphism K.isGroupHomomorphism } + where + module H = GroupHomomorphism h + module K = GroupHomomorphism k -- NearSemiring -module _ {M₁ : NearSemiring a ℓ₁} - {M₂ : NearSemiring b ℓ₂} - {M₃ : NearSemiring c ℓ₃} - (h : NearSemiringHomomorphism M₁ M₂) - (k : NearSemiringHomomorphism M₂ M₃) - where - - private - module H = NearSemiringHomomorphism h - module K = NearSemiringHomomorphism k - - nearSemiringHomomorphism : NearSemiringHomomorphism M₁ M₃ - nearSemiringHomomorphism = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isNearSemiringHomomorphism = isNearSemiringHomomorphism (NearSemiring.trans M₃) H.isNearSemiringHomomorphism K.isNearSemiringHomomorphism } +nearSemiringHomomorphism : {M₁ : NearSemiring a ℓ₁} {M₂ : NearSemiring b ℓ₂} {M₃ : NearSemiring c ℓ₃} → + (h : NearSemiringHomomorphism M₁ M₂) → + (k : NearSemiringHomomorphism M₂ M₃) → + NearSemiringHomomorphism M₁ M₃ +nearSemiringHomomorphism {M₃ = M₃} h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isNearSemiringHomomorphism = isNearSemiringHomomorphism (NearSemiring.trans M₃) H.isNearSemiringHomomorphism K.isNearSemiringHomomorphism } + where + module H = NearSemiringHomomorphism h + module K = NearSemiringHomomorphism k -- Semiring -module _ {M₁ : Semiring a ℓ₁} - {M₂ : Semiring b ℓ₂} - {M₃ : Semiring c ℓ₃} - (h : SemiringHomomorphism M₁ M₂) - (k : SemiringHomomorphism M₂ M₃) - where - - private - module H = SemiringHomomorphism h - module K = SemiringHomomorphism k - - semiringHomomorphism : SemiringHomomorphism M₁ M₃ - semiringHomomorphism = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isSemiringHomomorphism = isSemiringHomomorphism (Semiring.trans M₃) H.isSemiringHomomorphism K.isSemiringHomomorphism } +semiringHomomorphism : {M₁ : Semiring a ℓ₁} {M₂ : Semiring b ℓ₂} {M₃ : Semiring c ℓ₃} → + (h : SemiringHomomorphism M₁ M₂) → + (k : SemiringHomomorphism M₂ M₃) → + SemiringHomomorphism M₁ M₃ +semiringHomomorphism {M₃ = M₃} h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isSemiringHomomorphism = isSemiringHomomorphism (Semiring.trans M₃) H.isSemiringHomomorphism K.isSemiringHomomorphism } + where + module H = SemiringHomomorphism h + module K = SemiringHomomorphism k -- RingWithoutOne -module _ {M₁ : RingWithoutOne a ℓ₁} - {M₂ : RingWithoutOne b ℓ₂} - {M₃ : RingWithoutOne c ℓ₃} - (h : RingWithoutOneHomomorphism M₁ M₂) - (k : RingWithoutOneHomomorphism M₂ M₃) - where - - private - module H = RingWithoutOneHomomorphism h - module K = RingWithoutOneHomomorphism k - - ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M₁ M₃ - ringWithoutOneHomomorphism = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism (RingWithoutOne.trans M₃) H.isRingWithoutOneHomomorphism K.isRingWithoutOneHomomorphism } +ringWithoutOneHomomorphism : {M₁ : RingWithoutOne a ℓ₁} {M₂ : RingWithoutOne b ℓ₂} {M₃ : RingWithoutOne c ℓ₃} → + (h : RingWithoutOneHomomorphism M₁ M₂) → + (k : RingWithoutOneHomomorphism M₂ M₃) → + RingWithoutOneHomomorphism M₁ M₃ +ringWithoutOneHomomorphism {M₃ = M₃} h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism (RingWithoutOne.trans M₃) H.isRingWithoutOneHomomorphism K.isRingWithoutOneHomomorphism } + where + module H = RingWithoutOneHomomorphism h + module K = RingWithoutOneHomomorphism k -- Ring -module _ {M₁ : Ring a ℓ₁} - {M₂ : Ring b ℓ₂} - {M₃ : Ring c ℓ₃} - (h : RingHomomorphism M₁ M₂) - (k : RingHomomorphism M₂ M₃) - where - - private - module H = RingHomomorphism h - module K = RingHomomorphism k - - ringHomomorphism : RingHomomorphism M₁ M₃ - ringHomomorphism = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isRingHomomorphism = isRingHomomorphism (Ring.trans M₃) H.isRingHomomorphism K.isRingHomomorphism } +ringHomomorphism : {M₁ : Ring a ℓ₁} {M₂ : Ring b ℓ₂} {M₃ : Ring c ℓ₃} → + (h : RingHomomorphism M₁ M₂) → + (k : RingHomomorphism M₂ M₃) → + RingHomomorphism M₁ M₃ +ringHomomorphism {M₃ = M₃} h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isRingHomomorphism = isRingHomomorphism (Ring.trans M₃) H.isRingHomomorphism K.isRingHomomorphism } + where + module H = RingHomomorphism h + module K = RingHomomorphism k -- Quasigroup -module _ {M₁ : Quasigroup a ℓ₁} - {M₂ : Quasigroup b ℓ₂} - {M₃ : Quasigroup c ℓ₃} - (h : QuasigroupHomomorphism M₁ M₂) - (k : QuasigroupHomomorphism M₂ M₃) - where - - private - module H = QuasigroupHomomorphism h - module K = QuasigroupHomomorphism k - - quasigroupHomomorphism : QuasigroupHomomorphism M₁ M₃ - quasigroupHomomorphism = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isQuasigroupHomomorphism = isQuasigroupHomomorphism (Quasigroup.trans M₃) H.isQuasigroupHomomorphism K.isQuasigroupHomomorphism } +quasigroupHomomorphism : {M₁ : Quasigroup a ℓ₁} {M₂ : Quasigroup b ℓ₂} {M₃ : Quasigroup c ℓ₃} → + (h : QuasigroupHomomorphism M₁ M₂) → + (k : QuasigroupHomomorphism M₂ M₃) → + QuasigroupHomomorphism M₁ M₃ +quasigroupHomomorphism {M₃ = M₃} h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isQuasigroupHomomorphism = isQuasigroupHomomorphism (Quasigroup.trans M₃) H.isQuasigroupHomomorphism K.isQuasigroupHomomorphism } + where + module H = QuasigroupHomomorphism h + module K = QuasigroupHomomorphism k -- Loop -module _ {M₁ : Loop a ℓ₁} - {M₂ : Loop b ℓ₂} - {M₃ : Loop c ℓ₃} - (h : LoopHomomorphism M₁ M₂) - (k : LoopHomomorphism M₂ M₃) - where - - private - module H = LoopHomomorphism h - module K = LoopHomomorphism k - - loopHomomorphism : LoopHomomorphism M₁ M₃ - loopHomomorphism = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isLoopHomomorphism = isLoopHomomorphism (Loop.trans M₃) H.isLoopHomomorphism K.isLoopHomomorphism } +loopHomomorphism : {M₁ : Loop a ℓ₁} {M₂ : Loop b ℓ₂} {M₃ : Loop c ℓ₃} → + (h : LoopHomomorphism M₁ M₂) → + (k : LoopHomomorphism M₂ M₃) → + LoopHomomorphism M₁ M₃ +loopHomomorphism {M₃ = M₃} h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isLoopHomomorphism = isLoopHomomorphism (Loop.trans M₃) H.isLoopHomomorphism K.isLoopHomomorphism } + where + module H = LoopHomomorphism h + module K = LoopHomomorphism k diff --git a/src/Algebra/Morphism/Construct/Identity.agda b/src/Algebra/Morphism/Construct/Identity.agda index da043514f8..38407820ca 100644 --- a/src/Algebra/Morphism/Construct/Identity.agda +++ b/src/Algebra/Morphism/Construct/Identity.agda @@ -291,7 +291,6 @@ magmaHomomorphism M = record open Magma M using (rawMagma; refl) open MagmaMorphisms rawMagma rawMagma - -- Monoid monoidHomomorphism : (M : Monoid c ℓ) → MonoidHomomorphism M M @@ -391,4 +390,3 @@ loopHomomorphism M = record where open Loop M using (rawLoop; refl) open LoopMorphisms rawLoop rawLoop - From 04fa1f40cfe160935d20791dcf4d247d59783764 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 17 May 2024 08:50:33 +0100 Subject: [PATCH 14/27] add `isNearSemiring` to `IsRingWithoutOne` plus knock-on re-exports --- src/Algebra/Structures.agda | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 3cdc55a4b5..40ad6779c8 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -726,6 +726,18 @@ record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ zero : Zero 0# * zero = zeroˡ , zeroʳ + isNearSemiring′ : IsNearSemiring + * 0# + isNearSemiring′ = record + { +-isMonoid = +-isMonoid + ; *-cong = *-cong + ; *-assoc = *-assoc + ; distribʳ = distribʳ + ; zeroˡ = zeroˡ + } + + open IsNearSemiring isNearSemiring′ public + using (*-isMagma; *-isSemigroup; *-congˡ; *-congʳ) +{- *-isMagma : IsMagma * *-isMagma = record { isEquivalence = isEquivalence @@ -744,7 +756,7 @@ record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ ( ∙-congˡ to *-congˡ ; ∙-congʳ to *-congʳ ) - +-} ------------------------------------------------------------------------ -- Structures with 2 binary operations, 1 unary operation & 2 elements ------------------------------------------------------------------------ From 71e8e2e465219336213a89ca014935e44fbb5d55 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 17 May 2024 09:00:26 +0100 Subject: [PATCH 15/27] add `nearSemiring` to `RingWithoutOne` plus knock-on re-exports --- CHANGELOG.md | 10 +++++++++- src/Algebra/Bundles.agda | 13 ++++++------- 2 files changed, 15 insertions(+), 8 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 564318d897..4558cd2c4d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -195,8 +195,10 @@ Additions to existing modules +-rawGroup : RawGroup _ _ ``` -* Exporting `RawRingWithoutOne` substructure from `Algebra.Bundles.RingWithoutOne`: +* Exporting `RawRingWithoutOne` and `NearSemiring` subbundles from + `Algebra.Bundles.RingWithoutOne`: ```agda + nearSemiring : NearSemiring _ _ rawRingWithoutOne : RawRingWithoutOne _ _ ``` @@ -349,6 +351,7 @@ Additions to existing modules * In `Algebra.Structures` ```agda record IsSuccessorSet (suc# : Op₁ A) (zero# : A) : Set _ + ``` * In `Algebra.Structures.IsGroup`: ```agda @@ -360,6 +363,11 @@ Additions to existing modules x \\ y = (x ⁻¹) ∙ y ``` +* In `Algebra.Structures.RingWithoutOne`: + ```agda + isNearSemiring : IsNearSemiring _ _ + ``` + * In `Algebra.Structures.IsCancellativeCommutativeSemiring` add the extra property as an exposed definition: ```agda diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 7eb34a72e6..c6b65fffac 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -878,22 +878,21 @@ record RingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where open IsRingWithoutOne isRingWithoutOne public + nearSemiring : NearSemiring _ _ + nearSemiring = record { isNearSemiring = isNearSemiring } + + open NearSemiring nearSemiring public + using (*-semigroup; *-magma) + +-abelianGroup : AbelianGroup _ _ +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup } - *-semigroup : Semigroup _ _ - *-semigroup = record { isSemigroup = *-isSemigroup } - open AbelianGroup +-abelianGroup public using () renaming (group to +-group; invertibleMagma to +-invertibleMagma; invertibleUnitalMagma to +-invertibleUnitalMagma) - open Semigroup *-semigroup public - using () - renaming (magma to *-magma) - rawRingWithoutOne : RawRingWithoutOne _ _ rawRingWithoutOne = record { _≈_ = _≈_ From 8e1c8a12229fdc48fd70adf608b0fe173e2c9652 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 17 May 2024 09:26:26 +0100 Subject: [PATCH 16/27] add `rawNearSemiring` to `RingWithoutOne` plus knock-on re-exports --- CHANGELOG.md | 13 ++++++++++--- src/Algebra/Bundles.agda | 2 +- src/Algebra/Bundles/Raw.agda | 20 +++++++++++--------- src/Algebra/Structures.agda | 27 ++++----------------------- 4 files changed, 26 insertions(+), 36 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4558cd2c4d..15f3aab65e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -178,14 +178,19 @@ Additions to existing modules record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) ``` +* In `Algebra.Bundles.KleeneAlgebra`: + ```agda + rawKleeneAlgebra : RawKleeneAlgebra _ _ + ``` + * In `Algebra.Bundles.Raw` ```agda record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) ``` -* Exporting `RawKleeneAlgebra` substructure from `Algebra.Bundles.KleeneAlgebra`: +* In `Algebra.Bundles.Raw.RawRingWithoutOne` ```agda - rawKleeneAlgebra : RawKleeneAlgebra _ _ + rawNearSemiring : RawNearSemiring c ℓ ``` * Exporting more `Raw` substructures from `Algebra.Bundles.Ring`: @@ -195,10 +200,11 @@ Additions to existing modules +-rawGroup : RawGroup _ _ ``` -* Exporting `RawRingWithoutOne` and `NearSemiring` subbundles from +* Exporting `RawRingWithoutOne` and `(Raw)NearSemiring` subbundles from `Algebra.Bundles.RingWithoutOne`: ```agda nearSemiring : NearSemiring _ _ + rawNearSemiring : RawNearSemiring _ _ rawRingWithoutOne : RawRingWithoutOne _ _ ``` @@ -301,6 +307,7 @@ Additions to existing modules record IsSuccessorSetHomomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ record IsSuccessorSetMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ record IsSuccessorSetIsomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ + ``` * In `Algebra.Properties.AbelianGroup`: ``` diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index c6b65fffac..68c3b3e32f 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -903,7 +903,7 @@ record RingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where } open RawRingWithoutOne rawRingWithoutOne public - using (+-rawGroup; *-rawMagma) + using (+-rawGroup; *-rawMagma; rawNearSemiring) ------------------------------------------------------------------------ diff --git a/src/Algebra/Bundles/Raw.agda b/src/Algebra/Bundles/Raw.agda index 5c99d02790..1947e3846d 100644 --- a/src/Algebra/Bundles/Raw.agda +++ b/src/Algebra/Bundles/Raw.agda @@ -174,6 +174,17 @@ record RawRingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where -_ : Op₁ Carrier 0# : Carrier + rawNearSemiring : RawNearSemiring c ℓ + rawNearSemiring = record + { _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; 0# = 0# + } + + open RawNearSemiring rawNearSemiring public + using (_≉_; *-rawMagma; +-rawMagma; +-rawMonoid) + +-rawGroup : RawGroup c ℓ +-rawGroup = record { _≈_ = _≈_ @@ -182,15 +193,6 @@ record RawRingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where ; _⁻¹ = -_ } - open RawGroup +-rawGroup public - using (_≉_) renaming (rawMagma to +-rawMagma; rawMonoid to +-rawMonoid) - - *-rawMagma : RawMagma c ℓ - *-rawMagma = record - { _≈_ = _≈_ - ; _∙_ = _*_ - } - ------------------------------------------------------------------------ -- Raw bundles with 2 binary operations, 1 unary operation & 2 elements ------------------------------------------------------------------------ diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 40ad6779c8..7b894c9497 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -726,8 +726,8 @@ record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ zero : Zero 0# * zero = zeroˡ , zeroʳ - isNearSemiring′ : IsNearSemiring + * 0# - isNearSemiring′ = record + isNearSemiring : IsNearSemiring + * 0# + isNearSemiring = record { +-isMonoid = +-isMonoid ; *-cong = *-cong ; *-assoc = *-assoc @@ -735,28 +735,9 @@ record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ ; zeroˡ = zeroˡ } - open IsNearSemiring isNearSemiring′ public + open IsNearSemiring isNearSemiring public using (*-isMagma; *-isSemigroup; *-congˡ; *-congʳ) -{- - *-isMagma : IsMagma * - *-isMagma = record - { isEquivalence = isEquivalence - ; ∙-cong = *-cong - } - - *-isSemigroup : IsSemigroup * - *-isSemigroup = record - { isMagma = *-isMagma - ; assoc = *-assoc - } - open IsSemigroup *-isSemigroup public - using () - renaming - ( ∙-congˡ to *-congˡ - ; ∙-congʳ to *-congʳ - ) --} ------------------------------------------------------------------------ -- Structures with 2 binary operations, 1 unary operation & 2 elements ------------------------------------------------------------------------ @@ -896,7 +877,7 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where } open IsSemiring isSemiring public - using (isNearSemiring; isSemiringWithoutOne) + using (isSemiringWithoutOne) record IsCommutativeRing From da9b808e19cb477d53b595130b7f2bad31d996ef Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 17 May 2024 09:37:39 +0100 Subject: [PATCH 17/27] lots more exported sub-structures and sub-bundles --- CHANGELOG.md | 5 +++++ src/Algebra/Morphism/Bundles.agda | 17 +++++++++++++---- src/Algebra/Morphism/Structures.agda | 15 ++++++++++++--- 3 files changed, 30 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 15f3aab65e..5c78228d35 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -309,6 +309,11 @@ Additions to existing modules record IsSuccessorSetIsomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ ``` +* In `Algebra.Morphism.Structures.RingWithoutOneMorphisms` + ```agda + isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧ + ``` + * In `Algebra.Properties.AbelianGroup`: ``` ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda index 6341e03da8..5134e3f7b9 100644 --- a/src/Algebra/Morphism/Bundles.agda +++ b/src/Algebra/Morphism/Bundles.agda @@ -76,6 +76,9 @@ record GroupHomomorphism (A : Group a ℓa) (B : Group b ℓb) : Set (a ⊔ b monoidHomomorphism : MonoidHomomorphism A.monoid B.monoid monoidHomomorphism = record { isMonoidHomomorphism = isMonoidHomomorphism } + open MonoidHomomorphism monoidHomomorphism public + using (magmaHomomorphism) + ------------------------------------------------------------------------ -- Morphisms between NearSemirings ------------------------------------------------------------------------ @@ -98,6 +101,9 @@ record NearSemiringHomomorphism (A : NearSemiring a ℓa) (B : NearSemiring b *-magmaHomomorphism : MagmaHomomorphism A.*-magma B.*-magma *-magmaHomomorphism = record { isMagmaHomomorphism = *-isMagmaHomomorphism } + open MonoidHomomorphism +-monoidHomomorphism public + renaming (magmaHomomorphism to +-magmaHomomorphism) + ------------------------------------------------------------------------ -- Morphisms between Semirings ------------------------------------------------------------------------ @@ -118,7 +124,7 @@ record SemiringHomomorphism (A : Semiring a ℓa) (B : Semiring b ℓb) : Set (a nearSemiringHomomorphism = record { isNearSemiringHomomorphism = isNearSemiringHomomorphism } open NearSemiringHomomorphism nearSemiringHomomorphism public - using (*-magmaHomomorphism; +-monoidHomomorphism) + using (*-magmaHomomorphism; +-monoidHomomorphism; +-magmaHomomorphism) *-monoidHomomorphism : MonoidHomomorphism A.*-monoid B.*-monoid *-monoidHomomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism } @@ -159,12 +165,15 @@ record RingWithoutOneHomomorphism (A : RingWithoutOne a ℓa) (B : RingWithoutOn open IsRingWithoutOneHomomorphism isRingWithoutOneHomomorphism public + nearSemiringHomomorphism : NearSemiringHomomorphism A.nearSemiring B.nearSemiring + nearSemiringHomomorphism = record { isNearSemiringHomomorphism = isNearSemiringHomomorphism } + + open NearSemiringHomomorphism nearSemiringHomomorphism public + using (*-magmaHomomorphism; +-magmaHomomorphism; +-monoidHomomorphism) + +-groupHomomorphism : GroupHomomorphism A.+-group B.+-group +-groupHomomorphism = record { isGroupHomomorphism = +-isGroupHomomorphism } - *-magmaHomomorphism : MagmaHomomorphism A.*-magma B.*-magma - *-magmaHomomorphism = record { isMagmaHomomorphism = *-isMagmaHomomorphism } - ------------------------------------------------------------------------ -- Morphisms between Rings ------------------------------------------------------------------------ diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index c352904be7..3d7d251378 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -405,17 +405,20 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi ( Carrier to A; _≈_ to _≈₁_ ; _*_ to _*₁_ ; *-rawMagma to *-rawMagma₁ - ; +-rawGroup to +-rawGroup₁) + ; +-rawGroup to +-rawGroup₁ + ; rawNearSemiring to rawNearSemiring₁) open RawRingWithoutOne R₂ renaming ( Carrier to B; _≈_ to _≈₂_ ; _*_ to _*₂_ ; *-rawMagma to *-rawMagma₂ - ; +-rawGroup to +-rawGroup₂) + ; +-rawGroup to +-rawGroup₂ + ; rawNearSemiring to rawNearSemiring₂) private module + = GroupMorphisms +-rawGroup₁ +-rawGroup₂ module * = MagmaMorphisms *-rawMagma₁ *-rawMagma₂ + module +* = NearSemiringMorphisms rawNearSemiring₁ rawNearSemiring₂ open MorphismDefinitions A B _≈₂_ @@ -425,7 +428,13 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi *-homo : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_ open +.IsGroupHomomorphism +-isGroupHomomorphism public - renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism) + renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism; isMonoidHomomorphism to +-isMonoidHomomorphism) + + isNearSemiringHomomorphism : +*.IsNearSemiringHomomorphism ⟦_⟧ + isNearSemiringHomomorphism = record + { +-isMonoidHomomorphism = +-isMonoidHomomorphism + ; *-homo = *-homo + } *-isMagmaHomomorphism : *.IsMagmaHomomorphism ⟦_⟧ *-isMagmaHomomorphism = record From 6d1c1c1b071db2b2d7f3d635f59af9f9cbf1da25 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 17 May 2024 10:20:01 +0100 Subject: [PATCH 18/27] fix bug: restrict exports --- src/Algebra/Morphism/Bundles.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda index 5134e3f7b9..ed90b6a7c6 100644 --- a/src/Algebra/Morphism/Bundles.agda +++ b/src/Algebra/Morphism/Bundles.agda @@ -102,6 +102,7 @@ record NearSemiringHomomorphism (A : NearSemiring a ℓa) (B : NearSemiring b *-magmaHomomorphism = record { isMagmaHomomorphism = *-isMagmaHomomorphism } open MonoidHomomorphism +-monoidHomomorphism public + using () renaming (magmaHomomorphism to +-magmaHomomorphism) ------------------------------------------------------------------------ From 88aa9f6f5d724227a2bef4e3c334407e45aa19fe Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 17 May 2024 10:46:25 +0100 Subject: [PATCH 19/27] lots more exported sub-structures and sub-bundles --- CHANGELOG.md | 5 +++++ src/Algebra/Morphism/Bundles.agda | 16 ++++++++++++---- src/Algebra/Morphism/Structures.agda | 9 +++++++++ 3 files changed, 26 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5c78228d35..aa51bca3c8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -309,6 +309,11 @@ Additions to existing modules record IsSuccessorSetIsomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ ``` +* In `Algebra.Morphism.Structures.RingMorphisms` + ```agda + isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧ + ``` + * In `Algebra.Morphism.Structures.RingWithoutOneMorphisms` ```agda isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧ diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda index ed90b6a7c6..0c7490c48c 100644 --- a/src/Algebra/Morphism/Bundles.agda +++ b/src/Algebra/Morphism/Bundles.agda @@ -190,11 +190,19 @@ record RingHomomorphism (A : Ring a ℓa) (B : Ring b ℓb) : Set (a ⊔ b ⊔ open IsRingHomomorphism isRingHomomorphism public - +-groupHomomorphism : GroupHomomorphism A.+-group B.+-group - +-groupHomomorphism = record { isGroupHomomorphism = +-isGroupHomomorphism } + ringWithoutOneHomomorphism : RingWithoutOneHomomorphism A.ringWithoutOne B.ringWithoutOne + ringWithoutOneHomomorphism = record { isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism } - *-monoidHomomorphism : MonoidHomomorphism A.*-monoid B.*-monoid - *-monoidHomomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism } + open RingWithoutOneHomomorphism ringWithoutOneHomomorphism public + using (+-groupHomomorphism) + + semiringHomomorphism : SemiringHomomorphism A.semiring B.semiring + semiringHomomorphism = record { isSemiringHomomorphism = isSemiringHomomorphism } + + open SemiringHomomorphism semiringHomomorphism public + using ( nearSemiringHomomorphism + ; *-monoidHomomorphism; *-magmaHomomorphism + ; +-monoidHomomorphism; +-magmaHomomorphism) ------------------------------------------------------------------------ -- Morphisms between Quasigroups diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index 3d7d251378..08d091d72a 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -498,6 +498,7 @@ module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where open RawRing R₁ renaming ( Carrier to A; _≈_ to _≈₁_ ; -_ to -₁_ + ; rawRingWithoutOne to rawRingWithoutOne₁ ; rawSemiring to rawSemiring₁ ; *-rawMonoid to *-rawMonoid₁ ; +-rawGroup to +-rawGroup₁) @@ -505,12 +506,14 @@ module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where open RawRing R₂ renaming ( Carrier to B; _≈_ to _≈₂_ ; -_ to -₂_ + ; rawRingWithoutOne to rawRingWithoutOne₂ ; rawSemiring to rawSemiring₂ ; *-rawMonoid to *-rawMonoid₂ ; +-rawGroup to +-rawGroup₂) module + = GroupMorphisms +-rawGroup₁ +-rawGroup₂ module * = MonoidMorphisms *-rawMonoid₁ *-rawMonoid₂ + module *+0 = RingWithoutOneMorphisms rawRingWithoutOne₁ rawRingWithoutOne₂ open MorphismDefinitions A B _≈₂_ open SemiringMorphisms rawSemiring₁ rawSemiring₂ @@ -529,6 +532,12 @@ module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where ; ⁻¹-homo = -‿homo } + isRingWithoutOneHomomorphism : *+0.IsRingWithoutOneHomomorphism ⟦_⟧ + isRingWithoutOneHomomorphism = record + { +-isGroupHomomorphism = +-isGroupHomomorphism + ; *-homo = *-homo + } + record IsRingMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isRingHomomorphism : IsRingHomomorphism ⟦_⟧ From 6c31fde04b4f5d815dde0d17cc38bb1436a20f6b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Jun 2024 11:59:43 +0100 Subject: [PATCH 20/27] refactor: `RawX` parameterisation --- src/Algebra/Morphism/Bundles.agda | 136 +++++++++++++++++------------- 1 file changed, 76 insertions(+), 60 deletions(-) diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda index 0c7490c48c..8bfe695825 100644 --- a/src/Algebra/Morphism/Bundles.agda +++ b/src/Algebra/Morphism/Bundles.agda @@ -2,17 +2,19 @@ -- The Agda standard library -- -- Bundled definitions of homomorphisms between algebras +-- +-- NB indexed by Raw bundles, just as IsXHomomorphism is ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Algebra.Morphism.Bundles where -open import Algebra.Bundles -- using (Magma) -open import Algebra.Morphism.Structures -- using (IsMagmaHomomorphism) +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) +--open import Relation.Binary.Morphism using (IsRelHomomorphism) +--open import Relation.Binary.Morphism.Bundles using (SetoidHomomorphism) private variable @@ -23,57 +25,60 @@ private -- Morphisms between Magmas ------------------------------------------------------------------------ -record MagmaHomomorphism (A : Magma a ℓa) (B : Magma b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where +record MagmaHomomorphism + (A : RawMagma a ℓa) (B : RawMagma b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) + where private - module A = Magma A - module B = Magma B + module A = RawMagma A + module B = RawMagma B field ⟦_⟧ : A.Carrier → B.Carrier - isMagmaHomomorphism : IsMagmaHomomorphism A.rawMagma B.rawMagma ⟦_⟧ + isMagmaHomomorphism : IsMagmaHomomorphism A B ⟦_⟧ open IsMagmaHomomorphism isMagmaHomomorphism public - setoidHomomorphism : SetoidHomomorphism A.setoid B.setoid - setoidHomomorphism = record { isRelHomomorphism = isRelHomomorphism } - ------------------------------------------------------------------------ -- Morphisms between Monoids ------------------------------------------------------------------------ -record MonoidHomomorphism (A : Monoid a ℓa) (B : Monoid b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where +record MonoidHomomorphism + (A : RawMonoid a ℓa) (B : RawMonoid b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) + where private - module A = Monoid A - module B = Monoid B + module A = RawMonoid A + module B = RawMonoid B field ⟦_⟧ : A.Carrier → B.Carrier - isMonoidHomomorphism : IsMonoidHomomorphism A.rawMonoid B.rawMonoid ⟦_⟧ + isMonoidHomomorphism : IsMonoidHomomorphism A B ⟦_⟧ open IsMonoidHomomorphism isMonoidHomomorphism public - magmaHomomorphism : MagmaHomomorphism A.magma B.magma + magmaHomomorphism : MagmaHomomorphism A.rawMagma B.rawMagma magmaHomomorphism = record { isMagmaHomomorphism = isMagmaHomomorphism } ------------------------------------------------------------------------ -- Morphisms between Groups ------------------------------------------------------------------------ -record GroupHomomorphism (A : Group a ℓa) (B : Group b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where +record GroupHomomorphism + (A : RawGroup a ℓa) (B : RawGroup b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) + where private - module A = Group A - module B = Group B + module A = RawGroup A + module B = RawGroup B field ⟦_⟧ : A.Carrier → B.Carrier - isGroupHomomorphism : IsGroupHomomorphism A.rawGroup B.rawGroup ⟦_⟧ + isGroupHomomorphism : IsGroupHomomorphism A B ⟦_⟧ open IsGroupHomomorphism isGroupHomomorphism public - monoidHomomorphism : MonoidHomomorphism A.monoid B.monoid + monoidHomomorphism : MonoidHomomorphism A.rawMonoid B.rawMonoid monoidHomomorphism = record { isMonoidHomomorphism = isMonoidHomomorphism } open MonoidHomomorphism monoidHomomorphism public @@ -83,22 +88,24 @@ record GroupHomomorphism (A : Group a ℓa) (B : Group b ℓb) : Set (a ⊔ b -- Morphisms between NearSemirings ------------------------------------------------------------------------ -record NearSemiringHomomorphism (A : NearSemiring a ℓa) (B : NearSemiring b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where +record NearSemiringHomomorphism + (A : RawNearSemiring a ℓa) (B : RawNearSemiring b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) + where private - module A = NearSemiring A - module B = NearSemiring B + module A = RawNearSemiring A + module B = RawNearSemiring B field ⟦_⟧ : A.Carrier → B.Carrier - isNearSemiringHomomorphism : IsNearSemiringHomomorphism A.rawNearSemiring B.rawNearSemiring ⟦_⟧ + isNearSemiringHomomorphism : IsNearSemiringHomomorphism A B ⟦_⟧ open IsNearSemiringHomomorphism isNearSemiringHomomorphism public - +-monoidHomomorphism : MonoidHomomorphism A.+-monoid B.+-monoid + +-monoidHomomorphism : MonoidHomomorphism A.+-rawMonoid B.+-rawMonoid +-monoidHomomorphism = record { isMonoidHomomorphism = +-isMonoidHomomorphism } - *-magmaHomomorphism : MagmaHomomorphism A.*-magma B.*-magma + *-magmaHomomorphism : MagmaHomomorphism A.*-rawMagma B.*-rawMagma *-magmaHomomorphism = record { isMagmaHomomorphism = *-isMagmaHomomorphism } open MonoidHomomorphism +-monoidHomomorphism public @@ -109,43 +116,47 @@ record NearSemiringHomomorphism (A : NearSemiring a ℓa) (B : NearSemiring b -- Morphisms between Semirings ------------------------------------------------------------------------ -record SemiringHomomorphism (A : Semiring a ℓa) (B : Semiring b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where +record SemiringHomomorphism + (A : RawSemiring a ℓa) (B : RawSemiring b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) + where private - module A = Semiring A - module B = Semiring B + module A = RawSemiring A + module B = RawSemiring B field ⟦_⟧ : A.Carrier → B.Carrier - isSemiringHomomorphism : IsSemiringHomomorphism A.rawSemiring B.rawSemiring ⟦_⟧ + isSemiringHomomorphism : IsSemiringHomomorphism A B ⟦_⟧ open IsSemiringHomomorphism isSemiringHomomorphism public - nearSemiringHomomorphism : NearSemiringHomomorphism A.nearSemiring B.nearSemiring + nearSemiringHomomorphism : NearSemiringHomomorphism A.rawNearSemiring B.rawNearSemiring nearSemiringHomomorphism = record { isNearSemiringHomomorphism = isNearSemiringHomomorphism } open NearSemiringHomomorphism nearSemiringHomomorphism public using (*-magmaHomomorphism; +-monoidHomomorphism; +-magmaHomomorphism) - *-monoidHomomorphism : MonoidHomomorphism A.*-monoid B.*-monoid + *-monoidHomomorphism : MonoidHomomorphism A.*-rawMonoid B.*-rawMonoid *-monoidHomomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism } ------------------------------------------------------------------------ -- Morphisms between KleeneAlgebras ------------------------------------------------------------------------ -record KleeneAlgebraHomomorphism (A : KleeneAlgebra a ℓa) (B : KleeneAlgebra b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where +record KleeneAlgebraHomomorphism + (A : RawKleeneAlgebra a ℓa) (B : RawKleeneAlgebra b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) + where private - module A = KleeneAlgebra A - module B = KleeneAlgebra B + module A = RawKleeneAlgebra A + module B = RawKleeneAlgebra B field ⟦_⟧ : A.Carrier → B.Carrier - isKleeneAlgebraHomomorphism : IsKleeneAlgebraHomomorphism A.rawKleeneAlgebra B.rawKleeneAlgebra ⟦_⟧ + isKleeneAlgebraHomomorphism : IsKleeneAlgebraHomomorphism A B ⟦_⟧ open IsKleeneAlgebraHomomorphism isKleeneAlgebraHomomorphism public - semiringHomomorphism : SemiringHomomorphism A.semiring B.semiring + semiringHomomorphism : SemiringHomomorphism A.rawSemiring B.rawSemiring semiringHomomorphism = record { isSemiringHomomorphism = isSemiringHomomorphism } open SemiringHomomorphism semiringHomomorphism public @@ -155,48 +166,48 @@ record KleeneAlgebraHomomorphism (A : KleeneAlgebra a ℓa) (B : KleeneAlgebra b -- Morphisms between RingWithoutOnes ------------------------------------------------------------------------ -record RingWithoutOneHomomorphism (A : RingWithoutOne a ℓa) (B : RingWithoutOne b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where +record RingWithoutOneHomomorphism (A : RawRingWithoutOne a ℓa) (B : RawRingWithoutOne b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where private - module A = RingWithoutOne A - module B = RingWithoutOne B + module A = RawRingWithoutOne A + module B = RawRingWithoutOne B field ⟦_⟧ : A.Carrier → B.Carrier - isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism A.rawRingWithoutOne B.rawRingWithoutOne ⟦_⟧ + isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism A B ⟦_⟧ open IsRingWithoutOneHomomorphism isRingWithoutOneHomomorphism public - nearSemiringHomomorphism : NearSemiringHomomorphism A.nearSemiring B.nearSemiring + nearSemiringHomomorphism : NearSemiringHomomorphism A.rawNearSemiring B.rawNearSemiring nearSemiringHomomorphism = record { isNearSemiringHomomorphism = isNearSemiringHomomorphism } open NearSemiringHomomorphism nearSemiringHomomorphism public using (*-magmaHomomorphism; +-magmaHomomorphism; +-monoidHomomorphism) - +-groupHomomorphism : GroupHomomorphism A.+-group B.+-group + +-groupHomomorphism : GroupHomomorphism A.+-rawGroup B.+-rawGroup +-groupHomomorphism = record { isGroupHomomorphism = +-isGroupHomomorphism } ------------------------------------------------------------------------ -- Morphisms between Rings ------------------------------------------------------------------------ -record RingHomomorphism (A : Ring a ℓa) (B : Ring b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where +record RingHomomorphism (A : RawRing a ℓa) (B : RawRing b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where private - module A = Ring A - module B = Ring B + module A = RawRing A + module B = RawRing B field ⟦_⟧ : A.Carrier → B.Carrier - isRingHomomorphism : IsRingHomomorphism A.rawRing B.rawRing ⟦_⟧ + isRingHomomorphism : IsRingHomomorphism A B ⟦_⟧ open IsRingHomomorphism isRingHomomorphism public - ringWithoutOneHomomorphism : RingWithoutOneHomomorphism A.ringWithoutOne B.ringWithoutOne + ringWithoutOneHomomorphism : RingWithoutOneHomomorphism A.rawRingWithoutOne B.rawRingWithoutOne ringWithoutOneHomomorphism = record { isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism } open RingWithoutOneHomomorphism ringWithoutOneHomomorphism public using (+-groupHomomorphism) - semiringHomomorphism : SemiringHomomorphism A.semiring B.semiring + semiringHomomorphism : SemiringHomomorphism A.rawSemiring B.rawSemiring semiringHomomorphism = record { isSemiringHomomorphism = isSemiringHomomorphism } open SemiringHomomorphism semiringHomomorphism public @@ -208,34 +219,39 @@ record RingHomomorphism (A : Ring a ℓa) (B : Ring b ℓb) : Set (a ⊔ b ⊔ -- Morphisms between Quasigroups ------------------------------------------------------------------------ -record QuasigroupHomomorphism (A : Quasigroup a ℓa) (B : Quasigroup b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where +record QuasigroupHomomorphism + (A : RawQuasigroup a ℓa) (B : RawQuasigroup b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) + where private - module A = Quasigroup A - module B = Quasigroup B + module A = RawQuasigroup A + module B = RawQuasigroup B field ⟦_⟧ : A.Carrier → B.Carrier - isQuasigroupHomomorphism : IsQuasigroupHomomorphism A.rawQuasigroup B.rawQuasigroup ⟦_⟧ + isQuasigroupHomomorphism : IsQuasigroupHomomorphism A B ⟦_⟧ open IsQuasigroupHomomorphism isQuasigroupHomomorphism public - magmaHomomorphism : MagmaHomomorphism A.magma B.magma + magmaHomomorphism : MagmaHomomorphism A.∙-rawMagma B.∙-rawMagma magmaHomomorphism = record { isMagmaHomomorphism = ∙-isMagmaHomomorphism } ------------------------------------------------------------------------ -- Morphisms between Loops ------------------------------------------------------------------------ -record LoopHomomorphism (A : Loop a ℓa) (B : Loop b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where +record LoopHomomorphism + (A : RawLoop a ℓa) (B : RawLoop b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) + where private - module A = Loop A - module B = Loop B + module A = RawLoop A + module B = RawLoop B field ⟦_⟧ : A.Carrier → B.Carrier - isLoopHomomorphism : IsLoopHomomorphism A.rawLoop B.rawLoop ⟦_⟧ + isLoopHomomorphism : IsLoopHomomorphism A B ⟦_⟧ open IsLoopHomomorphism isLoopHomomorphism public - quasigroupHomomorphism : QuasigroupHomomorphism A.quasigroup B.quasigroup + quasigroupHomomorphism : QuasigroupHomomorphism A.rawQuasigroup B.rawQuasigroup quasigroupHomomorphism = record { isQuasigroupHomomorphism = isQuasigroupHomomorphism } + From 38fb86172f940382aad411fdd68ae37b942a4249 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Jun 2024 12:16:32 +0100 Subject: [PATCH 21/27] knock-on: `Identity` takes a full `Bundle` --- src/Algebra/Morphism/Construct/Identity.agda | 142 +++++++++++-------- 1 file changed, 81 insertions(+), 61 deletions(-) diff --git a/src/Algebra/Morphism/Construct/Identity.agda b/src/Algebra/Morphism/Construct/Identity.agda index 38407820ca..3138417fc4 100644 --- a/src/Algebra/Morphism/Construct/Identity.agda +++ b/src/Algebra/Morphism/Construct/Identity.agda @@ -22,7 +22,6 @@ open import Algebra.Morphism.Structures ; module LoopMorphisms ; module KleeneAlgebraMorphisms ) -open import Data.Product.Base using (_,_) open import Function.Base using (id) import Function.Construct.Identity as Id open import Level using (Level) @@ -282,111 +281,132 @@ module _ (K : RawKleeneAlgebra c ℓ) (open RawKleeneAlgebra K) (refl : Reflexiv -- Magma -magmaHomomorphism : (M : Magma c ℓ) → MagmaHomomorphism M M -magmaHomomorphism M = record - { ⟦_⟧ = id - ; isMagmaHomomorphism = isMagmaHomomorphism rawMagma refl - } - where +module _ (M : Magma c ℓ) where + open Magma M using (rawMagma; refl) open MagmaMorphisms rawMagma rawMagma + magmaHomomorphism : MagmaHomomorphism rawMagma rawMagma + magmaHomomorphism = record + { ⟦_⟧ = id + ; isMagmaHomomorphism = isMagmaHomomorphism rawMagma refl + } + -- Monoid -monoidHomomorphism : (M : Monoid c ℓ) → MonoidHomomorphism M M -monoidHomomorphism M = record - { ⟦_⟧ = id - ; isMonoidHomomorphism = isMonoidHomomorphism rawMonoid refl - } - where +module _ (M : Monoid c ℓ) where + open Monoid M using (rawMonoid; refl) open MonoidMorphisms rawMonoid rawMonoid + monoidHomomorphism : MonoidHomomorphism rawMonoid rawMonoid + monoidHomomorphism = record + { ⟦_⟧ = id + ; isMonoidHomomorphism = isMonoidHomomorphism rawMonoid refl + } + -- Group -groupHomomorphism : (M : Group c ℓ) → GroupHomomorphism M M -groupHomomorphism M = record - { ⟦_⟧ = id - ; isGroupHomomorphism = isGroupHomomorphism rawGroup refl - } - where +module _ (M : Group c ℓ) where + open Group M using (rawGroup; refl) open GroupMorphisms rawGroup rawGroup + groupHomomorphism : GroupHomomorphism rawGroup rawGroup + groupHomomorphism = record + { ⟦_⟧ = id + ; isGroupHomomorphism = isGroupHomomorphism rawGroup refl + } + -- NearSemiring -nearSemiringHomomorphism : (M : NearSemiring c ℓ) → NearSemiringHomomorphism M M -nearSemiringHomomorphism M = record - { ⟦_⟧ = id - ; isNearSemiringHomomorphism = isNearSemiringHomomorphism rawNearSemiring refl - } - where +module _ (M : NearSemiring c ℓ) where + open NearSemiring M using (rawNearSemiring; refl) open NearSemiringMorphisms rawNearSemiring rawNearSemiring + nearSemiringHomomorphism : NearSemiringHomomorphism rawNearSemiring rawNearSemiring + nearSemiringHomomorphism = record + { ⟦_⟧ = id + ; isNearSemiringHomomorphism = isNearSemiringHomomorphism rawNearSemiring refl + } + -- Semiring -semiringHomomorphism : (M : Semiring c ℓ) → SemiringHomomorphism M M -semiringHomomorphism M = record - { ⟦_⟧ = id - ; isSemiringHomomorphism = isSemiringHomomorphism rawSemiring refl - } - where +module _ (M : Semiring c ℓ) where + open Semiring M using (rawSemiring; refl) open SemiringMorphisms rawSemiring rawSemiring + semiringHomomorphism : SemiringHomomorphism rawSemiring rawSemiring + semiringHomomorphism = record + { ⟦_⟧ = id + ; isSemiringHomomorphism = isSemiringHomomorphism rawSemiring refl + } + -- KleeneAlgebra -kleeneAlgebraHomomorphism : (M : KleeneAlgebra c ℓ) → KleeneAlgebraHomomorphism M M -kleeneAlgebraHomomorphism M = record - { ⟦_⟧ = id - ; isKleeneAlgebraHomomorphism = isKleeneAlgebraHomomorphism rawKleeneAlgebra refl - } - where +module _ (M : KleeneAlgebra c ℓ) where + open KleeneAlgebra M using (rawKleeneAlgebra; refl) open KleeneAlgebraMorphisms rawKleeneAlgebra rawKleeneAlgebra + kleeneAlgebraHomomorphism : KleeneAlgebraHomomorphism rawKleeneAlgebra rawKleeneAlgebra + kleeneAlgebraHomomorphism = record + { ⟦_⟧ = id + ; isKleeneAlgebraHomomorphism = isKleeneAlgebraHomomorphism rawKleeneAlgebra refl + } + -- RingWithoutOne -ringWithoutOneHomomorphism : (M : RingWithoutOne c ℓ) → RingWithoutOneHomomorphism M M -ringWithoutOneHomomorphism M = record - { ⟦_⟧ = id - ; isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism rawRingWithoutOne refl - } - where +module _ (M : RingWithoutOne c ℓ) where + open RingWithoutOne M using (rawRingWithoutOne; refl) open RingWithoutOneMorphisms rawRingWithoutOne rawRingWithoutOne + ringWithoutOneHomomorphism : RingWithoutOneHomomorphism rawRingWithoutOne rawRingWithoutOne + ringWithoutOneHomomorphism = record + { ⟦_⟧ = id + ; isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism rawRingWithoutOne refl + } + -- Ring -ringHomomorphism : (M : Ring c ℓ) → RingHomomorphism M M -ringHomomorphism M = record - { ⟦_⟧ = id - ; isRingHomomorphism = isRingHomomorphism rawRing refl - } - where +module _ (M : Ring c ℓ) where + open Ring M using (rawRing; refl) open RingMorphisms rawRing rawRing + ringHomomorphism : RingHomomorphism rawRing rawRing + ringHomomorphism = record + { ⟦_⟧ = id + ; isRingHomomorphism = isRingHomomorphism rawRing refl + } -- Quasigroup -quasigroupHomomorphism : (M : Quasigroup c ℓ) → QuasigroupHomomorphism M M -quasigroupHomomorphism M = record - { ⟦_⟧ = id - ; isQuasigroupHomomorphism = isQuasigroupHomomorphism rawQuasigroup refl - } - where +module _ (M : Quasigroup c ℓ) where + open Quasigroup M using (rawQuasigroup; refl) open QuasigroupMorphisms rawQuasigroup rawQuasigroup + quasigroupHomomorphism : QuasigroupHomomorphism rawQuasigroup rawQuasigroup + quasigroupHomomorphism = record + { ⟦_⟧ = id + ; isQuasigroupHomomorphism = isQuasigroupHomomorphism rawQuasigroup refl + } + -- Loop -loopHomomorphism : (M : Loop c ℓ) → LoopHomomorphism M M -loopHomomorphism M = record - { ⟦_⟧ = id - ; isLoopHomomorphism = isLoopHomomorphism rawLoop refl - } - where +module _ (M : Loop c ℓ) where + open Loop M using (rawLoop; refl) open LoopMorphisms rawLoop rawLoop + + loopHomomorphism : LoopHomomorphism rawLoop rawLoop + loopHomomorphism = record + { ⟦_⟧ = id + ; isLoopHomomorphism = isLoopHomomorphism rawLoop refl + } + + From 08624e5a024df95e78f45321ffe7d1dd25013681 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Jun 2024 12:35:57 +0100 Subject: [PATCH 22/27] tighten imports --- src/Algebra/Morphism/Construct/Identity.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Algebra/Morphism/Construct/Identity.agda b/src/Algebra/Morphism/Construct/Identity.agda index 3138417fc4..253fc96c60 100644 --- a/src/Algebra/Morphism/Construct/Identity.agda +++ b/src/Algebra/Morphism/Construct/Identity.agda @@ -32,6 +32,7 @@ private variable c ℓ : Level + ------------------------------------------------------------------------ -- Magmas From 52ab68a31d0f187e9e0770b6aec9bab60041a036 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Jun 2024 13:05:50 +0100 Subject: [PATCH 23/27] knock-on: `Composition` takes full `Bundle`s --- .../Morphism/Construct/Composition.agda | 245 +++++++++++------- 1 file changed, 155 insertions(+), 90 deletions(-) diff --git a/src/Algebra/Morphism/Construct/Composition.agda b/src/Algebra/Morphism/Construct/Composition.agda index fcb4ce530e..9a420f3000 100644 --- a/src/Algebra/Morphism/Construct/Composition.agda +++ b/src/Algebra/Morphism/Construct/Composition.agda @@ -21,6 +21,7 @@ private variable a b c ℓ₁ ℓ₂ ℓ₃ : Level + ------------------------------------------------------------------------ -- Magmas @@ -430,117 +431,181 @@ module _ {K₁ : RawKleeneAlgebra a ℓ₁} -- Magma -magmaHomomorphism : {M₁ : Magma a ℓ₁} {M₂ : Magma b ℓ₂} {M₃ : Magma c ℓ₃} → - (h : MagmaHomomorphism M₁ M₂) → - (k : MagmaHomomorphism M₂ M₃) → - MagmaHomomorphism M₁ M₃ -magmaHomomorphism {M₃ = M₃} h k = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isMagmaHomomorphism = isMagmaHomomorphism (Magma.trans M₃) H.isMagmaHomomorphism K.isMagmaHomomorphism } - where - module H = MagmaHomomorphism h - module K = MagmaHomomorphism k +module _ {M₁ : Magma a ℓ₁} {M₂ : Magma b ℓ₂} {M₃ : Magma c ℓ₃} where + + private + module M₁ = Magma M₁ + module M₂ = Magma M₂ + module M₃ = Magma M₃ + + magmaHomomorphism : (h : MagmaHomomorphism M₁.rawMagma M₂.rawMagma) → + (k : MagmaHomomorphism M₂.rawMagma M₃.rawMagma) → + MagmaHomomorphism M₁.rawMagma M₃.rawMagma + magmaHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isMagmaHomomorphism = isMagmaHomomorphism M₃.trans H.isMagmaHomomorphism K.isMagmaHomomorphism + } + where + module H = MagmaHomomorphism h + module K = MagmaHomomorphism k -- Monoid -monoidHomomorphism : {M₁ : Monoid a ℓ₁} {M₂ : Monoid b ℓ₂} {M₃ : Monoid c ℓ₃} → - (h : MonoidHomomorphism M₁ M₂) → - (k : MonoidHomomorphism M₂ M₃) → - MonoidHomomorphism M₁ M₃ -monoidHomomorphism {M₃ = M₃} h k = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isMonoidHomomorphism = isMonoidHomomorphism (Monoid.trans M₃) H.isMonoidHomomorphism K.isMonoidHomomorphism } - where - module H = MonoidHomomorphism h - module K = MonoidHomomorphism k +module _ {M₁ : Monoid a ℓ₁} {M₂ : Monoid b ℓ₂} {M₃ : Monoid c ℓ₃} where + + private + module M₁ = Monoid M₁ + module M₂ = Monoid M₂ + module M₃ = Monoid M₃ + + monoidHomomorphism : (h : MonoidHomomorphism M₁.rawMonoid M₂.rawMonoid) → + (k : MonoidHomomorphism M₂.rawMonoid M₃.rawMonoid) → + MonoidHomomorphism M₁.rawMonoid M₃.rawMonoid + monoidHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isMonoidHomomorphism = isMonoidHomomorphism M₃.trans H.isMonoidHomomorphism K.isMonoidHomomorphism + } + where + module H = MonoidHomomorphism h + module K = MonoidHomomorphism k -- Group -groupHomomorphism : {M₁ : Group a ℓ₁} {M₂ : Group b ℓ₂} {M₃ : Group c ℓ₃} → - (h : GroupHomomorphism M₁ M₂) → - (k : GroupHomomorphism M₂ M₃) → - GroupHomomorphism M₁ M₃ -groupHomomorphism {M₃ = M₃} h k = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isGroupHomomorphism = isGroupHomomorphism (Group.trans M₃) H.isGroupHomomorphism K.isGroupHomomorphism } - where - module H = GroupHomomorphism h - module K = GroupHomomorphism k +module _ {M₁ : Group a ℓ₁} {M₂ : Group b ℓ₂} {M₃ : Group c ℓ₃} where + + private + module M₁ = Group M₁ + module M₂ = Group M₂ + module M₃ = Group M₃ + + groupHomomorphism : (h : GroupHomomorphism M₁.rawGroup M₂.rawGroup) → + (k : GroupHomomorphism M₂.rawGroup M₃.rawGroup) → + GroupHomomorphism M₁.rawGroup M₃.rawGroup + groupHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isGroupHomomorphism = isGroupHomomorphism M₃.trans H.isGroupHomomorphism K.isGroupHomomorphism + } + where + module H = GroupHomomorphism h + module K = GroupHomomorphism k -- NearSemiring -nearSemiringHomomorphism : {M₁ : NearSemiring a ℓ₁} {M₂ : NearSemiring b ℓ₂} {M₃ : NearSemiring c ℓ₃} → - (h : NearSemiringHomomorphism M₁ M₂) → - (k : NearSemiringHomomorphism M₂ M₃) → - NearSemiringHomomorphism M₁ M₃ -nearSemiringHomomorphism {M₃ = M₃} h k = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isNearSemiringHomomorphism = isNearSemiringHomomorphism (NearSemiring.trans M₃) H.isNearSemiringHomomorphism K.isNearSemiringHomomorphism } - where - module H = NearSemiringHomomorphism h - module K = NearSemiringHomomorphism k +module _ {M₁ : NearSemiring a ℓ₁} {M₂ : NearSemiring b ℓ₂} {M₃ : NearSemiring c ℓ₃} where + + private + module M₁ = NearSemiring M₁ + module M₂ = NearSemiring M₂ + module M₃ = NearSemiring M₃ + + nearSemiringHomomorphism : (h : NearSemiringHomomorphism M₁.rawNearSemiring M₂.rawNearSemiring) → + (k : NearSemiringHomomorphism M₂.rawNearSemiring M₃.rawNearSemiring) → + NearSemiringHomomorphism M₁.rawNearSemiring M₃.rawNearSemiring + nearSemiringHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isNearSemiringHomomorphism = isNearSemiringHomomorphism M₃.trans H.isNearSemiringHomomorphism K.isNearSemiringHomomorphism + } + where + module H = NearSemiringHomomorphism h + module K = NearSemiringHomomorphism k -- Semiring -semiringHomomorphism : {M₁ : Semiring a ℓ₁} {M₂ : Semiring b ℓ₂} {M₃ : Semiring c ℓ₃} → - (h : SemiringHomomorphism M₁ M₂) → - (k : SemiringHomomorphism M₂ M₃) → - SemiringHomomorphism M₁ M₃ -semiringHomomorphism {M₃ = M₃} h k = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isSemiringHomomorphism = isSemiringHomomorphism (Semiring.trans M₃) H.isSemiringHomomorphism K.isSemiringHomomorphism } - where - module H = SemiringHomomorphism h - module K = SemiringHomomorphism k +module _ {M₁ : Semiring a ℓ₁} {M₂ : Semiring b ℓ₂} {M₃ : Semiring c ℓ₃} where + + private + module M₁ = Semiring M₁ + module M₂ = Semiring M₂ + module M₃ = Semiring M₃ + + semiringHomomorphism : (h : SemiringHomomorphism M₁.rawSemiring M₂.rawSemiring) → + (k : SemiringHomomorphism M₂.rawSemiring M₃.rawSemiring) → + SemiringHomomorphism M₁.rawSemiring M₃.rawSemiring + semiringHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isSemiringHomomorphism = isSemiringHomomorphism M₃.trans H.isSemiringHomomorphism K.isSemiringHomomorphism + } + where + module H = SemiringHomomorphism h + module K = SemiringHomomorphism k -- RingWithoutOne -ringWithoutOneHomomorphism : {M₁ : RingWithoutOne a ℓ₁} {M₂ : RingWithoutOne b ℓ₂} {M₃ : RingWithoutOne c ℓ₃} → - (h : RingWithoutOneHomomorphism M₁ M₂) → - (k : RingWithoutOneHomomorphism M₂ M₃) → - RingWithoutOneHomomorphism M₁ M₃ -ringWithoutOneHomomorphism {M₃ = M₃} h k = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism (RingWithoutOne.trans M₃) H.isRingWithoutOneHomomorphism K.isRingWithoutOneHomomorphism } - where - module H = RingWithoutOneHomomorphism h - module K = RingWithoutOneHomomorphism k +module _ {M₁ : RingWithoutOne a ℓ₁} {M₂ : RingWithoutOne b ℓ₂} {M₃ : RingWithoutOne c ℓ₃} where + + private + module M₁ = RingWithoutOne M₁ + module M₂ = RingWithoutOne M₂ + module M₃ = RingWithoutOne M₃ + + ringWithoutOneHomomorphism : (h : RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₂.rawRingWithoutOne) → + (k : RingWithoutOneHomomorphism M₂.rawRingWithoutOne M₃.rawRingWithoutOne) → + RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₃.rawRingWithoutOne + ringWithoutOneHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism M₃.trans H.isRingWithoutOneHomomorphism K.isRingWithoutOneHomomorphism + } + where + module H = RingWithoutOneHomomorphism h + module K = RingWithoutOneHomomorphism k -- Ring -ringHomomorphism : {M₁ : Ring a ℓ₁} {M₂ : Ring b ℓ₂} {M₃ : Ring c ℓ₃} → - (h : RingHomomorphism M₁ M₂) → - (k : RingHomomorphism M₂ M₃) → - RingHomomorphism M₁ M₃ -ringHomomorphism {M₃ = M₃} h k = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isRingHomomorphism = isRingHomomorphism (Ring.trans M₃) H.isRingHomomorphism K.isRingHomomorphism } - where - module H = RingHomomorphism h - module K = RingHomomorphism k +module _ {M₁ : Ring a ℓ₁} {M₂ : Ring b ℓ₂} {M₃ : Ring c ℓ₃} where + + private + module M₁ = Ring M₁ + module M₂ = Ring M₂ + module M₃ = Ring M₃ + + ringHomomorphism : (h : RingHomomorphism M₁.rawRing M₂.rawRing) → + (k : RingHomomorphism M₂.rawRing M₃.rawRing) → + RingHomomorphism M₁.rawRing M₃.rawRing + ringHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isRingHomomorphism = isRingHomomorphism M₃.trans H.isRingHomomorphism K.isRingHomomorphism + } + where + module H = RingHomomorphism h + module K = RingHomomorphism k -- Quasigroup -quasigroupHomomorphism : {M₁ : Quasigroup a ℓ₁} {M₂ : Quasigroup b ℓ₂} {M₃ : Quasigroup c ℓ₃} → - (h : QuasigroupHomomorphism M₁ M₂) → - (k : QuasigroupHomomorphism M₂ M₃) → - QuasigroupHomomorphism M₁ M₃ -quasigroupHomomorphism {M₃ = M₃} h k = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isQuasigroupHomomorphism = isQuasigroupHomomorphism (Quasigroup.trans M₃) H.isQuasigroupHomomorphism K.isQuasigroupHomomorphism } - where - module H = QuasigroupHomomorphism h - module K = QuasigroupHomomorphism k +module _ {M₁ : Quasigroup a ℓ₁} {M₂ : Quasigroup b ℓ₂} {M₃ : Quasigroup c ℓ₃} where + + private + module M₁ = Quasigroup M₁ + module M₂ = Quasigroup M₂ + module M₃ = Quasigroup M₃ + + quasigroupHomomorphism : (h : QuasigroupHomomorphism M₁.rawQuasigroup M₂.rawQuasigroup) → + (k : QuasigroupHomomorphism M₂.rawQuasigroup M₃.rawQuasigroup) → + QuasigroupHomomorphism M₁.rawQuasigroup M₃.rawQuasigroup + quasigroupHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isQuasigroupHomomorphism = isQuasigroupHomomorphism M₃.trans H.isQuasigroupHomomorphism K.isQuasigroupHomomorphism + } + where + module H = QuasigroupHomomorphism h + module K = QuasigroupHomomorphism k -- Loop -loopHomomorphism : {M₁ : Loop a ℓ₁} {M₂ : Loop b ℓ₂} {M₃ : Loop c ℓ₃} → - (h : LoopHomomorphism M₁ M₂) → - (k : LoopHomomorphism M₂ M₃) → - LoopHomomorphism M₁ M₃ -loopHomomorphism {M₃ = M₃} h k = record - { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ - ; isLoopHomomorphism = isLoopHomomorphism (Loop.trans M₃) H.isLoopHomomorphism K.isLoopHomomorphism } - where - module H = LoopHomomorphism h - module K = LoopHomomorphism k +module _ {M₁ : Loop a ℓ₁} {M₂ : Loop b ℓ₂} {M₃ : Loop c ℓ₃} where + + private + module M₁ = Loop M₁ + module M₂ = Loop M₂ + module M₃ = Loop M₃ + + loopHomomorphism : (h : LoopHomomorphism M₁.rawLoop M₂.rawLoop) → + (k : LoopHomomorphism M₂.rawLoop M₃.rawLoop) → + LoopHomomorphism M₁.rawLoop M₃.rawLoop + loopHomomorphism h k = record + { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧ + ; isLoopHomomorphism = isLoopHomomorphism M₃.trans H.isLoopHomomorphism K.isLoopHomomorphism + } + where + module H = LoopHomomorphism h + module K = LoopHomomorphism k + From 3409e84208b4d2125336fec4292692f274fffcd5 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Jun 2024 13:06:36 +0100 Subject: [PATCH 24/27] `CHANGELOG` --- CHANGELOG.md | 163 ++++++++++++++++++++++++++------------------------- 1 file changed, 83 insertions(+), 80 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2b4e94c935..0fc0e42754 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -113,30 +113,9 @@ New modules Algebra.Module.Bundles.Raw ``` -* Bundled morphisms between algebraic structures: +* Bundled morphisms between (raw) algebraic structures: ``` Algebra.Morphism.Bundles - ``` - -* Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid): - ``` - Data.List.Relation.Binary.Equality.Setoid.Properties - ``` - -* Refactoring of `Data.List.Base.{scanr|scanl}` and their properties: - ``` - Data.List.Scans.Base - Data.List.Scans.Properties - ``` - -* Prime factorisation of natural numbers. - ``` - Data.Nat.Primality.Factorisation - ``` - -* Consequences of 'infinite descent' for (accessible elements of) well-founded relations: - ```agda - Induction.InfiniteDescent ``` * The unique morphism from the initial, resp. terminal, algebra: @@ -150,12 +129,35 @@ New modules Algebra.Module.Construct.Idealization ``` +* Pointwise and equality relations over indexed containers: + ```agda + Data.Container.Indexed.Relation.Binary.Pointwise + Data.Container.Indexed.Relation.Binary.Pointwise.Properties + Data.Container.Indexed.Relation.Binary.Equality.Setoid + ``` + +* Refactoring of `Data.List.Base.{scanr|scanl}` and their properties: + ``` + Data.List.Scans.Base + Data.List.Scans.Properties + ``` + +* Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid): + ``` + Data.List.Relation.Binary.Equality.Setoid.Properties + ``` + * `Data.List.Relation.Binary.Sublist.Propositional.Slice` replacing `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` (*) and adding new functions: - `⊆-upper-bound-is-cospan` generalising `⊆-disjoint-union-is-cospan` from (*) - `⊆-upper-bound-cospan` generalising `⊆-disjoint-union-cospan` from (*) +* Prime factorisation of natural numbers. + ``` + Data.Nat.Primality.Factorisation + ``` + * `Data.Vec.Functional.Relation.Binary.Permutation`, defining: ```agda _↭_ : IRel (Vector A) _ @@ -180,27 +182,25 @@ New modules _⇨_ = setoid ``` -* Symmetric interior of a binary relation - ``` - Relation.Binary.Construct.Interior.Symmetric +* Consequences of 'infinite descent' for (accessible elements of) well-founded relations: + ```agda + Induction.InfiniteDescent ``` -* Properties of `Setoid`s with decidable equality relation: - ``` - Relation.Binary.Properties.DecSetoid +* New IO primitives to handle buffering + ```agda + IO.Primitive.Handle + IO.Handle ``` -* Pointwise and equality relations over indexed containers: +* Symmetric interior of a binary relation ```agda - Data.Container.Indexed.Relation.Binary.Pointwise - Data.Container.Indexed.Relation.Binary.Pointwise.Properties - Data.Container.Indexed.Relation.Binary.Equality.Setoid + Relation.Binary.Construct.Interior.Symmetric ``` -* New IO primitives to handle buffering +* Properties of `Setoid`s with decidable equality relation: ```agda - IO.Primitive.Handle - IO.Handle + Relation.Binary.Properties.DecSetoid ``` * `System.Random` bindings: @@ -299,52 +299,55 @@ Additions to existing modules ``` * In `Algebra.Morphism.Construct.Composition`: - ``` - magmaHomomorphism : MagmaHomomorphism M₁ M₂ → - MagmaHomomorphism M₂ M₃ → - MagmaHomomorphism M₁ M₃ - monoidHomomorphism : MonoidHomomorphism M₁ M₂ → - MagmaHomomorphism M₂ M₃ → - MagmaHomomorphism M₁ M₃ - groupHomomorphism : GroupHomomorphism M₁ M₂ → - MagmaHomomorphism M₂ M₃ → - MagmaHomomorphism M₁ M₃ - nearSemiringHomomorphism : NearSemiringHomomorphism M₁ M₂ → - NearSemiringHomomorphism M₂ M₃ → - NearSemiringHomomorphism M₁ M₃ - semiringHomomorphism : SemiringHomomorphism M₁ M₂ → - SemiringHomomorphism M₂ M₃ → - SemiringHomomorphism M₁ M₃ - kleeneAlgebraHomomorphism : KleeneAlgebraHomomorphism M₁ M₂ → - KleeneAlgebraHomomorphism M₂ M₃ → - KleeneAlgebraHomomorphism M₁ M₃ - ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M₁ M₂ → - RingWithoutOneHomomorphism M₂ M₃ → - RingWithoutOneHomomorphism M₁ M₃ - ringHomomorphism : RingHomomorphism M₁ M₂ → - RingHomomorphism M₂ M₃ → - RingHomomorphism M₁ M₃ - quasigroupHomomorphism : QuasigroupHomomorphism M₁ M₂ → - QuasigroupHomomorphism M₂ M₃ → - QuasigroupHomomorphism M₁ M₃ - loopHomomorphism : LoopHomomorphism M₁ M₂ → - LoopHomomorphism M₂ M₃ → - LoopHomomorphism M₁ M₃ + ```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`: - ``` - magmaHomomorphism : MagmaHomomorphism M M - monoidHomomorphism : MonoidHomomorphism M M - groupHomomorphism : GroupHomomorphism M M - nearSemiringHomomorphism : NearSemiringHomomorphism M M - semiringHomomorphism : SemiringHomomorphism M M - kleeneAlgebraHomomorphism : KleeneAlgebraHomomorphism M M - nearSemiringHomomorphism : NearSemiringHomomorphism M M - ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M M - ringHomomorphism : RingHomomorphism M M - quasigroupHomomorphism : QuasigroupHomomorphism M M - loopHomomorphism : LoopHomomorphism M M + ```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` @@ -366,7 +369,7 @@ Additions to existing modules ``` * In `Algebra.Properties.AbelianGroup`: - ``` + ```agda ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x ``` @@ -713,7 +716,7 @@ Additions to existing modules * Added new definitions in `Relation.Binary.Definitions` ``` Stable _∼_ = ∀ x y → Nullary.Stable (x ∼ y) - Empty _∼_ = ∀ {x y} → x ∼ y → ⊥ + Empty _∼_ = ∀ {x y} → ¬ (x ∼ y) ``` * Added new proofs in `Relation.Binary.Properties.Setoid`: From dfb67c9c01379d4b1fa1ffbbb70c4f027a5181e2 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Jun 2024 13:18:55 +0100 Subject: [PATCH 25/27] `fix-whitespace` --- src/Algebra/Morphism/Bundles.agda | 2 +- src/Algebra/Morphism/Construct/Identity.agda | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda index 8bfe695825..62f7287d0d 100644 --- a/src/Algebra/Morphism/Bundles.agda +++ b/src/Algebra/Morphism/Bundles.agda @@ -3,7 +3,7 @@ -- -- Bundled definitions of homomorphisms between algebras -- --- NB indexed by Raw bundles, just as IsXHomomorphism is +-- NB indexed by Raw bundles, just as IsXHomomorphism is ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} diff --git a/src/Algebra/Morphism/Construct/Identity.agda b/src/Algebra/Morphism/Construct/Identity.agda index 253fc96c60..d6032ecbe7 100644 --- a/src/Algebra/Morphism/Construct/Identity.agda +++ b/src/Algebra/Morphism/Construct/Identity.agda @@ -344,7 +344,7 @@ module _ (M : Semiring c ℓ) where { ⟦_⟧ = id ; isSemiringHomomorphism = isSemiringHomomorphism rawSemiring refl } - + -- KleeneAlgebra module _ (M : KleeneAlgebra c ℓ) where @@ -409,5 +409,4 @@ module _ (M : Loop c ℓ) where { ⟦_⟧ = id ; isLoopHomomorphism = isLoopHomomorphism rawLoop refl } - From bd661032da74b033e7a411c16c6631b5e15f2a73 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 28 Jul 2024 10:18:24 +0100 Subject: [PATCH 26/27] fix `CHANGELOG` --- CHANGELOG.md | 927 +-------------------------------------------------- 1 file changed, 2 insertions(+), 925 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 551a0c9751..80da9ee48e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,7 +1,7 @@ -Version 2.1-dev +Version 2.2-dev =============== -The library has been tested using Agda 2.6.4, 2.6.4.1, and 2.6.4.3. +The library has been tested using Agda 2.6.4.3. Highlights ---------- @@ -9,943 +9,20 @@ Highlights Bug-fixes --------- -* Fix statement of `Data.Vec.Properties.toList-replicate`, where `replicate` - was mistakenly applied to the level of the type `A` instead of the - variable `x` of type `A`. - -* Module `Data.List.Relation.Ternary.Appending.Setoid.Properties` no longer - exports the `Setoid` module under the alias `S`. - -* Remove unbound parameter from `Data.List.Properties.length-alignWith`, - `alignWith-map` and `map-alignWith`. - Non-backwards compatible changes -------------------------------- -* The modules and morphisms in `Algebra.Module.Morphism.Structures` are now - parametrized by _raw_ bundles rather than lawful bundles, in line with other - modules defining morphism structures. -* The definitions in `Algebra.Module.Morphism.Construct.Composition` are now - parametrized by _raw_ bundles, and as such take a proof of transitivity. -* The definitions in `Algebra.Module.Morphism.Construct.Identity` are now - parametrized by _raw_ bundles, and as such take a proof of reflexivity. -* The module `IO.Primitive` was moved to `IO.Primitive.Core`. -* The modules in the `Data.Word` hierarchy were moved to the `Data.Word64` - one instead. - -Other major improvements ------------------------- - Minor improvements ------------------ -* The size of the dependency graph for many modules has been - reduced. This may lead to speed ups for first-time loading of some - modules. - -* The definition of the `Pointwise` relational combinator in - `Data.Product.Relation.Binary.Pointwise.NonDependent.Pointwise` - has been generalised to take heterogeneous arguments in `REL`. - -* The structures `IsSemilattice` and `IsBoundedSemilattice` in - `Algebra.Lattice.Structures` have been redefined as aliases of - `IsCommutativeBand` and `IsIdempotentMonoid` in `Algebra.Structures`. - - Deprecated modules ------------------ -* `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` deprecated in favour of - `Data.List.Relation.Binary.Sublist.Propositional.Slice`. - -* The modules `Function.Endomorphism.Propositional` and - `Function.Endomorphism.Setoid` that use the old `Function` - hierarchy. Use `Function.Endo.Propositional` and - `Function.Endo.Setoid` instead. - Deprecated names ---------------- -* In `Algebra.Properties.Semiring.Mult`: - ```agda - 1×-identityʳ ↦ ×-homo-1 - ``` - -* In `Algebra.Structures.IsGroup`: - ```agda - _-_ ↦ _//_ - ``` - -* In `Algebra.Structures.Biased`: - ```agda - IsRing* ↦ Algebra.Structures.IsRing - isRing* ↦ Algebra.Structures.isRing - ``` - -* In `Data.List.Base`: - ```agda - scanr ↦ Data.List.Scans.Base.scanr - scanl ↦ Data.List.Scans.Base.scanl - ``` - -* In `Data.List.Properties`: - ```agda - scanr-defn ↦ Data.List.Scans.Properties.scanr-defn - scanl-defn ↦ Data.List.Scans.Properties.scanl-defn - ``` - -* In `Data.List.Relation.Unary.All.Properties`: - ```agda - map-compose ↦ map-∘ - ``` - -* In `Data.Nat.Divisibility.Core`: - ```agda - *-pres-∣ ↦ Data.Nat.Divisibility.*-pres-∣ - ``` - -* In `IO.Base`: - ```agda - untilRight ↦ untilInj₂ - ``` - -* In `Data.Float.Base`: - ```agda - toWord ↦ toWord64 - ``` - -* In `Data.Float.Properties`: - ```agda - toWord-injective ↦ toWord64-injective - ``` - New modules ----------- -* Pointwise lifting of algebraic structures `IsX` and bundles `X` from - carrier set `C` to function space `A → C`: - ``` - Algebra.Construct.Pointwise - ``` - -* Raw bundles for module-like algebraic structures: - ``` - Algebra.Module.Bundles.Raw - ``` - -* Nagata's construction of the "idealization of a module": - ```agda - Algebra.Module.Construct.Idealization - ``` - -* Bundled morphisms between (raw) algebraic structures: - ``` - Algebra.Morphism.Bundles - ``` - -* The unique morphism from the initial, resp. terminal, algebra: - ```agda - Algebra.Morphism.Construct.Initial - Algebra.Morphism.Construct.Terminal - ``` - -* Pointwise and equality relations over indexed containers: - ```agda - Data.Container.Indexed.Relation.Binary.Pointwise - Data.Container.Indexed.Relation.Binary.Pointwise.Properties - Data.Container.Indexed.Relation.Binary.Equality.Setoid - ``` - -* Refactoring of `Data.List.Base.{scanr|scanl}` and their properties: - ``` - Data.List.Scans.Base - Data.List.Scans.Properties - ``` - -* Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid): - ``` - Data.List.Relation.Binary.Equality.Setoid.Properties - ``` - -* Pointwise and equality relations over indexed containers: - ```agda - Data.Container.Indexed.Relation.Binary.Pointwise - Data.Container.Indexed.Relation.Binary.Pointwise.Properties - Data.Container.Indexed.Relation.Binary.Equality.Setoid - ``` - -* Refactoring of `Data.List.Base.{scanr|scanl}` and their properties: - ``` - Data.List.Scans.Base - Data.List.Scans.Properties - ``` - -* Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid): - ``` - Data.List.Relation.Binary.Equality.Setoid.Properties - ``` - -* `Data.List.Relation.Binary.Sublist.Propositional.Slice` - replacing `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` (*) - and adding new functions: - - `⊆-upper-bound-is-cospan` generalising `⊆-disjoint-union-is-cospan` from (*) - - `⊆-upper-bound-cospan` generalising `⊆-disjoint-union-cospan` from (*) - ``` - -* Decidability for the subset relation on lists: - ```agda - Data.List.Relation.Binary.Subset.DecSetoid (_⊆?_) - Data.List.Relation.Binary.Subset.DecPropositional - ``` - -* Decidability for the disjoint relation on lists: - ```agda - Data.List.Relation.Binary.Disjoint.DecSetoid (disjoint?) - Data.List.Relation.Binary.Disjoint.DecPropositional - ``` - -* Prime factorisation of natural numbers. - ``` - Data.Nat.Primality.Factorisation - ``` - -* Prime factorisation of natural numbers. - ``` - Data.Nat.Primality.Factorisation - ``` - -* `Data.Vec.Functional.Relation.Binary.Permutation`, defining: - ```agda - _↭_ : IRel (Vector A) _ - ``` - -* `Data.Vec.Functional.Relation.Binary.Permutation.Properties` of the above: - ```agda - ↭-refl : Reflexive (Vector A) _↭_ - ↭-reflexive : xs ≡ ys → xs ↭ ys - ↭-sym : Symmetric (Vector A) _↭_ - ↭-trans : Transitive (Vector A) _↭_ - isIndexedEquivalence : {A : Set a} → IsIndexedEquivalence (Vector A) _↭_ - 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 _ _ - ``` - and a convenient infix version - ```agda - _⇨_ = setoid - ``` - -* Consequences of 'infinite descent' for (accessible elements of) well-founded relations: - ```agda - Induction.InfiniteDescent - ``` - -* New IO primitives to handle buffering - ```agda - IO.Primitive.Handle - IO.Handle - ``` - -* Symmetric interior of a binary relation - ``` - Relation.Binary.Construct.Interior.Symmetric - ``` - -* Properties of `Setoid`s with decidable equality relation: - ```agda - Relation.Binary.Properties.DecSetoid - ``` - -* Systematise the use of `Recomputable A = .A → A`: - ```agda - Relation.Nullary.Recomputable - ``` - with `Recomputable` exported publicly from `Relation.Nullary`. - -* `System.Random` bindings: - ```agda - System.Random.Primitive - System.Random - ``` - -* Show modules: - ```agda - Data.List.Show - Data.Vec.Show - Data.Vec.Bounded.Show - ``` - -* Word64 literals and bit-based functions: - ```agda - Data.Word64.Literals - Data.Word64.Unsafe - Data.Word64.Show - ``` - -* A type of bytes: - ```agda - Data.Word8.Primitive - Data.Word8.Base - Data.Word8.Literals - Data.Word8.Show - ``` - -* Bytestrings and builders: - ```agda - Data.Bytestring.Base - Data.Bytestring.Builder.Base - Data.Bytestring.Builder.Primitive - Data.Bytestring.IO - Data.Bytestring.IO.Primitive - Data.Bytestring.Primitive - ``` - -* Decidability for the subset relation on lists: - ```agda - Data.List.Relation.Binary.Subset.DecSetoid (_⊆?_) - Data.List.Relation.Binary.Subset.DecPropositional - ``` - -* Decidability for the disjoint relation on lists: - ```agda - Data.List.Relation.Binary.Disjoint.DecSetoid (disjoint?) - Data.List.Relation.Binary.Disjoint.DecPropositional - ``` - Additions to existing modules ----------------------------- - -* In `Algebra.Bundles` - ```agda - record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) - record CommutativeBand c ℓ : Set (suc (c ⊔ ℓ)) - record IdempotentMonoid c ℓ : Set (suc (c ⊔ ℓ)) - ``` - and additional manifest fields for sub-bundles arising from these in: - ```agda - IdempotentCommutativeMonoid - IdempotentSemiring - ``` - - -* In `Algebra.Bundles.KleeneAlgebra`: - ```agda - rawKleeneAlgebra : RawKleeneAlgebra _ _ - ``` - -* In `Algebra.Bundles.Raw` - ```agda - record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) - ``` - -* 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.Construct.Terminal`: - ```agda - rawNearSemiring : RawNearSemiring c ℓ - nearSemiring : NearSemiring c ℓ - ``` - -* In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts. - -* In `Algebra.Module.Construct.DirectProduct`: - ```agda - rawLeftSemimodule : RawLeftSemimodule R m ℓm → RawLeftSemimodule m′ ℓm′ → RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawLeftModule : RawLeftModule R m ℓm → RawLeftModule m′ ℓm′ → RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawRightSemimodule : RawRightSemimodule R m ℓm → RawRightSemimodule m′ ℓm′ → RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawRightModule : RawRightModule R m ℓm → RawRightModule m′ ℓm′ → RawRightModule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawBisemimodule : RawBisemimodule R m ℓm → RawBisemimodule m′ ℓm′ → RawBisemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawBimodule : RawBimodule R m ℓm → RawBimodule m′ ℓm′ → RawBimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawSemimodule : RawSemimodule R m ℓm → RawSemimodule m′ ℓm′ → RawSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawModule : RawModule R m ℓm → RawModule m′ ℓm′ → RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′) - ``` - -* In `Algebra.Module.Construct.TensorUnit`: - ```agda - rawLeftSemimodule : RawLeftSemimodule _ c ℓ - rawLeftModule : RawLeftModule _ c ℓ - rawRightSemimodule : RawRightSemimodule _ c ℓ - rawRightModule : RawRightModule _ c ℓ - rawBisemimodule : RawBisemimodule _ _ c ℓ - rawBimodule : RawBimodule _ _ c ℓ - rawSemimodule : RawSemimodule _ c ℓ - rawModule : RawModule _ c ℓ - ``` - -* In `Algebra.Module.Construct.Zero`: - ```agda - rawLeftSemimodule : RawLeftSemimodule R c ℓ - rawLeftModule : RawLeftModule R c ℓ - rawRightSemimodule : RawRightSemimodule R c ℓ - rawRightModule : RawRightModule R c ℓ - rawBisemimodule : RawBisemimodule R c ℓ - rawBimodule : RawBimodule R c ℓ - rawSemimodule : RawSemimodule R c ℓ - rawModule : RawModule R c ℓ - ``` - -* 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`: - ```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 _ - ``` - -* In `Algebra.Morphism.Structures.RingMorphisms` - ```agda - isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧ - ``` - -* In `Algebra.Morphism.Structures.RingWithoutOneMorphisms` - ```agda - isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧ - ``` - -* In `Algebra.Properties.AbelianGroup`: - ```agda - ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x - ``` - -* In `Algebra.Properties.Group`: - ```agda - isQuasigroup : IsQuasigroup _∙_ _\\_ _//_ - quasigroup : Quasigroup _ _ - isLoop : IsLoop _∙_ _\\_ _//_ ε - loop : Loop _ _ - - \\-leftDividesˡ : LeftDividesˡ _∙_ _\\_ - \\-leftDividesʳ : LeftDividesʳ _∙_ _\\_ - \\-leftDivides : LeftDivides _∙_ _\\_ - //-rightDividesˡ : RightDividesˡ _∙_ _//_ - //-rightDividesʳ : RightDividesʳ _∙_ _//_ - //-rightDivides : RightDivides _∙_ _//_ - - ⁻¹-selfInverse : SelfInverse _⁻¹ - x∙y⁻¹≈ε⇒x≈y : ∀ x y → (x ∙ y ⁻¹) ≈ ε → x ≈ y - x≈y⇒x∙y⁻¹≈ε : ∀ {x y} → x ≈ y → (x ∙ y ⁻¹) ≈ ε - \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ - comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x - ⁻¹-anti-homo-// : (x // y) ⁻¹ ≈ y // x - ⁻¹-anti-homo-\\ : (x \\ y) ⁻¹ ≈ y \\ x - ``` - -* In `Algebra.Properties.Loop`: - ```agda - identityˡ-unique : x ∙ y ≈ y → x ≈ ε - identityʳ-unique : x ∙ y ≈ x → y ≈ ε - identity-unique : Identity x _∙_ → x ≈ ε - ``` - -* In `Algebra.Properties.Monoid.Mult`: - ```agda - ×-homo-0 : ∀ x → 0 × x ≈ 0# - ×-homo-1 : ∀ x → 1 × x ≈ x - ``` - -* In `Algebra.Properties.Semiring.Mult`: - ```agda - ×-homo-0# : ∀ x → 0 × x ≈ 0# * x - ×-homo-1# : ∀ x → 1 × x ≈ 1# * x - idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x - ``` - -* In `Algebra.Structures` - ```agda - record IsSuccessorSet (suc# : Op₁ A) (zero# : A) : Set _ - record IsCommutativeBand (∙ : Op₂ A) : Set _ - record IsIdempotentMonoid (∙ : Op₂ A) (ε : A) : Set _ - ``` - and additional manifest fields for substructures arising from these in: - ```agda - IsIdempotentCommutativeMonoid - IsIdempotentSemiring - ``` - -* In `Algebra.Structures.IsGroup`: - ```agda - infixl 6 _//_ - _//_ : Op₂ A - x // y = x ∙ (y ⁻¹) - infixr 6 _\\_ - _\\_ : Op₂ A - x \\ y = (x ⁻¹) ∙ y - ``` - -* In `Algebra.Structures.RingWithoutOne`: - ```agda - isNearSemiring : IsNearSemiring _ _ - ``` - -* In `Algebra.Structures.IsCancellativeCommutativeSemiring` add the - extra property as an exposed definition: - ```agda - *-cancelʳ-nonZero : AlmostRightCancellative 0# * - ``` - -* In `Data.Bool.Show`: - ```agda - showBit : Bool → Char - ``` - -* In `Data.Container.Indexed.Core`: - ```agda - Subtrees o c = (r : Response c) → X (next c r) - ``` - -* In `Data.Empty`: - ```agda - ⊥-elim-irr : .⊥ → Whatever - ``` - -* In `Data.Fin.Properties`: - ```agda - nonZeroIndex : Fin n → ℕ.NonZero n - ``` - -* In `Data.Float.Base`: - ```agda - _≤_ : Rel Float _ - ``` - -* In `Data.Integer.Divisibility`: introduce `divides` as an explicit pattern synonym - ```agda - pattern divides k eq = Data.Nat.Divisibility.divides k eq - ``` - -* In `Data.Integer.Properties`: - ```agda - ◃-nonZero : .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n) - sign-* : .{{NonZero (i * j)}} → sign (i * j) ≡ sign i Sign.* sign j - i*j≢0 : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j) - ``` - -* In `Data.List.Base` redefine `inits` and `tails` in terms of: - ```agda - tail∘inits : List A → List (List A) - tail∘tails : List A → List (List A) - ``` - -* In `Data.List.Membership.Propositional.Properties.Core`: - ```agda - find∘∃∈-Any : (p : ∃ λ x → x ∈ xs × P x) → find (∃∈-Any p) ≡ p - ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p - ``` - -* In `Data.List.Membership.Setoid.Properties`: - ```agda - reverse⁺ : x ∈ xs → x ∈ reverse xs - reverse⁻ : x ∈ reverse xs → x ∈ xs - ``` - -* In `Data.List.NonEmpty.Base`: - ```agda - inits : List A → List⁺ (List A) - tails : List A → List⁺ (List A) - ``` - -* In `Data.List.NonEmpty.Properties`: - ```agda - toList-inits : toList ∘ List⁺.inits ≗ List.inits - toList-tails : toList ∘ List⁺.tails ≗ List.tails - ``` - -* In `Data.List.Properties`: - ```agda - length-catMaybes : length (catMaybes xs) ≤ length xs - applyUpTo-∷ʳ : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n) - applyDownFrom-∷ʳ : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n) - upTo-∷ʳ : upTo n ∷ʳ n ≡ upTo (suc n) - downFrom-∷ʳ : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n) - reverse-selfInverse : SelfInverse {A = List A} _≡_ reverse - reverse-applyUpTo : reverse (applyUpTo f n) ≡ applyDownFrom f n - reverse-upTo : reverse (upTo n) ≡ downFrom n - reverse-applyDownFrom : reverse (applyDownFrom f n) ≡ applyUpTo f n - reverse-downFrom : reverse (downFrom n) ≡ upTo n - mapMaybe-map : mapMaybe f ∘ map g ≗ mapMaybe (f ∘ g) - map-mapMaybe : map g ∘ mapMaybe f ≗ mapMaybe (Maybe.map g ∘ f) - align-map : align (map f xs) (map g ys) ≡ map (map f g) (align xs ys) - zip-map : zip (map f xs) (map g ys) ≡ map (map f g) (zip xs ys) - unzipWith-map : unzipWith f ∘ map g ≗ unzipWith (f ∘ g) - map-unzipWith : map (map g) (map h) ∘ unzipWith f ≗ unzipWith (map g h ∘ f) - unzip-map : unzip ∘ map (map f g) ≗ map (map f) (map g) ∘ unzip - splitAt-map : splitAt n ∘ map f ≗ map (map f) (map f) ∘ splitAt n - uncons-map : uncons ∘ map f ≗ map (map f (map f)) ∘ uncons - last-map : last ∘ map f ≗ map f ∘ last - tail-map : tail ∘ map f ≗ map (map f) ∘ tail - mapMaybe-cong : f ≗ g → mapMaybe f ≗ mapMaybe g - zipWith-cong : (∀ a b → f a b ≡ g a b) → ∀ as → zipWith f as ≗ zipWith g as - unzipWith-cong : f ≗ g → unzipWith f ≗ unzipWith g - foldl-cong : (∀ x y → f x y ≡ g x y) → ∀ x → foldl f x ≗ foldl g x - alignWith-flip : alignWith f xs ys ≡ alignWith (f ∘ swap) ys xs - alignWith-comm : f ∘ swap ≗ f → alignWith f xs ys ≡ alignWith f ys xs - align-flip : align xs ys ≡ map swap (align ys xs) - zip-flip : zip xs ys ≡ map swap (zip ys xs) - unzipWith-swap : unzipWith (swap ∘ f) ≗ swap ∘ unzipWith f - unzip-swap : unzip ∘ map swap ≗ swap ∘ unzip - take-take : take n (take m xs) ≡ take (n ⊓ m) xs - take-drop : take n (drop m xs) ≡ drop m (take (m + n) xs) - zip-unzip : uncurry′ zip ∘ unzip ≗ id - unzipWith-zipWith : f ∘ uncurry′ g ≗ id → - length xs ≡ length ys → - unzipWith f (zipWith g xs ys) ≡ (xs , ys) - unzip-zip : length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys) - mapMaybe-++ : mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys - unzipWith-++ : unzipWith f (xs ++ ys) ≡ - zip _++_ _++_ (unzipWith f xs) (unzipWith f ys) - catMaybes-concatMap : catMaybes ≗ concatMap fromMaybe - catMaybes-++ : catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys - map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f) - Any-catMaybes⁺ : Any (M.Any P) xs → Any P (catMaybes xs) - mapMaybeIsInj₁∘mapInj₁ : mapMaybe isInj₁ (map inj₁ xs) ≡ xs - mapMaybeIsInj₁∘mapInj₂ : mapMaybe isInj₁ (map inj₂ xs) ≡ [] - mapMaybeIsInj₂∘mapInj₂ : mapMaybe isInj₂ (map inj₂ xs) ≡ xs - mapMaybeIsInj₂∘mapInj₁ : mapMaybe isInj₂ (map inj₁ xs) ≡ [] - ``` - -* In `Data.List.Relation.Binary.Pointwise.Base`: - ```agda - unzip : Pointwise (R ; S) ⇒ (Pointwise R ; Pointwise S) - ``` - -* In `Data.Maybe.Relation.Binary.Pointwise`: - ```agda - pointwise⊆any : Pointwise R (just x) ⊆ Any (R x) - ``` - -* In `Data.List.Relation.Binary.Sublist.Setoid`: - ```agda - ⊆-upper-bound : ∀ {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) → UpperBound τ σ - ``` - -* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`: - ```agda - ⊆-trans-idˡ : (trans-reflˡ : ∀ {x y} (p : x ≈ y) → trans ≈-refl p ≡ p) → - (pxs : xs ⊆ ys) → ⊆-trans ⊆-refl pxs ≡ pxs - ⊆-trans-idʳ : (trans-reflʳ : ∀ {x y} (p : x ≈ y) → trans p ≈-refl ≡ p) → - (pxs : xs ⊆ ys) → ⊆-trans pxs ⊆-refl ≡ pxs - ⊆-trans-assoc : (≈-assoc : ∀ {w x y z} (p : w ≈ x) (q : x ≈ y) (r : y ≈ z) → - trans p (trans q r) ≡ trans (trans p q) r) → - (ps : as ⊆ bs) (qs : bs ⊆ cs) (rs : cs ⊆ ds) → - ⊆-trans ps (⊆-trans qs rs) ≡ ⊆-trans (⊆-trans ps qs) rs - ``` - -* In `Data.List.Relation.Binary.Subset.Setoid.Properties`: - ```agda - map⁺ : f Preserves _≈_ ⟶ _≈′_ → as ⊆ bs → map f as ⊆′ map f bs - - reverse-selfAdjoint : as ⊆ reverse bs → reverse as ⊆ bs - reverse⁺ : as ⊆ bs → reverse as ⊆ reverse bs - reverse⁻ : reverse as ⊆ reverse bs → as ⊆ bs - ``` - -* In `Data.List.Relation.Unary.All`: - ```agda - universal-U : Universal (All U) - ``` - -* In `Data.List.Relation.Unary.All.Properties`: - ```agda - All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs) - Any-catMaybes⁺ : All (Maybe.Any P) xs → All P (catMaybes xs) - ``` - -* In `Data.List.Relation.Unary.AllPairs.Properties`: - ```agda - catMaybes⁺ : AllPairs (Pointwise R) xs → AllPairs R (catMaybes xs) - tabulate⁺-< : (i < j → R (f i) (f j)) → AllPairs R (tabulate f) - ``` - -* In `Data.List.Relation.Unary.Any.Properties`: - ```agda - map-cong : (f g : P ⋐ Q) → (∀ {x} (p : P x) → f p ≡ g p) → - (p : Any P xs) → Any.map f p ≡ Any.map g p - ``` - -* In `Data.List.Relation.Ternary.Appending.Setoid.Properties`: - ```agda - through→ : ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs → - ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs - through← : ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs → - ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs - assoc→ : ∃[ xs ] Appending as bs xs × Appending xs cs ds → - ∃[ ys ] Appending bs cs ys × Appending as ys ds - ``` - -* In `Data.List.Relation.Ternary.Appending.Properties`: - ```agda - through→ : (R ⇒ (S ; T)) → ((U ; V) ⇒ (W ; T)) → - ∃[ xs ] Pointwise U as xs × Appending V R xs bs cs → - ∃[ ys ] Appending W S as bs ys × Pointwise T ys cs - through← : ((R ; S) ⇒ T) → ((U ; S) ⇒ (V ; W)) → - ∃[ ys ] Appending U R as bs ys × Pointwise S ys cs → - ∃[ xs ] Pointwise V as xs × Appending W T xs bs cs - assoc→ : (R ⇒ (S ; T)) → ((U ; V) ⇒ (W ; T)) → ((Y ; V) ⇒ X) → - ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds → - ∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds - assoc← : ((S ; T) ⇒ R) → ((W ; T) ⇒ (U ; V)) → (X ⇒ (Y ; V)) → - ∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds → - ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds - ``` - -* In `Data.Nat.Divisibility`: - ```agda - quotient≢0 : m ∣ n → .{{NonZero n}} → NonZero quotient - - m∣n⇒n≡quotient*m : m ∣ n → n ≡ quotient * m - m∣n⇒n≡m*quotient : m ∣ n → n ≡ m * quotient - quotient-∣ : m ∣ n → quotient ∣ n - quotient>1 : m ∣ n → m < n → 1 < quotient - quotient-< : m ∣ n → .{{NonTrivial m}} → .{{NonZero n}} → quotient < n - n/m≡quotient : m ∣ n → .{{_ : NonZero m}} → n / m ≡ quotient - - m/n≡0⇒m⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n - productOfPrimes≢0 : All Prime as → NonZero (product as) - productOfPrimes≥1 : All Prime as → product as ≥ 1 - ``` - -* Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`: - ```agda - product-↭ : product Preserves _↭_ ⟶ _≡_ - catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys - mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys - ``` - -* Added new proofs to `Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe`: - ```agda - catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys - mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys - ``` - -* Added some very-dependent map and zipWith to `Data.Product`. - ```agda - map-Σ : {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} → - (f : (x : A) → B x) → (∀ {x} → (y : P x) → Q y (f x)) → - ((x , y) : Σ A P) → Σ (B x) (Q y) - - map-Σ′ : {B : A → Set b} {P : Set p} {Q : P → Set q} → - (f : (x : A) → B x) → ((x : P) → Q x) → ((x , y) : A × P) → B x × Q y - - zipWith : {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s} - (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) → - (_*_ : (x : C) → (y : R x) → S x y) → - ((a , p) : Σ A P) → ((b , q) : Σ B Q) → - S (a ∙ b) (p ∘ q) - - ``` - -* In `Data.Rational.Properties`: - ```agda - 1≢0 : 1ℚ ≢ 0ℚ - - #⇒invertible : p ≢ q → Invertible 1ℚ _*_ (p - q) - invertible⇒# : Invertible 1ℚ _*_ (p - q) → p ≢ q - - isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ - isHeytingField : IsHeytingField _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ - heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ - heytingField : HeytingField 0ℓ 0ℓ 0ℓ - ``` - -* Added new functions in `Data.String.Base`: - ```agda - map : (Char → Char) → String → String - between : String → String → String → String - ``` - -* Re-exported new types and functions in `IO`: - ```agda - BufferMode : Set - noBuffering : BufferMode - lineBuffering : BufferMode - blockBuffering : Maybe ℕ → BufferMode - Handle : Set - stdin : Handle - stdout : Handle - stderr : Handle - hSetBuffering : Handle → BufferMode → IO ⊤ - hGetBuffering : Handle → IO BufferMode - hFlush : Handle → IO ⊤ - ``` - -* Added new functions in `IO.Base`: - ```agda - whenInj₂ : E ⊎ A → (A → IO ⊤) → IO ⊤ - forever : IO ⊤ → IO ⊤ - ``` - -* In `IO.Primitive.Core`: - ```agda - _>>_ : IO A → IO B → IO B - ``` - -* In `Data.Word64.Base`: - ```agda - _≤_ : Rel Word64 zero - show : Word64 → String - ``` - -* Added new definition in `Relation.Binary.Construct.Closure.Transitive` - ```agda - transitive⁻ : Transitive _∼_ → TransClosure _∼_ ⇒ _∼_ - ``` - -* Added new definition in `Relation.Unary` - ``` - Stable : Pred A ℓ → Set _ - ``` - -* In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can - be used infix. - -* Added new proofs in `Relation.Binary.Construct.Composition`: - ```agda - transitive⇒≈;≈⊆≈ : Transitive ≈ → (≈ ; ≈) ⇒ ≈ - ``` - -* Added new definitions in `Relation.Binary.Definitions` - ``` - Stable _∼_ = ∀ x y → Nullary.Stable (x ∼ y) - Empty _∼_ = ∀ {x y} → ¬ (x ∼ y) - ``` - -* Added new proofs in `Relation.Binary.Properties.Setoid`: - ```agda - ≉-irrefl : Irreflexive _≈_ _≉_ - ≈;≈⇒≈ : _≈_ ; _≈_ ⇒ _≈_ - ≈⇒≈;≈ : _≈_ ⇒ _≈_ ; _≈_ - ``` - -* Added new definitions in `Relation.Nullary` - ``` - Recomputable : Set _ - WeaklyDecidable : Set _ - ``` - -* Added new proof in `Relation.Nullary.Decidable.Core`: - ```agda - recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q - ``` - -* Added new proof in `Relation.Nullary.Decidable`: - ```agda - ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋ - ``` - -* Added new definitions in `Relation.Nullary.Negation.Core`: - ```agda - contradiction-irr : .A → ¬ A → Whatever - ``` - -* Added new definitions in `Relation.Nullary.Reflects`: - ```agda - recompute : Reflects A b → Recomputable A - recompute-constant : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q - ``` - -* Added new definitions in `Relation.Unary` - ``` - Stable : Pred A ℓ → Set _ - WeaklyDecidable : Pred A ℓ → Set _ - ``` - -* Enhancements to `Tactic.Cong` - see `README.Tactic.Cong` for details. - - Provide a marker function, `⌞_⌟`, for user-guided anti-unification. - - Improved support for equalities between terms with instance arguments, - such as terms that contain `_/_` or `_%_`. From 8fa69d9a5078709a70ad04bd3cb0b2922b667f3d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 28 Jul 2024 10:40:10 +0100 Subject: [PATCH 27/27] update `CHANGELOG` --- CHANGELOG.md | 110 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 110 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 80da9ee48e..0478fac5ed 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -24,5 +24,115 @@ Deprecated names New modules ----------- +* Bundled morphisms between (raw) algebraic structures: + ``` + Algebra.Morphism.Bundles + ``` + Additions to existing modules ----------------------------- + +* In `Algebra.Bundles.KleeneAlgebra`: + ```agda + rawKleeneAlgebra : RawKleeneAlgebra _ _ + ``` + +* In `Algebra.Bundles.Raw` + ```agda + record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) + ``` + +* 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`: + ```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 _ + ``` + +* In `Algebra.Morphism.Structures.RingMorphisms` + ```agda + isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧ + ``` + +* In `Algebra.Morphism.Structures.RingWithoutOneMorphisms` + ```agda + isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧ + ``` + +* In `Algebra.Structures.RingWithoutOne`: + ```agda + isNearSemiring : IsNearSemiring _ _ + ```