Add CancellativeCommutativeSemiring (#1308)

Author: mechvel

CHANGELOG.md

@@ -44,6 +44,7 @@ Other minor additions
   ```agda
   RawNearSemiring c ℓ : Set (suc (c ⊔ ℓ))
   RawLattice c ℓ : Set (suc (c ⊔ ℓ))
+  CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ))
   ```
 
 * Added new records to `Algebra.Morphism.Structures`:
@@ -59,4 +60,16 @@ Other minor additions
   IsLatticeIsomorphism   (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
   ```
 
+* Added new definitions to `Algebra.Definitions`:
+  ```agda
+  AlmostLeftCancellative  e _•_ = ∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z
+  AlmostRightCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z
+  AlmostCancellative      e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_
+  ```
+
+* Added new record to `Algebra.Structures`:
+  ```agda
+  IsCancellativeCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ)
+  ```
+
 * Add version to library name

src/Algebra/Bundles.agda

@@ -670,6 +670,22 @@ record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
     }
 
 
+record CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier                           : Set c
+    _≈_                               : Rel Carrier ℓ
+    _+_                               : Op₂ Carrier
+    _*_                               : Op₂ Carrier
+    0#                                : Carrier
+    1#                                : Carrier
+    isCancellativeCommutativeSemiring : IsCancellativeCommutativeSemiring _≈_ _+_ _*_ 0# 1#
+
+  open IsCancellativeCommutativeSemiring isCancellativeCommutativeSemiring public
+
+
 ------------------------------------------------------------------------
 -- Bundles with 2 binary operations, 1 unary operation & 2 elements
 ------------------------------------------------------------------------

src/Algebra/Definitions.agda

@@ -10,6 +10,7 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary.Core
+open import Relation.Nullary using (¬_)
 
 module Algebra.Definitions
   {a ℓ} {A : Set a}   -- The underlying set
@@ -118,5 +119,14 @@ RightCancellative _•_ = ∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z
 Cancellative : Op₂ A → Set _
 Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_)
 
+AlmostLeftCancellative : A → Op₂ A → Set _
+AlmostLeftCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z
+
+AlmostRightCancellative : A → Op₂ A → Set _
+AlmostRightCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z
+
+AlmostCancellative : A → Op₂ A → Set _
+AlmostCancellative e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_
+
 Interchangable : Op₂ A → Op₂ A → Set _
 Interchangable _∘_ _∙_ = ∀ w x y z → ((w ∙ x) ∘ (y ∙ z)) ≈ ((w ∘ y) ∙ (x ∘ z))

src/Algebra/Structures.agda

@@ -425,6 +425,15 @@ record IsCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
     }
 
 
+record IsCancellativeCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+  field
+    isCommutativeSemiring : IsCommutativeSemiring + * 0# 1#
+    *-cancelˡ-nonZero     : AlmostLeftCancellative 0# *
+
+  open IsCommutativeSemiring isCommutativeSemiring public
+
+
+
 ------------------------------------------------------------------------
 -- Structures with 2 binary operations, 1 unary operation & 2 elements
 ------------------------------------------------------------------------