Define IsUnitalMagma and IsQuasigroup

CHANGELOG.md

@@ -30,19 +30,26 @@ New modules
 Other minor additions
 ---------------------
 
-* In `Algebra.Bundles`, `Lattice` now provides
+* Added new definitions to `Algebra.Bundles`:
+  ```agda
+  record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ))
+  record Quasigroup  c ℓ : Set (suc (c ⊔ ℓ))
+  ```
+  and the existing record `Lattice` now provides
   ```agda
   ∨-commutativeSemigroup : CommutativeSemigroup c ℓ
   ∧-commutativeSemigroup : CommutativeSemigroup c ℓ
   ```
   and their corresponding algebraic subbundles.
 
-* In `Algebra.Structures`, `IsLattice` now provides
+* Added new definitions to `Algebra.Structures`:
+  ```agda
+  record IsUnitalMagma (_∙_ : Op₂ A) (ε : A) : Set (a ⊔ ℓ)
+  record IsQuasigroup  (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ)
+  ```
+  and the existing record `IsLattice` now provides
   ```
   ∨-isCommutativeSemigroup : IsCommutativeSemigroup ∨
   ∧-isCommutativeSemigroup : IsCommutativeSemigroup ∧
   ```
   and their corresponding algebraic substructures.
-
-Other minor additions
----------------------

src/Algebra/Bundles.agda

@@ -187,6 +187,25 @@ record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
     using (_≉_)
 
 
+record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier  : Set c
+    _≈_      : Rel Carrier ℓ
+    _∙_      : Op₂ Carrier
+    ε        : Carrier
+    isUnitalMagma : IsUnitalMagma _≈_ _∙_ ε
+
+  open IsUnitalMagma isUnitalMagma public
+
+  magma : Magma c ℓ
+  magma = record { isMagma = isMagma }
+
+  open Magma magma public
+    using (_≉_; rawMagma)
+
+
 record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
   infix  4 _≈_
@@ -208,6 +227,9 @@ record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where
   rawMonoid : RawMonoid _ _
   rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε}
 
+  unitalMagma : UnitalMagma _ _
+  unitalMagma = record { isUnitalMagma = isUnitalMagma  }
+
 
 record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
@@ -225,7 +247,7 @@ record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
   monoid = record { isMonoid = isMonoid }
 
   open Monoid monoid public
-    using (_≉_; rawMagma; magma; semigroup; rawMonoid)
+    using (_≉_; rawMagma; magma; semigroup; unitalMagma; rawMonoid)
 
   commutativeSemigroup : CommutativeSemigroup _ _
   commutativeSemigroup = record { isCommutativeSemigroup = isCommutativeSemigroup }
@@ -251,7 +273,8 @@ record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open CommutativeMonoid commutativeMonoid public
     using
