Add IsIdempotentMonoid and IsCommutativeBand to Algebra.Structures

CHANGELOG.md

@@ -234,6 +234,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 +352,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/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,11 @@ 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)
 
 ------------------------------------------------------------------------
 -- Structures with 1 binary operation, 1 unary operation & 1 element