diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda
index bc66a893f4..fad491c7a1 100644
--- a/src/Algebra/Bundles.agda
+++ b/src/Algebra/Bundles.agda
@@ -976,11 +976,11 @@ record RingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open IsRingWithoutOne isRingWithoutOne public
 
-  nearSemiring : NearSemiring _ _
-  nearSemiring = record { isNearSemiring = isNearSemiring }
+  semiringWithoutOne : SemiringWithoutOne _ _
+  semiringWithoutOne = record { isSemiringWithoutOne = isSemiringWithoutOne }
 
-  open NearSemiring nearSemiring public
-    using (*-semigroup; *-magma)
+  open SemiringWithoutOne semiringWithoutOne public
+    using (nearSemiring; *-semigroup; *-magma)
 
   +-abelianGroup : AbelianGroup _ _
   +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }
diff --git a/src/Algebra/Properties/CommutativeMonoid.agda b/src/Algebra/Properties/CommutativeMonoid.agda
index 840155cd69..c5082bce6c 100644
--- a/src/Algebra/Properties/CommutativeMonoid.agda
+++ b/src/Algebra/Properties/CommutativeMonoid.agda
@@ -35,9 +35,24 @@ private variable
 
 
 ------------------------------------------------------------------------
--- Re-export properties of commutative semigroups
+-- Re-export properties of monoids and commutative semigroups
 
 open import Algebra.Properties.CommutativeSemigroup commutativeSemigroup public
+open import Algebra.Properties.Monoid monoid public
+  using
+    ( ε-unique
+    ; elimʳ
+    ; elimˡ
+    ; introʳ
+    ; introˡ
+    ; introᶜ
+    ; cancelˡ
+    ; cancelʳ
+    ; insertˡ
+    ; insertʳ
+    ; cancelᶜ
+    ; insertᶜ
+    )
 
 ------------------------------------------------------------------------
 -- Additional properties
diff --git a/src/Algebra/Properties/Ring.agda b/src/Algebra/Properties/Ring.agda
index 4f8eb31a14..de05b9396e 100644
--- a/src/Algebra/Properties/Ring.agda
+++ b/src/Algebra/Properties/Ring.agda
@@ -14,8 +14,26 @@ open Ring ring
 open import Relation.Binary.Reasoning.Setoid setoid
 
 ------------------------------------------------------------------------
--- Export properties of rings without a 1#.
-
+-- Export properties of semirings and rings without a 1#.
+
+open import Algebra.Properties.Semiring semiring public
+  using
+    ( 1#-unique
+    ; 1#-comm
+
+    ; *-elimʳ
+    ; *-elimˡ
+    ; *-introʳ
+    ; *-introˡ
+    ; *-introᶜ
+
+    ; *-cancelʳ
+    ; *-cancelˡ
+    ; *-insertˡ
+    ; *-insertʳ
+    ; *-cancelᶜ
+    ; *-insertᶜ
+    )
 open import Algebra.Properties.RingWithoutOne ringWithoutOne public
 
 ------------------------------------------------------------------------
