diff --git a/CHANGELOG.md b/CHANGELOG.md index 7d1e9b4e6c..9f8d6de9bd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -45,6 +45,11 @@ Minor improvements `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 ------------------ @@ -244,8 +249,16 @@ 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.Raw` ```agda record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) @@ -364,6 +377,14 @@ Additions to existing modules * 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 diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index a86529f5cd..d96584a733 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -243,6 +243,30 @@ record CommutativeSemigroup c ℓ : Set (suc (c ⊔ ℓ)) where commutativeMagma : CommutativeMagma c ℓ commutativeMagma = record { isCommutativeMagma = isCommutativeMagma } +record CommutativeBand c ℓ : Set (suc (c ⊔ ℓ)) where + infixl 7 _∙_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∙_ : Op₂ Carrier + isCommutativeBand : IsCommutativeBand _≈_ _∙_ + + open IsCommutativeBand isCommutativeBand public + + band : Band _ _ + band = record { isBand = isBand } + + open Band band public + using (_≉_; magma; rawMagma; semigroup) + + commutativeSemigroup : CommutativeSemigroup c ℓ + commutativeSemigroup = record { isCommutativeSemigroup = isCommutativeSemigroup } + + open CommutativeSemigroup commutativeSemigroup public + using (commutativeMagma) + + ------------------------------------------------------------------------ -- Bundles with 1 binary operation & 1 element ------------------------------------------------------------------------ @@ -315,6 +339,27 @@ record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where open CommutativeSemigroup commutativeSemigroup public using (commutativeMagma) +record IdempotentMonoid c ℓ : Set (suc (c ⊔ ℓ)) where + infixl 7 _∙_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∙_ : Op₂ Carrier + ε : Carrier + isIdempotentMonoid : IsIdempotentMonoid _≈_ _∙_ ε + + open IsIdempotentMonoid isIdempotentMonoid public + + monoid : Monoid _ _ + monoid = record { isMonoid = isMonoid } + + open Monoid monoid public + using (_≉_; rawMagma; magma; semigroup; unitalMagma; rawMonoid) + + band : Band _ _ + band = record { isBand = isBand } + record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ @@ -331,6 +376,12 @@ record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where commutativeMonoid : CommutativeMonoid _ _ commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid } + idempotentMonoid : IdempotentMonoid _ _ + idempotentMonoid = record { isIdempotentMonoid = isIdempotentMonoid } + + commutativeBand : CommutativeBand _ _ + commutativeBand = record { isCommutativeBand = isCommutativeBand } + open CommutativeMonoid commutativeMonoid public using ( _≉_; rawMagma; magma; unitalMagma; commutativeMagma @@ -338,6 +389,8 @@ record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where ; rawMonoid; monoid ) + open CommutativeBand commutativeBand public + using (band) -- Idempotent commutative monoids are also known as bounded lattices. -- Note that the BoundedLattice necessarily uses the notation inherited @@ -778,6 +831,16 @@ record IdempotentSemiring c ℓ : Set (suc (c ⊔ ℓ)) where ; rawSemiring ) + +-idempotentCommutativeMonoid : IdempotentCommutativeMonoid _ _ + +-idempotentCommutativeMonoid = record { isIdempotentCommutativeMonoid = +-isIdempotentCommutativeMonoid } + + open IdempotentCommutativeMonoid +-idempotentCommutativeMonoid public + using () + renaming ( band to +-band + ; commutativeBand to +-commutativeBand + ; idempotentMonoid to +-idempotentMonoid + ) + record KleeneAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 _⋆ infixl 7 _*_ diff --git a/src/Algebra/Lattice/Bundles.agda b/src/Algebra/Lattice/Bundles.agda index 28fd07d5b3..51318bf65c 100644 --- a/src/Algebra/Lattice/Bundles.agda +++ b/src/Algebra/Lattice/Bundles.agda @@ -43,7 +43,7 @@ record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where _∙_ : Op₂ Carrier isSemilattice : IsSemilattice _≈_ _∙_ - open IsSemilattice isSemilattice public + open IsSemilattice _≈_ isSemilattice public band : Band c ℓ band = record { isBand = isBand } diff --git a/src/Algebra/Lattice/Construct/Subst/Equality.agda b/src/Algebra/Lattice/Construct/Subst/Equality.agda index 8a498afbb2..48393f2b64 100644 --- a/src/Algebra/Lattice/Construct/Subst/Equality.agda +++ b/src/Algebra/Lattice/Construct/Subst/Equality.agda @@ -35,7 +35,7 @@ isSemilattice : IsSemilattice ≈₁ ∧ → IsSemilattice ≈₂ ∧ isSemilattice S = record { isBand = isBand S.isBand ; comm = comm S.comm - } where module S = IsSemilattice S + } where module S = IsSemilattice ≈₁ S isLattice : IsLattice ≈₁ ∨ ∧ → IsLattice ≈₂ ∨ ∧ isLattice {∨} {∧} S = record diff --git a/src/Algebra/Lattice/Structures.agda b/src/Algebra/Lattice/Structures.agda index 116ed85271..c82ed2db9e 100644 --- a/src/Algebra/Lattice/Structures.agda +++ b/src/Algebra/Lattice/Structures.agda @@ -31,11 +31,10 @@ open import Algebra.Structures _≈_ ------------------------------------------------------------------------ -- Structures with 1 binary operation -record IsSemilattice (∙ : Op₂ A) : Set (a ⊔ ℓ) where - field - isBand : IsBand ∙ - comm : Commutative ∙ - +IsSemilattice = IsCommutativeBand +module IsSemilattice {∙} (L : IsSemilattice ∙) where + open IsCommutativeBand L public + using (isBand; comm) open IsBand isBand public -- Used to bring names appropriate for a meet semilattice into scope. @@ -67,12 +66,7 @@ IsBoundedSemilattice = IsIdempotentCommutativeMonoid module IsBoundedSemilattice {∙ ε} (L : IsBoundedSemilattice ∙ ε) where open IsIdempotentCommutativeMonoid L public - - isSemilattice : IsSemilattice ∙ - isSemilattice = record - { isBand = isBand - ; comm = comm - } + renaming (isCommutativeBand to isSemilattice) -- Used to bring names appropriate for a bounded meet semilattice diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 3cdc55a4b5..b58245e6df 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -153,6 +153,20 @@ record IsCommutativeSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where ; comm = comm } + +record IsCommutativeBand (∙ : Op₂ A) : Set (a ⊔ ℓ) where + field + isBand : IsBand ∙ + comm : Commutative ∙ + + open IsBand isBand public + + isCommutativeSemigroup : IsCommutativeSemigroup ∙ + isCommutativeSemigroup = record { isSemigroup = isSemigroup ; comm = comm } + + open IsCommutativeSemigroup isCommutativeSemigroup public + using (isCommutativeMagma) + ------------------------------------------------------------------------ -- Structures with 1 binary operation & 1 element ------------------------------------------------------------------------ @@ -208,6 +222,17 @@ record IsCommutativeMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where using (isCommutativeMagma) +record IsIdempotentMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where + field + isMonoid : IsMonoid ∙ ε + idem : Idempotent ∙ + + open IsMonoid isMonoid public + + isBand : IsBand ∙ + isBand = record { isSemigroup = isSemigroup ; idem = idem } + + record IsIdempotentCommutativeMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where field @@ -216,9 +241,14 @@ record IsIdempotentCommutativeMonoid (∙ : Op₂ A) open IsCommutativeMonoid isCommutativeMonoid public - isBand : IsBand ∙ - isBand = record { isSemigroup = isSemigroup ; idem = idem } + isIdempotentMonoid : IsIdempotentMonoid ∙ ε + isIdempotentMonoid = record { isMonoid = isMonoid ; idem = idem } + open IsIdempotentMonoid isIdempotentMonoid public + using (isBand) + + isCommutativeBand : IsCommutativeBand ∙ + isCommutativeBand = record { isBand = isBand ; comm = comm } ------------------------------------------------------------------------ -- Structures with 1 binary operation, 1 unary operation & 1 element @@ -584,6 +614,20 @@ record IsIdempotentSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where open IsSemiring isSemiring public + +-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid + 0# + +-isIdempotentCommutativeMonoid = record + { isCommutativeMonoid = +-isCommutativeMonoid + ; idem = +-idem + } + + open IsIdempotentCommutativeMonoid +-isIdempotentCommutativeMonoid public + using () + renaming ( isCommutativeBand to +-isCommutativeBand + ; isBand to +-isBand + ; isIdempotentMonoid to +-isIdempotentMonoid + ) + + record IsKleeneAlgebra (+ * : Op₂ A) (⋆ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where field isIdempotentSemiring : IsIdempotentSemiring + * 0# 1#