-    ( _≉_; rawMagma; magma; commutativeMagma; semigroup; commutativeSemigroup
+    ( _≉_; rawMagma; magma; unitalMagma; commutativeMagma
+    ; semigroup; commutativeSemigroup
     ; rawMonoid; monoid
     )
 
@@ -292,6 +315,27 @@ record RawGroup c ℓ : Set (suc (c ⊔ ℓ)) where
     using (_≉_; rawMagma)
 
 
+record Quasigroup c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 _⁻¹
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _∙_     : Op₂ Carrier
+    ε       : Carrier
+    _⁻¹     : Op₁ Carrier
+    isQuasigroup : IsQuasigroup _≈_ _∙_ ε _⁻¹
+
+  open IsQuasigroup isQuasigroup public
+
+  magma : Magma _ _
+  magma = record { isMagma = isMagma }
+
+  open Magma magma public
+    using (_≉_; rawMagma)
+
+
 record Group c ℓ : Set (suc (c ⊔ ℓ)) where
   infix  8 _⁻¹
   infixl 7 _∙_
@@ -313,7 +357,13 @@ record Group c ℓ : Set (suc (c ⊔ ℓ)) where
   monoid = record { isMonoid = isMonoid }
 
   open Monoid monoid public
-    using (_≉_; rawMagma; magma; semigroup; rawMonoid)
+    using (_≉_; rawMagma; magma; semigroup; unitalMagma; rawMonoid)
+
+  quasigroup : Quasigroup c ℓ
+  quasigroup = record
+    { isQuasigroup = isQuasigroup
+    }
+
 
 record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
   infix  8 _⁻¹
@@ -332,8 +382,10 @@ record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
   group : Group _ _
   group = record { isGroup = isGroup }
 
-  open Group group public
-    using (_≉_; rawMagma; magma; semigroup; monoid; rawMonoid; rawGroup)
+  open Group group public using
+    (_≉_; rawMagma; magma; semigroup
+    ; rawMonoid; monoid; rawGroup; quasigroup
+    )
 
   commutativeMonoid : CommutativeMonoid _ _
   commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
@@ -475,10 +527,11 @@ record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open Monoid +-monoid public
     using (_≉_) renaming
-    ( rawMagma  to +-rawMagma
-    ; magma     to +-magma
-    ; semigroup to +-semigroup
-    ; rawMonoid to +-rawMonoid
+    ( rawMagma    to  +-rawMagma
+    ; magma       to  +-magma
+    ; semigroup   to  +-semigroup
+    ; unitalMagma to  +-unitalMagma
+    ; rawMonoid   to  +-rawMonoid
     )
 
   *-semigroup : Semigroup _ _
@@ -510,7 +563,7 @@ record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open NearSemiring nearSemiring public
     using
-    ( _≉_; +-rawMagma; +-magma; +-semigroup
+    ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-semigroup
     ; +-rawMonoid; +-monoid
     ; *-rawMagma; *-magma; *-semigroup
     ; rawNearSemiring
@@ -548,7 +601,7 @@ record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open SemiringWithoutOne semiringWithoutOne public
     using
-    ( _≉_; +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
+    ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-semigroup; +-commutativeSemigroup
     ; *-rawMagma; *-magma; *-semigroup
     ; +-rawMonoid; +-monoid; +-commutativeMonoid
     ; nearSemiring; rawNearSemiring
@@ -626,6 +679,7 @@ record SemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where
     using (_≉_) renaming
     ( rawMagma             to +-rawMagma
     ; magma                to +-magma
+    ; unitalMagma          to +-unitalMagma
     ; commutativeMagma     to +-commutativeMagma
     ; semigroup            to +-semigroup
     ; commutativeSemigroup to +-commutativeSemigroup
@@ -669,7 +723,8 @@ record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where
   open SemiringWithoutAnnihilatingZero
          semiringWithoutAnnihilatingZero public
     using
-    ( _≉_; +-rawMagma;  +-magma;  +-commutativeMagma; +-semigroup; +-commutativeSemigroup
+    ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
+    ; +-semigroup; +-commutativeSemigroup
     ; *-rawMagma;  *-magma;  *-semigroup
     ; +-rawMonoid; +-monoid; +-commutativeMonoid
     ; *-rawMonoid; *-monoid
@@ -704,7 +759,8 @@ record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open Semiring semiring public
     using
-    ( _≉_; +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
+    ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
+    ; +-semigroup; +-commutativeSemigroup
     ; *-rawMagma; *-magma; *-semigroup
     ; +-rawMonoid; +-monoid; +-commutativeMonoid
     ; *-rawMonoid; *-monoid
@@ -752,7 +808,8 @@ record CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open CommutativeSemiring commutativeSemiring public
     using
-    ( +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
+    ( +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
+    ; +-semigroup; +-commutativeSemigroup
     ; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup
     ; +-rawMonoid; +-monoid; +-commutativeMonoid
     ; *-rawMonoid; *-monoid; *-commutativeMonoid
@@ -808,6 +865,7 @@ record RawRing c ℓ : Set (suc (c ⊔ ℓ)) where
     ; _⁻¹ = -_
     }
 
+
 record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
   infix  8 -_
   infixl 7 _*_
@@ -833,7 +891,8 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open Semiring semiring public
     using
-    ( _≉_; +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
+    ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
+    ; +-semigroup; +-commutativeSemigroup
     ; *-rawMagma; *-magma; *-semigroup
     ; +-rawMonoid; +-monoid ; +-commutativeMonoid
     ; *-rawMonoid; *-monoid
@@ -842,7 +901,7 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
     )
 
   open AbelianGroup +-abelianGroup public
-    using () renaming (group to +-group)
+    using () renaming (group to +-group; quasigroup to +-quasigroup)
 
   rawRing : RawRing _ _
   rawRing = record
@@ -875,15 +934,16 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
   ring : Ring _ _
   ring = record { isRing = isRing }
 
-  open Ring ring public using (_≉_; rawRing; +-group; +-abelianGroup)
+  open Ring ring public using (_≉_; rawRing; +-quasigroup; +-group; +-abelianGroup)
 
   commutativeSemiring : CommutativeSemiring _ _
   commutativeSemiring =
     record { isCommutativeSemiring = isCommutativeSemiring }
 
   open CommutativeSemiring commutativeSemiring public
     using
-    ( +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
+    ( +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
+    ; +-semigroup; +-commutativeSemigroup
     ; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup
     ; +-rawMonoid; +-monoid; +-commutativeMonoid
     ; *-rawMonoid; *-monoid; *-commutativeMonoid

src/Algebra/Structures.agda

@@ -107,6 +107,20 @@ record IsSemilattice (∧ : Op₂ A) : Set (a ⊔ ℓ) where
 -- Structures with 1 binary operation & 1 element
 ------------------------------------------------------------------------
 
+record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
+  field
+    isMagma  : IsMagma ∙
+    identity : Identity ε ∙
+
+  open IsMagma isMagma public
+
+  identityˡ : LeftIdentity ε ∙
+  identityˡ = proj₁ identity
+
+  identityʳ : RightIdentity ε ∙
+  identityʳ = proj₂ identity
+
+
 record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
   field
     isSemigroup : IsSemigroup ∙
@@ -120,6 +134,12 @@ record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
   identityʳ : RightIdentity ε ∙
   identityʳ = proj₂ identity
 
+  isUnitalMagma : IsUnitalMagma ∙ ε
+  isUnitalMagma = record
+    { isMagma  = isMagma
+    ; identity = identity
+    }
+
 
 record IsCommutativeMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
   field
@@ -163,6 +183,20 @@ module IsBoundedLattice {∙ : Op₂ A}
 -- Structures with 1 binary operation, 1 unary operation & 1 element
 ------------------------------------------------------------------------
 
+record IsQuasigroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
+  field
+    isMagma  : IsMagma _∙_
+    inverse   : Inverse ε _⁻¹ _∙_
+
+  open IsMagma isMagma public
+
+  inverseˡ : LeftInverse ε _⁻¹ _∙_
+  inverseˡ = proj₁ inverse
+
+  inverseʳ : RightInverse ε _⁻¹ _∙_
+  inverseʳ = proj₂ inverse
+
+
 record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
   field
     isMonoid  : IsMonoid _∙_ ε
@@ -189,6 +223,12 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) w
   uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique
                 setoid ∙-cong assoc identity inverseˡ
 
+  isQuasigroup : IsQuasigroup _∙_ ε _⁻¹
+  isQuasigroup = record
+    { isMagma = isMagma
+    ; inverse = inverse
+    }
+
 
 record IsAbelianGroup (∙ : Op₂ A)
                       (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
@@ -277,15 +317,16 @@ record IsNearSemiring (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
 
   open IsMonoid +-isMonoid public
     renaming
-    ( assoc       to +-assoc
-    ; ∙-cong      to +-cong
-    ; ∙-congˡ     to +-congˡ
-    ; ∙-congʳ     to +-congʳ
-    ; identity    to +-identity
-    ; identityˡ   to +-identityˡ
-    ; identityʳ   to +-identityʳ
-    ; isMagma     to +-isMagma
-    ; isSemigroup to +-isSemigroup
+    ( assoc         to +-assoc
+    ; ∙-cong        to +-cong
+    ; ∙-congˡ       to +-congˡ
+    ; ∙-congʳ       to +-congʳ
+    ; identity      to +-identity
+    ; identityˡ     to +-identityˡ
+    ; identityʳ     to +-identityʳ
+    ; isMagma       to +-isMagma
+    ; isUnitalMagma to +-isUnitalMagma
+    ; isSemigroup   to +-isSemigroup
     )
 
   open IsSemigroup *-isSemigroup public
@@ -306,8 +347,7 @@ record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
     distrib               : * DistributesOver +
     zero                  : Zero 0# *
 
-  open IsCommutativeMonoid +-isCommutativeMonoid public
-    using ()
+  open IsCommutativeMonoid +-isCommutativeMonoid public using ()
     renaming
     ( comm                   to +-comm
     ; isMonoid               to +-isMonoid
@@ -382,6 +422,7 @@ record IsSemiringWithoutAnnihilatingZero (+ * : Op₂ A)
     ; isMagma                to +-isMagma
     ; isSemigroup            to +-isSemigroup
     ; isMonoid               to +-isMonoid
+    ; isUnitalMagma          to +-isUnitalMagma
     ; isCommutativeMagma     to +-isCommutativeMagma
     ; isCommutativeSemigroup to +-isCommutativeSemigroup
     )
@@ -490,9 +531,11 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
     ; isMagma                to +-isMagma
     ; isSemigroup            to +-isSemigroup
     ; isMonoid               to +-isMonoid
+    ; isUnitalMagma          to +-isUnitalMagma
     ; isCommutativeMagma     to +-isCommutativeMagma
     ; isCommutativeMonoid    to +-isCommutativeMonoid
     ; isCommutativeSemigroup to +-isCommutativeSemigroup
+    ; isQuasigroup           to +-isQuasigroup
     ; isGroup                to +-isGroup
     )