add: (Is)IntegralSemiring

Author: jamesmckinna

CHANGELOG.md

@@ -57,6 +57,11 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Bundles`:
+  ```agda
+  IntegralSemiring        : (c ℓ : Level) → Set _
+  ```
+
 * In `Algebra.Consequences.Base`:
   ```agda
   integral⇒noZeroDivisors : Integral _≈_ 1# 0# _•_ → ¬ (1# ≈ 0#) →
@@ -98,3 +103,8 @@ Additions to existing modules
   Integral       : A → A → Op₂ A → Set _
   ```
   (see [discussion on issue #2554](https://github.com/agda/agda-stdlib/issues/2554))
+
+* In `Algebra.Structures`:
+  ```agda
+  IsIntegralSemiring        : (+ * : Op₂ A) (0# 1# : A) → Set _
+  ```

src/Algebra/Bundles.agda

@@ -841,6 +841,36 @@ record IdempotentSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
              ; idempotentMonoid to +-idempotentMonoid
              )
 
+record IntegralSemiring 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
+    isIntegralSemiring : IsIntegralSemiring _≈_ _+_ _*_ 0# 1#
+
+  open IsIntegralSemiring isIntegralSemiring public
+
+  semiring : Semiring _ _
+  semiring = record { isSemiring = isSemiring }
+
+  open Semiring semiring public
+    using
+    ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
+    ; +-semigroup; +-commutativeSemigroup
+    ; *-rawMagma; *-magma; *-semigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; *-rawMonoid; *-monoid
+    ; nearSemiring; semiringWithoutOne
+    ; semiringWithoutAnnihilatingZero
+    ; rawSemiring
+    )
+
 record KleeneAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
   infix  8 _⋆
   infixl 7 _*_

src/Algebra/Structures.agda

@@ -582,6 +582,14 @@ record IsSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
     )
 
 
+record IsIntegralSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+  field
+    isSemiring : IsSemiring + * 0# 1#
+    integral   : Integral 1# 0# *
+
+  open IsSemiring isSemiring public
+
+
 record IsCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
   field
     isSemiring : IsSemiring + * 0# 1#