diff --git a/src/Algebra/Properties/RingWithoutOne.agda b/src/Algebra/Properties/RingWithoutOne.agda
index d45edeaf0b..8f5a89fd09 100644
--- a/src/Algebra/Properties/RingWithoutOne.agda
+++ b/src/Algebra/Properties/RingWithoutOne.agda
@@ -13,6 +13,7 @@ module Algebra.Properties.RingWithoutOne {r₁ r₂} (R : RingWithoutOne r₁ r
 open RingWithoutOne R
 
 import Algebra.Properties.AbelianGroup as AbelianGroupProperties
+import Algebra.Properties.SemiringWithoutOne as SemiringWithoutOneProperties
 open import Function.Base using (_$_)
 open import Relation.Binary.Reasoning.Setoid setoid
 
@@ -22,9 +23,6 @@ open import Relation.Binary.Reasoning.Setoid setoid
 open AbelianGroupProperties +-abelianGroup public
   renaming
   ( ε⁻¹≈ε            to -0#≈0#
-  ; ∙-cancelˡ        to +-cancelˡ
-  ; ∙-cancelʳ        to +-cancelʳ
-  ; ∙-cancel         to +-cancel
   ; ⁻¹-involutive    to -‿involutive
   ; ⁻¹-injective     to -‿injective
   ; ⁻¹-anti-homo-∙   to -‿anti-homo-+
@@ -36,6 +34,11 @@ open AbelianGroupProperties +-abelianGroup public
   ; ⁻¹-∙-comm        to -‿+-comm
   )
 
+------------------------------------------------------------------------
+-- Re-export semiring without one properties
+
+open SemiringWithoutOneProperties semiringWithoutOne public
+
 x+x≈x⇒x≈0 : ∀ x → x + x ≈ x → x ≈ 0#
 x+x≈x⇒x≈0 x eq = +-identityˡ-unique x x eq
 
diff --git a/src/Algebra/Properties/Semiring.agda b/src/Algebra/Properties/Semiring.agda
index 1db1076689..a4b3522b01 100644
--- a/src/Algebra/Properties/Semiring.agda
+++ b/src/Algebra/Properties/Semiring.agda
@@ -13,13 +13,24 @@ module Algebra.Properties.Semiring
   {c ℓ} (semiring : Semiring c ℓ) where
 
 open Semiring semiring
-import Algebra.Consequences.Setoid setoid as Consequences
-open import Relation.Binary.Reasoning.Setoid setoid
 
-------------------------------------------------------------------------
--- Re-export binomial expansion
+open import Algebra.Properties.SemiringWithoutOne semiringWithoutOne public
+open import Algebra.Properties.Monoid *-monoid public
+  using ()
+  renaming
+    ( ε-unique to 1#-unique
+    ; ε-comm to 1#-comm
 
-binomial-expansion : ∀ w x y z →
-                     (w + x) * (y + z) ≈ w * y + w * z + x * y + x * z
-binomial-expansion = Consequences.binomial-expansion +-cong +-assoc distrib
+    ; elimʳ to *-elimʳ
+    ; elimˡ to *-elimˡ
+    ; introʳ to *-introʳ
+    ; introˡ to *-introˡ
+    ; introᶜ to *-introᶜ
 
+    ; cancelʳ to *-cancelʳ
+    ; cancelˡ to *-cancelˡ
+    ; insertˡ to *-insertˡ
+    ; insertʳ to *-insertʳ
+    ; cancelᶜ to *-cancelᶜ
+    ; insertᶜ to *-insertᶜ
+    )
diff --git a/src/Algebra/Properties/SemiringWithoutOne.agda b/src/Algebra/Properties/SemiringWithoutOne.agda
new file mode 100644
index 0000000000..1b4f2810c7
--- /dev/null
+++ b/src/Algebra/Properties/SemiringWithoutOne.agda
@@ -0,0 +1,128 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some basic properties of Semirings without a multiplicative identity
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (SemiringWithoutOne)
+
+module Algebra.Properties.SemiringWithoutOne {c ℓ} (semiring : SemiringWithoutOne c ℓ) where
+
+open SemiringWithoutOne semiring
+
+import Algebra.Consequences.Setoid setoid as Consequences
+open import Algebra.Properties.CommutativeMonoid (+-commutativeMonoid) public
+  using ()
+  renaming
+    ( x∙yz≈xy∙z to x+[y+z]≈[x+y]+z
+    ; alternativeˡ to +-alternativeˡ
+    ; alternativeʳ to +-alternativeʳ
+    ; alternative to +-alternative
+    ; flexible to +-flexible
+
+    ; uv≈w⇒xu∙v≈xw to u+v≈w⇒[x+u]+v≈x+w
+    ; uv≈w⇒u∙vx≈wx to u+v≈w⇒u+[v+x]≈w+x
+    ; uv≈w⇒u[vx∙y]≈w∙xy to u+v≈w⇒u+[[v+x]+y]≈w+[x+y]
+    ; uv≈w⇒[x∙yu]v≈x∙yw to u+v≈w⇒[x+[y+u]]+v≈x+[y+w]
+    ; uv≈w⇒[xu∙v]y≈x∙wy to u+v≈w⇒[[x+u]+v]+y≈x+[w+y]
+    ; uv≈w⇒[xy∙u]v≈x∙yw to u+v≈w⇒[[x+y]+u]+v≈x+[y+w]
+
+    ; uv≈w⇒xu∙vy≈x∙wy to u+v≈w⇒[x+u]+[v+y]≈x+[w+y]
+    ; uv≈w⇒xy≈z⇒u[vx∙y]≈wz to u+v≈w⇒x+y≈z⇒u+[[v+x]+y]≈w+z
+    ; uv≈w⇒x∙wy≈x∙[u∙vy] to u+v≈w⇒x+[w+y]≈x+[u+[v+y]]
+
+    ; [uv∙w]x≈u[vw∙x] to [[u+v]+w]+x≈u+[[v+w]+x]
+    ; [uv∙w]x≈u[v∙wx] to [[u+v]+w]+x≈u+[v+[w+z]]
+    ; [u∙vw]x≈uv∙wx to [u+[v+w]]+x≈[u+v]+[w+x]
+    ; [u∙vw]x≈u[v∙wx] to [u+[v+w]]+x≈u+[v+[w+x]]
+    ; uv∙wx≈u[vw∙x] to [u+v]+[w+x]≈u+[[v+w]+x]
+
+    ; uv≈wx⇒yu∙v≈yw∙x to u+v≈w+x⇒[y+u]+v≈[y+w]+x
+    ; uv≈wx⇒u∙vy≈w∙xy to u+v≈w+x⇒u+[v+y]≈w+[x+y]
+    ; uv≈wx⇒yu∙vz≈yw∙xz to u+v≈w+x⇒[y+u]+[v+z]≈[y+w]+[x+z]
+
+    ; medial to +-medial
+
+    ; x∙yz≈y∙xz to x+[y+z]≈y+[x+z]
+    ; x∙yz≈z∙yx to x+[y+z]≈z+[y+x]
+    ; x∙yz≈x∙zy to x+[y+z]≈x+[z+y]
+    ; x∙yz≈y∙zx to x+[y+z]≈y+[z+x]
+    ; x∙yz≈z∙xy to x+[y+z]≈z+[x+y]
+
+    ; x∙yz≈yx∙z to x+[y+z]≈[y+x]+z
+    ; x∙yz≈zy∙x to x+[y+z]≈[z+y]+x
+    ; x∙yz≈xz∙y to x+[y+z]≈[x+z]+y
+    ; x∙yz≈yz∙x to x+[y+z]≈[y+z]+x
+    ; x∙yz≈zx∙y to x+[y+z]≈[z+x]+y
+
+    ; xy∙z≈y∙xz to [x+y]+z≈y+[x+z]
+    ; xy∙z≈z∙yx to [x+y]+z≈z+[y+x]
+    ; xy∙z≈x∙zy to [x+y]+z≈x+[z+y]
+    ; xy∙z≈y∙zx to [x+y]+z≈y+[z+x]
+    ; xy∙z≈z∙xy to [x+y]+z≈z∙[x+y]
+
+    ; xy∙z≈yx∙z to [x+y]+z≈[y+x]+z
+    ; xy∙z≈zy∙x to [x+y]+z≈[z+y]+x
+    ; xy∙z≈xz∙y to [x+y]+z≈[x+z]+y
+    ; xy∙z≈yz∙x to [x+y]+z≈[y+z]+x
+    ; xy∙z≈zx∙y to [x+y]+z≈[z+x]+y
+
+    ; xy∙xx≈x∙yxx to [x+y]+[x+x]≈x+[y+x+x]
+
+    ; semimedialˡ to +-semimedialˡ
+    ; semimedialʳ to +-semimedialʳ
+    ; middleSemimedial to +-middleSemimedial
+    ; semimedial to +-semimedial
+
+    ; ε-unique to 0#-unique
+    
+    ; elimʳ to +-elimʳ
+    ; elimˡ to +-elimˡ
+    ; introʳ to +-introʳ
+    ; introˡ to +-introˡ
+    ; introᶜ to +-introᶜ
+
+    ; cancelʳ to +-cancelʳ
+    ; cancelˡ to +-cancelˡ
+    ; insertˡ to +-insertˡ
+    ; insertʳ to +-insertʳ
+    ; cancelᶜ to +-cancelᶜ
+    ; insertᶜ to +-insertᶜ
+    )
+
+open import Algebra.Properties.Semigroup (*-semigroup)
+  using ()
+  renaming
+    ( x∙yz≈xy∙z to x*yz≈xy*z
+    ; alternativeˡ to *-alternativeˡ
+    ; alternativeʳ to *-alternativeʳ
+    ; alternative to *-alternative
+    ; flexible to *-flexible
+
+    ; uv≈w⇒xu∙v≈xw to uv≈w⇒xu*v≈xw
+    ; uv≈w⇒u∙vx≈wx to uv≈w⇒u*vx≈wx
+    ; uv≈w⇒u[vx∙y]≈w∙xy to uv≈w⇒u[vx*y]≈w*xy
+    ; uv≈w⇒[x∙yu]v≈x∙yw to uv≈w⇒[x*yu]v≈x*yw
+    ; uv≈w⇒[xu∙v]y≈x∙wy to uv≈w⇒[xu*v]y≈x*wy
+    ; uv≈w⇒[xy∙u]v≈x∙yw to uv≈w⇒[xy*u]v≈x*yw
+
+    ; uv≈w⇒xu∙vy≈x∙wy to uv≈w⇒xu*vy≈x*wy
+    ; uv≈w⇒xy≈z⇒u[vx∙y]≈wz to uv≈w⇒xy≈z⇒u[vx*y]≈wz
+    ; uv≈w⇒x∙wy≈x∙[u∙vy] to uv≈w⇒x*wy≈x[u*vy]
+
+    ; [uv∙w]x≈u[vw∙x] to [uv*w]x≈u[vw*x]
+    ; [uv∙w]x≈u[v∙wx] to [uv*w]x≈u[v*wz]
+    ; [u∙vw]x≈uv∙wx to [u*vw]x≈uv*wx
+    ; [u∙vw]x≈u[v∙wx] to [u*vw]x≈u[v*wx]
+    ; uv∙wx≈u[vw∙x] to uv*wx≈u[vw*x]
+
+    ; uv≈wx⇒yu∙v≈yw∙x to uv≈wx⇒yu*v≈yw*x
+    ; uv≈wx⇒u∙vy≈w∙xy to uv≈wx⇒u*vy≈w*xy
+    ; uv≈wx⇒yu∙vz≈yw∙xz to uv≈wx⇒yu*vz≈yw*xz
+    )
+
+binomial-expansion : ∀ w x y z →
+                     (w + x) * (y + z) ≈ w * y + w * z + x * y + x * z
+binomial-expansion = Consequences.binomial-expansion +-cong +-assoc distrib
diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index e2a2257f6c..abecd0dbb4 100644
--- a/src/Algebra/Structures.agda
+++ b/src/Algebra/Structures.agda
@@ -825,17 +825,17 @@ record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ
   zero : Zero 0# *
   zero = zeroˡ , zeroʳ
 
-  isNearSemiring : IsNearSemiring + * 0#
-  isNearSemiring = record
-    { +-isMonoid = +-isMonoid
+  isSemiringWithoutOne : IsSemiringWithoutOne + * 0#
+  isSemiringWithoutOne = record
+    { +-isCommutativeMonoid = +-isCommutativeMonoid
     ; *-cong = *-cong
     ; *-assoc = *-assoc
-    ; distribʳ = distribʳ
-    ; zeroˡ = zeroˡ
+    ; distrib = distrib
+    ; zero = zero
     }
 
-  open IsNearSemiring isNearSemiring public
-    using (*-isMagma; *-isSemigroup; *-congˡ; *-congʳ)
+  open IsSemiringWithoutOne isSemiringWithoutOne public
+    using (*-isMagma; *-isSemigroup; isNearSemiring; *-congˡ; *-congʳ)
 
 ------------------------------------------------------------------------
 -- Structures with 2 binary operations, 1 unary operation & 2 elements
@@ -975,10 +975,6 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
     ; zero = zero
     }
 
-  open IsSemiring isSemiring public
-    using (isSemiringWithoutOne)
-
-
 record IsCommutativeRing
          (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
   field