diff --git a/CHANGELOG.md b/CHANGELOG.md
index eb838bcbe1..b22e6948ab 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -281,6 +281,12 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Construct.Add.Negatives.CommutativeMonoid` and
+  `Algebra.Construct.Add.Negatives.Semiring` for the group completion of a
+  commutative monoid and the ring completion of a semiring,
+  respectively, including isomorphisms when the input is already an
+  abelian group or ring.
+
 * `Algebra.Properties.KleeneAlgebra` has been completely rewritten.
 
 * `Codata.Guarded.Stream.Relation.Unary.Linked` for a proof that each pair
diff --git a/src/Algebra/Construct/Add/Negatives/CommutativeMonoid.agda b/src/Algebra/Construct/Add/Negatives/CommutativeMonoid.agda
new file mode 100644
index 0000000000..9abf94144f
--- /dev/null
+++ b/src/Algebra/Construct/Add/Negatives/CommutativeMonoid.agda
@@ -0,0 +1,335 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Group completion of a commutative monoid, i.e. the Grothendieck group
+-- of the monoid.
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Algebra.Construct.Add.Negatives.CommutativeMonoid where
+
+open import Algebra.Bundles using (AbelianGroup; CommutativeMonoid)
+import Algebra.Construct.DirectProduct as DirectProduct
+import Algebra.Definitions as Definitions
+open import Algebra.Morphism.Bundles using (MonoidHomomorphism)
+open import Algebra.Morphism.Structures using
+  (IsGroupHomomorphism; IsGroupIsomorphism; IsMonoidHomomorphism)
+import Algebra.Properties.AbelianGroup as AbelianGroupProperties
+import Algebra.Properties.CommutativeSemigroup
+  as CommSemigroupProperties
+import Algebra.Properties.Monoid as MonoidProperties
+open import Algebra.Structures using (IsAbelianGroup)
+open import Data.Product.Base as Product
+  using (∃-syntax; _,_; -,_; <_,_>; proj₁; proj₂; uncurry)
+open import Function.Base using (const; id; _∘_; _∘₂_)
+import Function.Consequences.Setoid as Consequences
+open import Function.Definitions using (Bijective; Congruent)
+open import Level using (Level; _⊔_)
+open import Relation.Binary.Core using (Rel)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+open import Relation.Binary.Structures using (IsEquivalence)
+
+module _ {m ℓ : Level} (monoid : CommutativeMonoid m ℓ) where
+
+  private
+    module M = CommutativeMonoid monoid
+    module Mₚ = MonoidProperties M.monoid
+    open M using (commutativeSemigroup; rawMonoid; setoid)
+      renaming
+      ( Carrier   to Base         ; _≈_       to _≈ₘ_
+      ; _∙_       to _+ₘ_         ; ε         to 0ₘ
+      ; refl      to ≈ₘ-refl      ; sym       to ≈ₘ-sym
+      ; comm      to +ₘ-comm      ; ∙-cong    to +ₘ-cong
+      ; ∙-congˡ   to +ₘ-congˡ     ; ∙-congʳ   to +ₘ-congʳ
+      ; identityˡ to +ₘ-identityˡ ; identityʳ to +ₘ-identityʳ
+      )
+
+    module M² = CommutativeMonoid
+      (DirectProduct.commutativeMonoid monoid monoid)
+    open CommSemigroupProperties commutativeSemigroup using (medial)
+
+  open ≈-Reasoning setoid
+
+
+  ------------------------------------------------------------------------
+  -- Formal differences
+
+  open M² public using (Carrier) renaming (_∙_ to _+_; ε to 0#)
+
+  ------------------------------------------------------------------------
+  -- Equality
+
+  infix 4 _≈₀_ _≈_
+
+  -- The zero-slack balance relation. It need not be transitive unless
+  -- the original monoid is cancellative.
+  _≈₀_ : Rel Carrier ℓ
+  (a , b) ≈₀ (c , d) = a +ₘ d ≈ₘ c +ₘ b
+
+  -- The completion relation stabilizes _≈₀_ by a common left summand.
+  _≈_ : Rel Carrier (m ⊔ ℓ)
+  (a , b) ≈ (c , d) = ∃[ slack ]
+    slack +ₘ (a +ₘ d) ≈ₘ slack +ₘ (c +ₘ b)
+
+  open Definitions _≈_ using (Congruent₁; Congruent₂; LeftInverse)
+
+  private
+    rearrange : ∀ a b c d u v →
+                (u +ₘ v) +ₘ ((a +ₘ c) +ₘ (b +ₘ d)) ≈ₘ
+                (u +ₘ (a +ₘ b)) +ₘ (v +ₘ (c +ₘ d))
+    rearrange a b c d u v = begin
+      (u +ₘ v) +ₘ ((a +ₘ c) +ₘ (b +ₘ d))
+        ≈⟨ +ₘ-comm _ _ ⟩
+      ((a +ₘ c) +ₘ (b +ₘ d)) +ₘ (u +ₘ v)
+        ≈⟨ +ₘ-congʳ (medial a c b d) ⟩
+      ((a +ₘ b) +ₘ (c +ₘ d)) +ₘ (u +ₘ v)
+        ≈⟨ medial (a +ₘ b) (c +ₘ d) u v ⟩
+      ((a +ₘ b) +ₘ u) +ₘ ((c +ₘ d) +ₘ v)
+        ≈⟨ +ₘ-cong (+ₘ-comm _ _) (+ₘ-comm _ _) ⟩
+      (u +ₘ (a +ₘ b)) +ₘ (v +ₘ (c +ₘ d))  ∎
+
+    composeˡ : ∀ a b c d u v →
+               ((u +ₘ v) +ₘ (c +ₘ d)) +ₘ (a +ₘ b) ≈ₘ
+               (u +ₘ (a +ₘ d)) +ₘ (v +ₘ (c +ₘ b))
+    composeˡ a b c d u v = begin
+      ((u +ₘ v) +ₘ (c +ₘ d)) +ₘ (a +ₘ b)
+        ≈⟨ M.assoc (u +ₘ v) (c +ₘ d) (a +ₘ b) ⟩
+      (u +ₘ v) +ₘ ((c +ₘ d) +ₘ (a +ₘ b))
+        ≈⟨ +ₘ-congˡ (medial c d a b) ⟩
+      (u +ₘ v) +ₘ ((c +ₘ a) +ₘ (d +ₘ b))
+        ≈⟨ +ₘ-congˡ (+ₘ-congʳ (+ₘ-comm c a)) ⟩
+      (u +ₘ v) +ₘ ((a +ₘ c) +ₘ (d +ₘ b))
+        ≈⟨ rearrange a d c b u v ⟩
+      (u +ₘ (a +ₘ d)) +ₘ (v +ₘ (c +ₘ b))  ∎
+
+  ≈₀⇒≈ : ∀ {x y} → x ≈₀ y → x ≈ y
+  ≈₀⇒≈ eq = 0ₘ , +ₘ-congˡ eq
+
+  ≈-from-parts : ∀ {a b c d} → a ≈ₘ c → b ≈ₘ d → (a , b) ≈ (c , d)
+  ≈-from-parts x⁺≈y⁺ x⁻≈y⁻ = ≈₀⇒≈ (+ₘ-cong x⁺≈y⁺ (≈ₘ-sym x⁻≈y⁻))
+
+  private
+    pointwise⇒≈ : ∀ {x y} → M²._≈_ x y → x ≈ y
+    pointwise⇒≈ = uncurry ≈-from-parts
+
+  ≈-isEquivalence : IsEquivalence _≈_
+  ≈-isEquivalence = record
+    { refl  = pointwise⇒≈ M².refl
+    ; sym   = Product.map₂ ≈ₘ-sym
+    ; trans = λ { {a , b} {c , d} {e , f} →
+        Product.zip (λ u v → (u +ₘ v) +ₘ (c +ₘ d))
+        λ {u} {v} eq₁ eq₂ → begin
+          ((u +ₘ v) +ₘ (c +ₘ d)) +ₘ (a +ₘ f)
+            ≈⟨ composeˡ a f c d u v ⟩
+          (u +ₘ (a +ₘ d)) +ₘ (v +ₘ (c +ₘ f))
+            ≈⟨ +ₘ-cong eq₁ eq₂ ⟩
+          (u +ₘ (c +ₘ b)) +ₘ (v +ₘ (e +ₘ d))
+            ≈⟨ +ₘ-comm _ _ ⟩
+          (v +ₘ (e +ₘ d)) +ₘ (u +ₘ (c +ₘ b))
+            ≈⟨ composeˡ e b c d v u ⟨
+          ((v +ₘ u) +ₘ (c +ₘ d)) +ₘ (e +ₘ b)
+            ≈⟨ +ₘ-congʳ (+ₘ-congʳ (+ₘ-comm v u)) ⟩
+          ((u +ₘ v) +ₘ (c +ₘ d)) +ₘ (e +ₘ b)  ∎ }
+    }
+
+  private module ≈ = IsEquivalence ≈-isEquivalence
+
+  ------------------------------------------------------------------------
+  -- Operations
+
+  infix  8 -_
+
+  -_ : Carrier → Carrier
+  -_ = Product.swap
+
+  +-cong : Congruent₂ _+_
+  +-cong {a , b} {a′ , b′} {c , d} {c′ , d′} =
+    Product.zip _+ₘ_ λ {u} {v} eq₁ eq₂ → begin
+      (u +ₘ v) +ₘ ((a +ₘ c) +ₘ (b′ +ₘ d′))  ≈⟨ rearrange a b′ c d′ u v ⟩
+      (u +ₘ (a +ₘ b′)) +ₘ (v +ₘ (c +ₘ d′))  ≈⟨ +ₘ-cong eq₁ eq₂ ⟩
+      (u +ₘ (a′ +ₘ b)) +ₘ (v +ₘ (c′ +ₘ d))  ≈⟨ rearrange a′ b c′ d u v ⟨
+      (u +ₘ v) +ₘ ((a′ +ₘ c′) +ₘ (b +ₘ d))  ∎
+
+  -‿cong : Congruent₁ -_
+  -‿cong {a , b} {c , d} = Product.map₂ λ {u} eq → begin
+    u +ₘ (b +ₘ c)  ≈⟨ +ₘ-congˡ (+ₘ-comm b c) ⟩
+    u +ₘ (c +ₘ b)  ≈⟨ eq ⟨
+    u +ₘ (a +ₘ d)  ≈⟨ +ₘ-congˡ (+ₘ-comm a d) ⟩
+    u +ₘ (d +ₘ a)  ∎
+
+  +-inverseˡ : LeftInverse 0# -_ _+_
+  +-inverseˡ (a , b) = -, (begin
+    0ₘ +ₘ ((b +ₘ a) +ₘ 0ₘ)  ≈⟨ +ₘ-identityˡ _ ⟩
+    (b +ₘ a) +ₘ 0ₘ          ≈⟨ +ₘ-identityʳ _ ⟩
+    b +ₘ a                  ≈⟨ +ₘ-comm b a ⟩
+    a +ₘ b                  ≈⟨ +ₘ-identityˡ _ ⟨
+    0ₘ +ₘ (a +ₘ b)          ≈⟨ +ₘ-congˡ (+ₘ-identityˡ _) ⟨
+    0ₘ +ₘ (0ₘ +ₘ (a +ₘ b))  ∎)
+
+  ------------------------------------------------------------------------
+  -- Bundle
+
+  completion-is-abelian-group : IsAbelianGroup _≈_ _+_ 0# -_
+  completion-is-abelian-group = record
+    { isGroup = record
+      { isMonoid = record
+        { isSemigroup = record
+          { isMagma = record
+            { isEquivalence = ≈-isEquivalence
+            ; ∙-cong = +-cong
+            }
+          ; assoc = λ x → pointwise⇒≈ ∘₂ M².assoc x
+          }
+        ; identity = Product.map
+            (pointwise⇒≈ ∘_) (pointwise⇒≈ ∘_) M².identity
+        }
+      ; inverse = +-inverseˡ , +-inverseˡ ∘ -_
+      ; ⁻¹-cong = -‿cong
+      }
+    ; comm = pointwise⇒≈ ∘₂ M².comm
+    }
+
+  abelianGroup : AbelianGroup m (m ⊔ ℓ)
+  abelianGroup = record { isAbelianGroup = completion-is-abelian-group }
+
+  open AbelianGroup abelianGroup
+    using () renaming (rawMonoid to rawMonoid#)
+
+  ------------------------------------------------------------------------
+  -- Canonical embedding
+
+  embed : Base → Carrier
+  embed = < id , const 0ₘ >
+
+  embed-cong : Congruent _≈ₘ_ _≈_ embed
+  embed-cong x≈y = ≈-from-parts x≈y ≈ₘ-refl
+
+  embed-∙ : ∀ x y → embed (x +ₘ y) ≈ embed x + embed y
+  embed-∙ x y = ≈-from-parts ≈ₘ-refl (Mₚ.introˡ ≈ₘ-refl 0ₘ)
+
+  embed-isMonoidHomomorphism :
+    IsMonoidHomomorphism rawMonoid rawMonoid# embed
+  embed-isMonoidHomomorphism = record
+    { isMagmaHomomorphism = record
+      { isRelHomomorphism = record { cong = embed-cong }
+      ; ∙-homo            = embed-∙
+      }
+    ; ε-homo = ≈.refl
+    }
+
+  embed-monoidHomomorphism :
+    MonoidHomomorphism rawMonoid rawMonoid#
+  embed-monoidHomomorphism = record
+    { isMonoidHomomorphism = embed-isMonoidHomomorphism }
+
+  decompose : ∀ x → x ≈ embed (proj₁ x) + - embed (proj₂ x)
+  decompose (a , b) =
+    ≈-from-parts (Mₚ.introʳ ≈ₘ-refl a)
+                 (Mₚ.introˡ ≈ₘ-refl b)
+
+
+  ------------------------------------------------------------------------
+  -- Trivial completions
+
+  open Definitions _≈ₘ_ using () renaming (LeftZero to LeftAbsorbing)
+
+  absorbing⇒trivial : (∞ : Base) → LeftAbsorbing ∞ _+ₘ_ →
+                      ∀ x → x ≈ 0#
+  absorbing⇒trivial ∞ absorbˡ (a , b) = -, (begin
+    ∞ +ₘ (a +ₘ 0ₘ)  ≈⟨ absorbˡ (a +ₘ 0ₘ) ⟩
+    ∞               ≈⟨ absorbˡ (0ₘ +ₘ b) ⟨
+    ∞ +ₘ (0ₘ +ₘ b)  ∎)
+
+
+------------------------------------------------------------------------
+-- Completion of an abelian group
+
+module AlreadyGroup {m ℓ : Level} (G : AbelianGroup m ℓ) where
+
+  private
+    module G = AbelianGroup G
+    module Gₚ = AbelianGroupProperties G
+    module Gₘ = MonoidProperties G.monoid
+    open CommSemigroupProperties G.commutativeSemigroup using (medial)
+    open Gₘ using (cancelᶜ; elimʳ; introʳ)
+    open Gₚ using
+      (∙-cancelˡ; ∙-cancelʳ; ε⁻¹≈ε; ⁻¹-anti-homo‿-; ⁻¹-∙-comm)
+
+    module C = AbelianGroup (abelianGroup G.commutativeMonoid)
+    open Consequences C.setoid G.setoid using
+      (inverseᵇ⇒bijective; strictlyInverseˡ⇒inverseˡ
+      ; strictlyInverseʳ⇒inverseʳ)
+
+    open ≈-Reasoning G.setoid
+
+  self-completion-to-self : C.Carrier → G.Carrier
+  self-completion-to-self = Product.uncurry G._-_
+
+  to-self-cong : Congruent C._≈_ G._≈_ self-completion-to-self
+  to-self-cong {a , b} {c , d} = Product.uncurry λ slack eq →
+    ∙-cancelʳ (b G.∙ d) _ _ (begin
+      (a G.- b) G.∙ (b G.∙ d)   ≈⟨ cancelᶜ (G.inverseˡ b) a d ⟩
+      a G.∙ d                   ≈⟨ ∙-cancelˡ slack _ _ eq ⟩
+      c G.∙ b                   ≈⟨ cancelᶜ (G.inverseˡ d) c b ⟨
+      (c G.- d) G.∙ (d G.∙ b)   ≈⟨ G.∙-congˡ (G.comm b d) ⟨
+      (c G.- d) G.∙ (b G.∙ d)   ∎)
+
+  to-self-∙ : ∀ x y →
+              self-completion-to-self (C._∙_ x y) G.≈
+              self-completion-to-self x G.∙ self-completion-to-self y
+  to-self-∙ (a , b) (c , d) = begin
+    (a G.∙ c) G.- (b G.∙ d)           ≡⟨⟩
+    (a G.∙ c) G.∙ (b G.∙ d) G.⁻¹      ≈⟨ G.∙-congˡ (⁻¹-∙-comm _ _) ⟨
+    (a G.∙ c) G.∙ (b G.⁻¹ G.∙ d G.⁻¹) ≈⟨ medial a c (b G.⁻¹) (d G.⁻¹) ⟩
+    (a G.∙ b G.⁻¹) G.∙ (c G.∙ d G.⁻¹) ≡⟨⟩
+    (a G.- b) G.∙ (c G.- d)           ∎
+
+  to-self-embed : ∀ x →
+    self-completion-to-self (embed G.commutativeMonoid x) G.≈ x
+  to-self-embed x = elimʳ ε⁻¹≈ε x
+
+  to-self-⁻¹ : ∀ x →
+               self-completion-to-self (C._⁻¹ x) G.≈
+               self-completion-to-self x G.⁻¹
+  to-self-⁻¹ (a , b) = G.sym (⁻¹-anti-homo‿- a b)
+
+  to-self-isGroupHomomorphism :
+    IsGroupHomomorphism C.rawGroup G.rawGroup self-completion-to-self
+  to-self-isGroupHomomorphism = record
+    { isMonoidHomomorphism = record
+      { isMagmaHomomorphism = record
+        { isRelHomomorphism = record { cong = to-self-cong }
+        ; ∙-homo            = to-self-∙
+        }
+      ; ε-homo = to-self-embed G.ε
+      }
+    ; ⁻¹-homo = to-self-⁻¹
+    }
+
+  embed-to-self : ∀ x →
+    embed G.commutativeMonoid (self-completion-to-self x) C.≈ x
+  embed-to-self (a , b) = -, (begin
+    G.ε G.∙ ((a G.- b) G.∙ b)   ≈⟨ G.identityˡ _ ⟩
+    (a G.- b) G.∙ b             ≈⟨ Gₘ.cancelʳ (G.inverseˡ b) a ⟩
+    a                           ≈⟨ introʳ G.refl _ ⟩
+    a G.∙ G.ε                   ≈⟨ G.identityˡ _ ⟨
+    G.ε G.∙ (a G.∙ G.ε)         ∎)
+
+  to-self-bijective :
+    Bijective C._≈_ G._≈_ self-completion-to-self
+  to-self-bijective = inverseᵇ⇒bijective
+    ( strictlyInverseˡ⇒inverseˡ to-self-cong to-self-embed
+    , strictlyInverseʳ⇒inverseʳ (embed-cong G.commutativeMonoid)
+        embed-to-self
+    )
+
+  self-completion-≅ :
+    IsGroupIsomorphism C.rawGroup G.rawGroup self-completion-to-self
+  self-completion-≅ = record
+    { isGroupMonomorphism = record
+      { isGroupHomomorphism = to-self-isGroupHomomorphism
+      ; injective           = proj₁ to-self-bijective
+      }
+    ; surjective = proj₂ to-self-bijective
+    }
diff --git a/src/Algebra/Construct/Add/Negatives/Semiring.agda b/src/Algebra/Construct/Add/Negatives/Semiring.agda
new file mode 100644
index 0000000000..cfb3e512b9
--- /dev/null
+++ b/src/Algebra/Construct/Add/Negatives/Semiring.agda
@@ -0,0 +1,350 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Ring completion of a semiring, freely adjoining negatives
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Algebra.Construct.Add.Negatives.Semiring where
+
+open import Algebra.Bundles
+  using (AbelianGroup; CommutativeRing; Ring; Semiring)
+import Algebra.Construct.Add.Negatives.CommutativeMonoid as Negatives
+import Algebra.Definitions as Definitions
+open import Algebra.Morphism.Bundles using (SemiringHomomorphism)
+open import Algebra.Morphism.Structures using
+  (IsGroupIsomorphism; IsRingHomomorphism; IsRingIsomorphism
+  ; IsSemiringHomomorphism)
+import Algebra.Properties.CommutativeSemigroup as CSProperties
+import Algebra.Properties.Monoid as MonoidProperties
+import Algebra.Properties.Ring as RingProperties
+open import Algebra.Structures using (IsRing)
+open import Data.Product.Base as Product using (_,_; proj₁; proj₂)
+open import Function.Definitions using (Congruent)
+open import Level using (Level; _⊔_)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+module _ {m ℓ : Level} (semiring : Semiring m ℓ) where
+
+  private
+    module S = Semiring semiring
+    module Sₘ = MonoidProperties S.+-monoid
+    open CSProperties S.+-commutativeSemigroup using (medial)
+
+    open S using () renaming
+      ( Carrier to Base
+      ; _+_     to _+ₛ_ ; _*_ to _*ₛ_ ; _≈_ to _≈ₛ_
+      ; 0#      to 0ₛ   ; 1#  to 1ₛ
+      )
+
+  ----------------------------------------------------------------------
+  -- Additive completion
+
+  private
+    -- Ring completion reuses the commutative-monoid completion verbatim
+    -- for its additive structure and only extends multiplication below.
+    module Additive = AbelianGroup
+      (Negatives.abelianGroup S.+-commutativeMonoid)
+
+  open Additive public using (Carrier)
+    renaming (_≈_ to _≈_; _∙_ to _+_; ε to 0#; _⁻¹ to -_)
+  open Additive using () renaming
+    (∙-cong to +-cong; ⁻¹-cong to -‿cong)
+
+  private
+    pos neg : Carrier → Base
+    pos = proj₁
+    neg = proj₂
+
+    ≈-from-parts : ∀ {x y} →
+                   pos x S.≈ pos y → neg x S.≈ neg y → x ≈ y
+    ≈-from-parts = Negatives.≈-from-parts S.+-commutativeMonoid
+
+    variable
+      x y z : Carrier
+      a : Base
+
+  open Definitions _≈_ using (Congruent₂)
+
+  ----------------------------------------------------------------------
+  -- Multiplication
+
+  infixl 7 _*_
+
+  private
+    prod⁺ : Carrier → Carrier → Base
+    prod⁺ (a , b) (c , d) = a *ₛ c +ₛ b *ₛ d
+
+  _*_ : Carrier → Carrier → Carrier
+  x * y = prod⁺ x y , prod⁺ x (- y)
+
+  1# : Carrier
+  1# = 1ₛ , 0ₛ
+
+  private
+    scaleˡ : Base → Carrier → Carrier
+    scaleˡ a = Product.map (a *ₛ_) (a *ₛ_)
+
+    scaleʳ : Carrier → Base → Carrier
+    scaleʳ x a = Product.map (_*ₛ a) (_*ₛ a) x
+
+    -- Mapping a completion equality changes its witness from `slack` to
+    -- `f slack`, so the witness must be exposed here.
+    map-cong : ∀ f → Congruent _≈ₛ_ _≈ₛ_ f →
+      (∀ a b → f (a +ₛ b) ≈ₛ f a +ₛ f b) →
+      Congruent _≈_ _≈_ (Product.map f f)
+    map-cong f cong homo = Product.map f λ {slack} eq → begin
+      f slack +ₛ (f _ +ₛ f _)  ≈⟨ S.+-congˡ (homo _ _) ⟨
+      f slack +ₛ f (_ +ₛ _)    ≈⟨ homo slack (_ +ₛ _) ⟨
+      f (slack +ₛ (_ +ₛ _))    ≈⟨ cong eq ⟩
+      f (slack +ₛ (_ +ₛ _))    ≈⟨ homo slack (_ +ₛ _) ⟩
+      f slack +ₛ f (_ +ₛ _)    ≈⟨ S.+-congˡ (homo _ _) ⟩
+      f slack +ₛ (f _ +ₛ f _)  ∎
+      where open ≈-Reasoning S.setoid
+
+    scale-congˡ : Congruent _≈_ _≈_ (scaleˡ a)
+    scale-congˡ {a} = map-cong (a *ₛ_) S.*-congˡ (S.distribˡ a)
+
+    scale-congʳ : Congruent _≈_ _≈_ (λ x → scaleʳ x a)
+    scale-congʳ {a} = map-cong (_*ₛ a) S.*-congʳ (S.distribʳ a)
+
+    *-as-scalesʳ : x * y ≈ scaleʳ x (pos y) + - scaleʳ x (neg y)
+    *-as-scalesʳ {(a , b)} {(c , d)} =
+      ≈-from-parts S.refl (S.+-comm (a *ₛ d) (b *ₛ c))
+
+    *-cong : Congruent₂ _*_
+    *-cong {a , b} {a′ , b′} {y} {y′} x≈x′ y≈y′ = begin
+      (a , b) * y
+        ≈⟨ *-as-scalesʳ ⟩
+      scaleʳ (a , b) (pos y) + - scaleʳ (a , b) (neg y)
+        ≈⟨ +-cong (scale-congʳ x≈x′) (-‿cong (scale-congʳ x≈x′)) ⟩
+      scaleʳ (a′ , b′) (pos y) + - scaleʳ (a′ , b′) (neg y)
+        ≈⟨ *-as-scalesʳ ⟨
+      (a′ , b′) * y
+        ≈⟨ +-cong (scale-congˡ y≈y′) (-‿cong (scale-congˡ y≈y′)) ⟩
+      (a′ , b′) * y′  ∎
+      where open ≈-Reasoning Additive.setoid
+
+  open ≈-Reasoning S.setoid
+
+  ----------------------------------------------------------------------
+  -- Ring laws
+
+  private
+    distrib⁺ˡ : ∀ x y z →
+      prod⁺ x (y + z) ≈ₛ prod⁺ x y +ₛ prod⁺ x z
+    distrib⁺ˡ (x⁺ , x⁻) (y⁺ , y⁻) (z⁺ , z⁻) = begin
+      x⁺ *ₛ (y⁺ +ₛ z⁺) +ₛ x⁻ *ₛ (y⁻ +ₛ z⁻)
+        ≈⟨ S.+-cong (S.distribˡ _ _ _) (S.distribˡ _ _ _) ⟩
+      (x⁺ *ₛ y⁺ +ₛ x⁺ *ₛ z⁺) +ₛ (x⁻ *ₛ y⁻ +ₛ x⁻ *ₛ z⁻)
+        ≈⟨ medial _ _ _ _ ⟩
+      (x⁺ *ₛ y⁺ +ₛ x⁻ *ₛ y⁻) +ₛ (x⁺ *ₛ z⁺ +ₛ x⁻ *ₛ z⁻)  ∎
+
+    distrib⁺ʳ : ∀ x y z →
+      prod⁺ (x + y) z ≈ₛ prod⁺ x z +ₛ prod⁺ y z
+    distrib⁺ʳ (x⁺ , x⁻) (y⁺ , y⁻) (z⁺ , z⁻) = begin
+      (x⁺ +ₛ y⁺) *ₛ z⁺ +ₛ (x⁻ +ₛ y⁻) *ₛ z⁻
+        ≈⟨ S.+-cong (S.distribʳ _ _ _) (S.distribʳ _ _ _) ⟩
+      (x⁺ *ₛ z⁺ +ₛ y⁺ *ₛ z⁺) +ₛ (x⁻ *ₛ z⁻ +ₛ y⁻ *ₛ z⁻)
+        ≈⟨ medial _ _ _ _ ⟩
+      (x⁺ *ₛ z⁺ +ₛ x⁻ *ₛ z⁻) +ₛ (y⁺ *ₛ z⁺ +ₛ y⁻ *ₛ z⁻)  ∎
+
+    scale-prod : ∀ a x y →
+      prod⁺ (scaleˡ a x) y ≈ₛ a *ₛ prod⁺ x y
+    scale-prod a (b , c) (d , e) = begin
+      (a *ₛ b) *ₛ d +ₛ (a *ₛ c) *ₛ e
+        ≈⟨ S.+-cong (S.*-assoc _ _ _) (S.*-assoc _ _ _) ⟩
+      a *ₛ (b *ₛ d) +ₛ a *ₛ (c *ₛ e)
+        ≈⟨ S.distribˡ _ _ _ ⟨
+      a *ₛ (b *ₛ d +ₛ c *ₛ e)  ∎
+
+    neg-scale-prod : ∀ a x y →
+      prod⁺ (- scaleˡ a x) y ≈ₛ a *ₛ prod⁺ x (- y)
+    neg-scale-prod a (b , c) (d , e) = begin
+      (a *ₛ c) *ₛ d +ₛ (a *ₛ b) *ₛ e  ≈⟨ scale-prod a (c , b) (d , e) ⟩
+      a *ₛ (c *ₛ d +ₛ b *ₛ e)         ≈⟨ S.*-congˡ (S.+-comm _ _) ⟩
+      a *ₛ (b *ₛ e +ₛ c *ₛ d)         ∎
+
+    assoc⁺ : ∀ x y z → prod⁺ (x * y) z ≈ₛ prod⁺ x (y * z)
+    assoc⁺ (a , b) y z = begin
+      prod⁺ ((a , b) * y) z
+        ≡⟨⟩
+      prod⁺ (scaleˡ a y + - scaleˡ b y) z
+        ≈⟨ distrib⁺ʳ (scaleˡ a y) (- scaleˡ b y) z ⟩
+      prod⁺ (scaleˡ a y) z +ₛ prod⁺ (- scaleˡ b y) z
+        ≈⟨ S.+-cong (scale-prod a y z) (neg-scale-prod b y z) ⟩
+      a *ₛ prod⁺ y z +ₛ b *ₛ prod⁺ y (- z)
+        ≡⟨⟩
+      prod⁺ (a , b) (y * z)  ∎
+
+  ----------------------------------------------------------------------
+  -- Bundle
+
+  completion-is-ring : IsRing _≈_ _+_ _*_ -_ 0# 1#
+  completion-is-ring = record
+    { +-isAbelianGroup = Additive.isAbelianGroup
+    ; *-cong           = *-cong
+    ; *-assoc          = λ x y z → ≈-from-parts
+        (assoc⁺ x y z) (assoc⁺ x y (- z))
+    ; *-identity       =
+        ( (λ { (x⁺ , x⁻) → ≈-from-parts
+            (begin
+              1ₛ *ₛ x⁺ +ₛ 0ₛ *ₛ x⁻  ≈⟨ S.+-congʳ (S.*-identityˡ _) ⟩
+              x⁺ +ₛ 0ₛ *ₛ x⁻        ≈⟨ Sₘ.elimʳ (S.zeroˡ _) x⁺ ⟩
+              x⁺                    ∎)
+            (begin
+              1ₛ *ₛ x⁻ +ₛ 0ₛ *ₛ x⁺  ≈⟨ S.+-congʳ (S.*-identityˡ _) ⟩
+              x⁻ +ₛ 0ₛ *ₛ x⁺        ≈⟨ Sₘ.elimʳ (S.zeroˡ _) x⁻ ⟩
+              x⁻                    ∎) })
+        , (λ { (x⁺ , x⁻) → ≈-from-parts
+            (begin
+              x⁺ *ₛ 1ₛ +ₛ x⁻ *ₛ 0ₛ  ≈⟨ S.+-congʳ (S.*-identityʳ _) ⟩
+              x⁺ +ₛ x⁻ *ₛ 0ₛ        ≈⟨ Sₘ.elimʳ (S.zeroʳ _) x⁺ ⟩
+              x⁺                    ∎)
+            (begin
+              x⁺ *ₛ 0ₛ +ₛ x⁻ *ₛ 1ₛ  ≈⟨ S.+-congˡ (S.*-identityʳ _) ⟩
+              x⁺ *ₛ 0ₛ +ₛ x⁻        ≈⟨ Sₘ.elimˡ (S.zeroʳ _) x⁻ ⟩
+              x⁻                    ∎) })
+        )
+    ; distrib          =
+        ( (λ x y z → ≈-from-parts
+            (distrib⁺ˡ x y z) (distrib⁺ˡ x (- y) (- z)))
+        , (λ x y z → ≈-from-parts
+            (distrib⁺ʳ y z x) (distrib⁺ʳ y z (- x)))
+        )
+    }
+
+  ring : Ring m (m ⊔ ℓ)
+  ring = record { isRing = completion-is-ring }
+
+  private module R = Semiring (Ring.semiring ring)
+  open Definitions (_≈ₛ_)
+    using (Commutative) renaming (LeftZero to LeftAbsorbing)
+
+  ------------------------------------------------------------------------
+  -- Commutative specialization
+
+  commutativeRing : Commutative S._*_ → CommutativeRing m (m ⊔ ℓ)
+  commutativeRing comm = record
+    { isCommutativeRing = record
+      { isRing = completion-is-ring
+      ; *-comm = λ { (a , b) (c , d) → ≈-from-parts
+          (S.+-cong (comm a c) (comm b d))
+          (begin
+            a *ₛ d +ₛ b *ₛ c  ≈⟨ S.+-cong (comm a d) (comm b c) ⟩
+            d *ₛ a +ₛ c *ₛ b  ≈⟨ S.+-comm _ _ ⟩
+            c *ₛ b +ₛ d *ₛ a  ∎) }
+      }
+    }
+
+
+  ----------------------------------------------------------------------
+  -- Canonical embedding
+
+  embed : Base → Carrier
+  embed = Negatives.embed S.+-commutativeMonoid
+
+  decompose : ∀ x → x ≈ embed (proj₁ x) + - embed (proj₂ x)
+  decompose = Negatives.decompose S.+-commutativeMonoid
+
+  embed-* : ∀ x y → embed (x *ₛ y) ≈ embed x * embed y
+  embed-* x y = ≈-from-parts
+    (Sₘ.introʳ (S.zeroˡ 0ₛ) (x *ₛ y))
+    (begin
+      0ₛ                      ≈⟨ S.zeroˡ y ⟨
+      0ₛ *ₛ y                 ≈⟨ Sₘ.introˡ (S.zeroʳ x) _ ⟩
+      (x *ₛ 0ₛ) +ₛ (0ₛ *ₛ y)  ∎)
+
+  embed-isSemiringHomomorphism :
+    IsSemiringHomomorphism S.rawSemiring R.rawSemiring embed
+  embed-isSemiringHomomorphism = record
+    { isNearSemiringHomomorphism = record
+      { +-isMonoidHomomorphism =
+          Negatives.embed-isMonoidHomomorphism
+            S.+-commutativeMonoid
+      ; *-homo                 = embed-*
+      }
+    ; 1#-homo = Additive.refl
+    }
+
+  embed-semiringHomomorphism :
+    SemiringHomomorphism S.rawSemiring R.rawSemiring
+  embed-semiringHomomorphism = record
+    { isSemiringHomomorphism = embed-isSemiringHomomorphism }
+
+
+  ----------------------------------------------------------------------
+  -- Trivial completions
+
+  +-absorbing⇒trivial : (∞ : Base) → LeftAbsorbing ∞ S._+_ →
+                        ∀ x → x ≈ 0#
+  +-absorbing⇒trivial =
+    Negatives.absorbing⇒trivial S.+-commutativeMonoid
+
+  +-absorbing⇒1#≈0# : (∞ : Base) → LeftAbsorbing ∞ S._+_ →
+                      1# ≈ 0#
+  +-absorbing⇒1#≈0# ∞ absorbˡ = +-absorbing⇒trivial ∞ absorbˡ 1#
+
+
+------------------------------------------------------------------------
+-- Completion of a ring
+
+module AlreadyRing {m ℓ : Level} (R : Ring m ℓ) where
+
+  private
+    module R = Ring R
+    module Rₚ = RingProperties R
+    open CSProperties R.+-commutativeSemigroup using (medial)
+    module Additive = Negatives.AlreadyGroup R.+-abelianGroup
+    module Additive≅ = IsGroupIsomorphism Additive.self-completion-≅
+
+    module C = Ring (ring R.semiring)
+
+    open ≈-Reasoning R.setoid
+
+  self-completion-to-self : C.Carrier → R.Carrier
+  self-completion-to-self = Product.uncurry R._-_
+
+  to-self-* : ∀ x y →
+              self-completion-to-self (C._*_ x y) R.≈
+              self-completion-to-self x R.* self-completion-to-self y
+  to-self-* (a , b) (c , d) = begin
+    (a R.* c R.+ b R.* d) R.- (a R.* d R.+ b R.* c)  ≡⟨⟩
+    (a R.* c R.+ b R.* d) R.+ R.-_ (a R.* d R.+ b R.* c)
+      ≈⟨ R.+-congˡ (Rₚ.-‿+-comm (a R.* d) (b R.* c)) ⟨
+    (a R.* c R.+ b R.* d) R.+
+      (R.-_ (a R.* d) R.+ R.-_ (b R.* c))
+      ≈⟨ medial (a R.* c) (b R.* d)
+               (R.-_ (a R.* d)) (R.-_ (b R.* c)) ⟩
+    (a R.* c R.- a R.* d) R.+ (b R.* d R.- b R.* c)
+      ≈⟨ R.+-congˡ (Rₚ.⁻¹-anti-homo‿- (b R.* c) (b R.* d)) ⟨
+    (a R.* c R.- a R.* d) R.- (b R.* c R.- b R.* d)
+      ≈⟨ R.+-cong (Rₚ.x[y-z]≈xy-xz a c d)
+                   (R.-‿cong (Rₚ.x[y-z]≈xy-xz b c d)) ⟨
+    a R.* (c R.- d) R.- b R.* (c R.- d)
+      ≈⟨ Rₚ.[y-z]x≈yx-zx (c R.- d) a b ⟨
+    (a R.- b) R.* (c R.- d)                           ∎
+
+  to-self-isRingHomomorphism :
+    IsRingHomomorphism C.rawRing R.rawRing self-completion-to-self
+  to-self-isRingHomomorphism = record
+    { isSemiringHomomorphism = record
+      { isNearSemiringHomomorphism = record
+        { +-isMonoidHomomorphism = Additive≅.isMonoidHomomorphism
+        ; *-homo                 = to-self-*
+        }
+      ; 1#-homo = Additive.to-self-embed R.1#
+      }
+    ; -‿homo = Additive≅.⁻¹-homo
+    }
+
+  self-completion-≅ :
+    IsRingIsomorphism C.rawRing R.rawRing self-completion-to-self
+  self-completion-≅ = record
+    { isRingMonomorphism = record
+      { isRingHomomorphism = to-self-isRingHomomorphism
+      ; injective          = Additive≅.injective
+      }
+    ; surjective = Additive≅.surjective
+    }