Add IsIdempotentMonoid and IsCommutativeBand to Algebra.Structures (#2402)

* fix #2138

* fixed `Structures`; added `Bundles`

* added fields; plus redefined `IsSemilattice` and `IsBoundedSemilattice` as aliases

* `fix-whitespace`

* reexported `comm`

* fixed `Lattice.Bundles`

* knock-on

* added text about redefinition of `Is(Bounded)Semilattice`

* add manifest fields to `IsIdempotentSemiring`

* final missing `Bundles`

* `CHANGELOG`

Author: jamesmckinna

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

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,21 @@ 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
     ; semigroup; commutativeSemigroup
     ; 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 _*_

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
@@ -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#