Add IsIdempotentMonoid and IsCommutativeBand to Algebra.Structures

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
 ------------------
 
@@ -234,6 +239,8 @@ 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 ⊔ ℓ))
  ```
 
 * In `Algebra.Bundles.Raw`
@@ -350,6 +357,9 @@ 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 _
+ ```
 
 * In `Algebra.Structures.IsGroup`:
  ```agda

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,13 +376,19 @@ record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
  commutativeMonoid : CommutativeMonoid _ _
  commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
 
+ idempotentMonoid : IdempotentMonoid _ _
+ idempotentMonoid = record { isIdempotentMonoid = isIdempotentMonoid }
+
  open CommutativeMonoid commutativeMonoid public
  using
  ( _≉_; rawMagma; magma; unitalMagma; commutativeMagma
  ; semigroup; commutativeSemigroup
  ; rawMonoid; monoid
  )
 
+ open IdempotentMonoid idempotentMonoid public
+ using (band)
+
 
 -- Idempotent commutative monoids are also known as bounded lattices.
 -- Note that the BoundedLattice necessarily uses the notation inherited

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 }

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

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

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