From e2ff677ed39cf9336abc5cd81bb32aaf039ff310 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 5 Nov 2025 14:10:20 +0000
Subject: [PATCH 01/15] refactor: alternative to #2852 and #2854

---
 CHANGELOG.md | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6679049fd0..3f3ad2178f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -79,6 +79,12 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Construct.Quotient.{Abelian}Group` for the definition of quotient (Abelian) groups.
+
+* `Algebra.Construct.Sub.{Abelian}Group` for the definition of sub-(Abelian)groups.
+
+* `Algebra.Construct.Sub.Group.Normal` for the definition of normal subgroups.
+
 * `Algebra.Properties.BooleanRing`.
 
 * `Algebra.Properties.BooleanSemiring`.

From f702f82769122220fa79d7a2ac43666db136b169 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 5 Nov 2025 14:12:53 +0000
Subject: [PATCH 02/15] refactor: alternative to #2852 and #2854

---
 .../Construct/Quotient/AbelianGroup.agda      |  35 +++++
 src/Algebra/Construct/Quotient/Group.agda     | 126 ++++++++++++++++++
 src/Algebra/Construct/Sub/AbelianGroup.agda   |  48 +++++++
 src/Algebra/Construct/Sub/Group.agda          |  31 +++++
 src/Algebra/Construct/Sub/Group/Normal.agda   |  32 +++++
 5 files changed, 272 insertions(+)
 create mode 100644 src/Algebra/Construct/Quotient/AbelianGroup.agda
 create mode 100644 src/Algebra/Construct/Quotient/Group.agda
 create mode 100644 src/Algebra/Construct/Sub/AbelianGroup.agda
 create mode 100644 src/Algebra/Construct/Sub/Group.agda
 create mode 100644 src/Algebra/Construct/Sub/Group/Normal.agda

diff --git a/src/Algebra/Construct/Quotient/AbelianGroup.agda b/src/Algebra/Construct/Quotient/AbelianGroup.agda
new file mode 100644
index 0000000000..46ccdf3c68
--- /dev/null
+++ b/src/Algebra/Construct/Quotient/AbelianGroup.agda
@@ -0,0 +1,35 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Quotient Abelian groups
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (Group; AbelianGroup)
+import Algebra.Construct.Sub.AbelianGroup as AbelianSubgroup
+
+module Algebra.Construct.Quotient.AbelianGroup
+  {c ℓ} (G : AbelianGroup c ℓ)
+  (open AbelianSubgroup G using (Subgroup; normalSubgroup)) 
+  {c′ ℓ′} (N : Subgroup c′ ℓ′)
+  where
+
+private
+  module G = AbelianGroup G
+
+-- Re-export the quotient group
+
+open import Algebra.Construct.Quotient.Group G.group (normalSubgroup N) public
+
+-- With its additional bundle
+
+quotientAbelianGroup : AbelianGroup c _
+quotientAbelianGroup = record
+  { isAbelianGroup = record
+    { isGroup = isGroup
+    ; comm = λ g h → ≈⇒≋ (G.comm g h)
+    }
+  } where open Group quotientGroup
+
+-- Public re-exports, as needed?
diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda
new file mode 100644
index 0000000000..99e22352cf
--- /dev/null
+++ b/src/Algebra/Construct/Quotient/Group.agda
@@ -0,0 +1,126 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Quotient groups
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (Group)
+open import Algebra.Construct.Sub.Group.Normal using (NormalSubgroup)
+
+module Algebra.Construct.Quotient.Group
+  {c ℓ} (G : Group c ℓ) {c′ ℓ′} (N : NormalSubgroup G c′ ℓ′) where
+
+open import Algebra.Definitions using (Congruent₁; Congruent₂)
+open import Algebra.Morphism.Structures
+  using (IsMagmaHomomorphism; IsMonoidHomomorphism; IsGroupHomomorphism)
+open import Data.Product.Base using (_,_)
+open import Function.Base using (_∘_)
+open import Function.Definitions using (Surjective)
+open import Level using (_⊔_)
+open import Relation.Binary.Core using (_⇒_)
+open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
+
+private
+  open module G = Group G
+
+open import Algebra.Properties.Group G using (⁻¹-anti-homo-∙)
+open import Algebra.Properties.Monoid monoid
+open import Relation.Binary.Reasoning.Setoid setoid
+
+private
+  open module N = NormalSubgroup N
+    using (ι; module ι; conjugate; normal)
+
+infix 0 _by_
+
+data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where
+  _by_ : ∀ g → ι g ∙ x ≈ y → x ≋ y
+
+≈⇒≋ : _≈_ ⇒ _≋_
+≈⇒≋ x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ _)
+
+≋-refl : Reflexive _≋_
+≋-refl = ≈⇒≋ refl
+
+≋-sym : Symmetric _≋_
+≋-sym {x} {y} (g by ιg∙x≈y) = g N.⁻¹ by begin
+  ι (g N.⁻¹) ∙ y      ≈⟨ ∙-cong (ι.⁻¹-homo g) (sym ιg∙x≈y) ⟩
+  ι g ⁻¹ ∙ (ι g ∙ x)  ≈⟨ cancelˡ (inverseˡ (ι g)) x ⟩
+  x                   ∎
+
+≋-trans : Transitive _≋_
+≋-trans {x} {y} {z} (g by ιg∙x≈y) (h by ιh∙y≈z) = h N.∙ g by begin
+  ι (h N.∙ g) ∙ x ≈⟨ ∙-congʳ (ι.∙-homo h g) ⟩
+  (ι h ∙ ι g) ∙ x ≈⟨ uv≈w⇒xu∙v≈xw ιg∙x≈y (ι h) ⟩
+  ι h ∙ y         ≈⟨ ιh∙y≈z ⟩
+  z               ∎
+
+≋-∙-cong : Congruent₂ _≋_ _∙_
+≋-∙-cong {x} {y} {u} {v} (g by ιg∙x≈y) (h by ιh∙u≈v) = g N.∙ h′ by begin
+  ι (g N.∙ h′) ∙ (x ∙ u) ≈⟨ ∙-congʳ (ι.∙-homo g h′) ⟩
+  (ι g ∙ ι h′) ∙ (x ∙ u) ≈⟨ uv≈wx⇒yu∙vz≈yw∙xz (normal h x) (ι g) u ⟩
+  (ι g ∙ x) ∙ (ι h ∙ u)  ≈⟨ ∙-cong ιg∙x≈y ιh∙u≈v ⟩
+  y ∙ v                  ∎
+  where h′ = conjugate h x
+
+≋-⁻¹-cong : Congruent₁ _≋_ _⁻¹
+≋-⁻¹-cong {x} {y} (g by ιg∙x≈y) = h by begin
+  ι h ∙ x ⁻¹        ≈⟨ normal (g N.⁻¹) (x ⁻¹) ⟩
+  x ⁻¹ ∙ ι (g N.⁻¹) ≈⟨ ∙-congˡ (ι.⁻¹-homo g) ⟩
+  x ⁻¹ ∙ ι g ⁻¹     ≈⟨ ⁻¹-anti-homo-∙ (ι g) x ⟨
+  (ι g ∙ x) ⁻¹      ≈⟨ ⁻¹-cong ιg∙x≈y ⟩
+  y ⁻¹              ∎
+  where h = conjugate (g N.⁻¹) (x ⁻¹)
+
+quotientGroup : Group c (c ⊔ ℓ ⊔ c′)
+quotientGroup = record
+  { isGroup = record
+    { isMonoid = record
+      { isSemigroup = record
+        { isMagma = record
+          { isEquivalence = record
+            { refl = ≋-refl
+            ; sym = ≋-sym
+            ; trans = ≋-trans
+            }
+          ; ∙-cong = ≋-∙-cong
+          }
+        ; assoc = λ x y z → ≈⇒≋ (assoc x y z)
+        }
+      ; identity = ≈⇒≋ ∘ identityˡ , ≈⇒≋ ∘ identityʳ
+      }
+    ; inverse = ≈⇒≋ ∘ inverseˡ , ≈⇒≋ ∘ inverseʳ
+    ; ⁻¹-cong = ≋-⁻¹-cong
+    }
+  }
+
+_/_ : Group c (c ⊔ ℓ ⊔ c′)
+_/_ = quotientGroup
+
+π : Group.Carrier G → Group.Carrier quotientGroup
+π x = x -- because we do all the work in the relation
+
+π-isMagmaHomomorphism : IsMagmaHomomorphism rawMagma (Group.rawMagma quotientGroup) π
+π-isMagmaHomomorphism = record
+  { isRelHomomorphism = record
+    { cong = ≈⇒≋
+    }
+  ; homo = λ _ _ → ≋-refl
+  }
+
+π-isMonoidHomomorphism : IsMonoidHomomorphism rawMonoid (Group.rawMonoid quotientGroup) π
+π-isMonoidHomomorphism = record
+  { isMagmaHomomorphism = π-isMagmaHomomorphism
+  ; ε-homo = ≋-refl
+  }
+
+π-isGroupHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) π
+π-isGroupHomomorphism = record
+  { isMonoidHomomorphism = π-isMonoidHomomorphism
+  ; ⁻¹-homo = λ _ → ≋-refl
+  }
+
+π-surjective : Surjective _≈_ _≋_ π
+π-surjective g = g , ≈⇒≋
diff --git a/src/Algebra/Construct/Sub/AbelianGroup.agda b/src/Algebra/Construct/Sub/AbelianGroup.agda
new file mode 100644
index 0000000000..be527587cd
--- /dev/null
+++ b/src/Algebra/Construct/Sub/AbelianGroup.agda
@@ -0,0 +1,48 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Subgroups of Abelian groups: necessarily Normal
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (AbelianGroup)
+
+module Algebra.Construct.Sub.AbelianGroup {c ℓ} (G : AbelianGroup c ℓ) where
+
+open import Algebra.Morphism.GroupMonomorphism using (isAbelianGroup)
+
+private
+  module G = AbelianGroup G
+
+open import Algebra.Construct.Sub.Group.Normal G.group
+  using (IsNormal; NormalSubgroup)
+
+-- Re-export the notion of subgroup of the underlying Group
+
+open import Algebra.Construct.Sub.Group G.group public
+  using (Subgroup)
+
+-- Then, for any such Subgroup:
+-- * it defines an AbelianGroup
+-- * and is, in fact, Normal
+
+module _ {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) where
+
+  open Subgroup subgroup public
+    using (ι; ι-monomorphism)
+
+  abelianGroup : AbelianGroup c′ ℓ′
+  abelianGroup = record
+    { isAbelianGroup = isAbelianGroup ι-monomorphism G.isAbelianGroup }
+
+  open AbelianGroup abelianGroup public
+
+  isNormal : IsNormal subgroup
+  isNormal = record { normal = λ n → G.comm (ι n) }
+
+  normalSubgroup : NormalSubgroup c′ ℓ′
+  normalSubgroup = record { isNormal = isNormal }
+
+  open NormalSubgroup normalSubgroup public
+    using (conjugate; normal)
diff --git a/src/Algebra/Construct/Sub/Group.agda b/src/Algebra/Construct/Sub/Group.agda
new file mode 100644
index 0000000000..a43a2070de
--- /dev/null
+++ b/src/Algebra/Construct/Sub/Group.agda
@@ -0,0 +1,31 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definition of subgroup via Group monomorphism
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (Group; RawGroup)
+
+module Algebra.Construct.Sub.Group {c ℓ} (G : Group c ℓ) where
+
+open import Algebra.Morphism.Structures using (IsGroupMonomorphism)
+open import Algebra.Morphism.GroupMonomorphism using (isGroup)
+open import Level using (suc; _⊔_)
+
+private
+  module G = Group G
+
+record Subgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
+  field
+    domain         : RawGroup c′ ℓ′
+    ι              : _ → G.Carrier
+    ι-monomorphism : IsGroupMonomorphism domain G.rawGroup ι
+
+  module ι = IsGroupMonomorphism ι-monomorphism
+
+  group : Group _ _
+  group = record { isGroup = isGroup ι-monomorphism G.isGroup }
+
+  open Group group public
diff --git a/src/Algebra/Construct/Sub/Group/Normal.agda b/src/Algebra/Construct/Sub/Group/Normal.agda
new file mode 100644
index 0000000000..4ff5f1d18c
--- /dev/null
+++ b/src/Algebra/Construct/Sub/Group/Normal.agda
@@ -0,0 +1,32 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definition of normal subgroups
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (Group)
+
+module Algebra.Construct.Sub.Group.Normal {c ℓ} (G : Group c ℓ)  where
+
+open import Algebra.Construct.Sub.Group G using (Subgroup)
+open import Level using (suc; _⊔_)
+
+private
+  module G = Group G
+
+-- every element of the subgroup commutes in G
+record IsNormal {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) : Set (c ⊔ ℓ ⊔ c′) where
+  open Subgroup subgroup using (ι)
+  field
+    conjugate : ∀ n g → _
+    normal : ∀ n g → ι (conjugate n g) G.∙ g G.≈ g G.∙ ι n
+
+record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
+  field
+    subgroup : Subgroup c′ ℓ′
+    isNormal : IsNormal subgroup
+
+  open Subgroup subgroup public
+  open IsNormal isNormal public

From bd5cfeed0b9073ca71959c0d6bb38d38a2e8a9da Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 5 Nov 2025 14:27:23 +0000
Subject: [PATCH 03/15] add: sub-`Bimodule`s

---
 CHANGELOG.md                                  |  2 +
 .../Module/Construct/Sub/Bimodule.agda        | 53 +++++++++++++++++++
 2 files changed, 55 insertions(+)
 create mode 100644 src/Algebra/Module/Construct/Sub/Bimodule.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3f3ad2178f..dd92156200 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -85,6 +85,8 @@ New modules
 
 * `Algebra.Construct.Sub.Group.Normal` for the definition of normal subgroups.
 
+* `Algebra.Module.Construct.Sub.Bimodule` for the definition of sub-bimodules.
+
 * `Algebra.Properties.BooleanRing`.
 
 * `Algebra.Properties.BooleanSemiring`.
diff --git a/src/Algebra/Module/Construct/Sub/Bimodule.agda b/src/Algebra/Module/Construct/Sub/Bimodule.agda
new file mode 100644
index 0000000000..19c778a4bf
--- /dev/null
+++ b/src/Algebra/Module/Construct/Sub/Bimodule.agda
@@ -0,0 +1,53 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definition of sub-bimodules
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (Ring)
+open import Algebra.Module.Bundles using (Bimodule; RawBimodule)
+
+module Algebra.Module.Construct.Sub.Bimodule
+  {cr ℓr cs ℓs cm ℓm} {R : Ring cr ℓr} {S : Ring cs ℓs}  (M : Bimodule R S cm ℓm)
+  where
+
+open import Algebra.Module.Morphism.Structures using (IsBimoduleMonomorphism)
+open import Algebra.Module.Morphism.BimoduleMonomorphism using (isBimodule)
+open import Level using (suc; _⊔_)
+
+private
+  module R = Ring R
+  module S = Ring S
+  module M = Bimodule M
+
+open import Algebra.Construct.Sub.AbelianGroup M.+ᴹ-abelianGroup
+  as AbelianSubgroup
+  using (Subgroup)
+
+------------------------------------------------------------------------
+-- Definition
+
+record Subbimodule cm′ ℓm′ : Set (cr ⊔ cs ⊔ cm ⊔ ℓm ⊔ suc (cm′ ⊔ ℓm′)) where
+  field
+    domain         : RawBimodule R.Carrier S.Carrier cm′ ℓm′
+    ι              : _ → M.Carrierᴹ
+    ι-monomorphism : IsBimoduleMonomorphism domain M.rawBimodule ι
+
+  module ι = IsBimoduleMonomorphism ι-monomorphism
+
+  bimodule : Bimodule R S _ _
+  bimodule = record
+    { isBimodule = isBimodule ι-monomorphism R.isRing S.isRing M.isBimodule }
+
+  open Bimodule bimodule public
+
+-- Additionally, have Abelian (hence: Normal) subgroups of M.+ᴹ-abelianGroup
+
+  subgroup : Subgroup cm′ ℓm′
+  subgroup = record { ι-monomorphism = ι.+ᴹ-isGroupMonomorphism }
+
+  isNormal = AbelianSubgroup.isNormal subgroup
+
+  normalSubgroup = AbelianSubgroup.normalSubgroup subgroup

From d3d6797ac2aabc9bec33f0f5dc1548896c27fc0e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 5 Nov 2025 14:31:13 +0000
Subject: [PATCH 04/15] fix: whitespace

---
 src/Algebra/Construct/Quotient/AbelianGroup.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Algebra/Construct/Quotient/AbelianGroup.agda b/src/Algebra/Construct/Quotient/AbelianGroup.agda
index 46ccdf3c68..25187d25c9 100644
--- a/src/Algebra/Construct/Quotient/AbelianGroup.agda
+++ b/src/Algebra/Construct/Quotient/AbelianGroup.agda
@@ -11,7 +11,7 @@ import Algebra.Construct.Sub.AbelianGroup as AbelianSubgroup
 
 module Algebra.Construct.Quotient.AbelianGroup
   {c ℓ} (G : AbelianGroup c ℓ)
-  (open AbelianSubgroup G using (Subgroup; normalSubgroup)) 
+  (open AbelianSubgroup G using (Subgroup; normalSubgroup))
   {c′ ℓ′} (N : Subgroup c′ ℓ′)
   where
 

From c05773b2d7afa038cda83132813771df13027fdb Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 5 Nov 2025 15:09:06 +0000
Subject: [PATCH 05/15] add: `Ideal`s and quotients of `Ring`s

---
 CHANGELOG.md                              |  2 +
 src/Algebra/Construct/Quotient/Ring.agda  | 76 +++++++++++++++++++++++
 src/Algebra/Construct/Sub/Ring/Ideal.agda | 26 ++++++++
 3 files changed, 104 insertions(+)
 create mode 100644 src/Algebra/Construct/Quotient/Ring.agda
 create mode 100644 src/Algebra/Construct/Sub/Ring/Ideal.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index dd92156200..403d274c0c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -85,6 +85,8 @@ New modules
 
 * `Algebra.Construct.Sub.Group.Normal` for the definition of normal subgroups.
 
+* `Algebra.Construct.Sub.Ring.Ideal` for the definition of ideals of a ring.
+
 * `Algebra.Module.Construct.Sub.Bimodule` for the definition of sub-bimodules.
 
 * `Algebra.Properties.BooleanRing`.
diff --git a/src/Algebra/Construct/Quotient/Ring.agda b/src/Algebra/Construct/Quotient/Ring.agda
new file mode 100644
index 0000000000..574f68c5ff
--- /dev/null
+++ b/src/Algebra/Construct/Quotient/Ring.agda
@@ -0,0 +1,76 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Quotient rings
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (AbelianGroup; Ring; RawRing)
+open import Algebra.Construct.Sub.Ring.Ideal using (Ideal)
+
+module Algebra.Construct.Quotient.Ring
+  {c ℓ} (R : Ring c ℓ) {c′ ℓ′} (I : Ideal R c′ ℓ′)
+  where
+
+open import Algebra.Morphism.Structures using (IsRingHomomorphism)
+open import Data.Product.Base using (_,_)
+open import Function.Base using (_∘_)
+open import Level using (_⊔_)
+
+import Algebra.Construct.Quotient.AbelianGroup as Quotient
+
+private
+  module R = Ring R
+  module I = Ideal I
+  module R/I = Quotient R.+-abelianGroup I.subgroup
+
+
+open R/I public
+  using (_≋_; _by_; ≋-refl; ≈⇒≋
+        ; quotientAbelianGroup
+        ; π; π-isMonoidHomomorphism; π-surjective
+        )
+
+open import Algebra.Definitions _≋_ using (Congruent₂)
+
+≋-*-cong : Congruent₂ R._*_
+≋-*-cong {x} {y} {u} {v} (j by ιj+x≈y) (k by ιk+u≈v) = ι j *ₗ k +ᴹ j *ᵣ u +ᴹ x *ₗ k by begin
+  ι (ι j *ₗ k +ᴹ j *ᵣ u +ᴹ x *ₗ k) + x * u       ≈⟨ +-congʳ (ι.+ᴹ-homo (ι j *ₗ k +ᴹ j *ᵣ u) (x *ₗ k)) ⟩
+  ι (ι j *ₗ k +ᴹ j *ᵣ u) + ι (x *ₗ k) + x * u    ≈⟨ +-congʳ (+-congʳ (ι.+ᴹ-homo (ι j *ₗ k) (j *ᵣ u))) ⟩
+  ι (ι j *ₗ k) + ι (j *ᵣ u) + ι (x *ₗ k) + x * u ≈⟨ +-congʳ (+-cong (+-cong (ι.*ₗ-homo (ι j) k) (ι.*ᵣ-homo u j)) (ι.*ₗ-homo x k)) ⟩
+  ι j * ι k + ι j * u + x * ι k + x * u          ≈⟨ binomial-expansion (ι j) x (ι k) u ⟨
+  (ι j + x) * (ι k + u)                          ≈⟨ *-cong ιj+x≈y ιk+u≈v ⟩
+  y * v                                          ∎
+  where
+  open R using (_+_; _*_; +-congʳ ;+-cong; *-cong)
+  open import Algebra.Properties.Semiring R.semiring using (binomial-expansion)
+  open import Relation.Binary.Reasoning.Setoid R.setoid
+  open I using (ι; _*ₗ_; _*ᵣ_; _+ᴹ_)
+
+quotientRawRing : RawRing c (c ⊔ ℓ ⊔ c′)
+quotientRawRing = record { RawRing R.rawRing hiding (_≈_) ; _≈_ = _≋_ }
+
+quotientRing : Ring c (c ⊔ ℓ ⊔ c′)
+quotientRing = record
+  { isRing = record
+    { +-isAbelianGroup = isAbelianGroup
+    ; *-cong = ≋-*-cong
+    ; *-assoc = λ x y z → ≈⇒≋ (R.*-assoc x y z)
+    ; *-identity = ≈⇒≋ ∘ R.*-identityˡ , ≈⇒≋ ∘ R.*-identityʳ
+    ; distrib = (λ x y z → ≈⇒≋ (R.distribˡ x y z)) , (λ x y z → ≈⇒≋ (R.distribʳ x y z))
+    }
+  } where open AbelianGroup quotientAbelianGroup using (isAbelianGroup)
+
+π-isRingHomomorphism : IsRingHomomorphism R.rawRing quotientRawRing π
+π-isRingHomomorphism = record
+  { isSemiringHomomorphism = record
+    { isNearSemiringHomomorphism = record
+      { +-isMonoidHomomorphism = π-isMonoidHomomorphism
+      ; *-homo = λ _ _ → ≋-refl
+      }
+    ; 1#-homo = ≋-refl
+    }
+  ; -‿homo = λ _ → ≋-refl
+  }
+
diff --git a/src/Algebra/Construct/Sub/Ring/Ideal.agda b/src/Algebra/Construct/Sub/Ring/Ideal.agda
new file mode 100644
index 0000000000..ceac1c1fb3
--- /dev/null
+++ b/src/Algebra/Construct/Sub/Ring/Ideal.agda
@@ -0,0 +1,26 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Ideals of a ring
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (Ring)
+
+module Algebra.Construct.Sub.Ring.Ideal {c ℓ} (R : Ring c ℓ) where
+
+open import Algebra.Module.Construct.Sub.Bimodule using (Subbimodule)
+open import Algebra.Module.Construct.TensorUnit using (bimodule)
+open import Level
+
+------------------------------------------------------------------------
+-- Definition
+-- a (two sided) ideal is exactly a subbimodule of R considered as a bimodule over itself
+
+record Ideal c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
+  field
+
+    subbimodule : Subbimodule {R = R} bimodule c′ ℓ′
+
+  open Subbimodule subbimodule public

From b707d833c5d2d2e5fb9709ba1ad66f2be4791164 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 5 Nov 2025 15:14:39 +0000
Subject: [PATCH 06/15] fix: tidy up

---
 src/Algebra/Construct/Sub/Ring/Ideal.agda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Algebra/Construct/Sub/Ring/Ideal.agda b/src/Algebra/Construct/Sub/Ring/Ideal.agda
index ceac1c1fb3..8e40d0d7e1 100644
--- a/src/Algebra/Construct/Sub/Ring/Ideal.agda
+++ b/src/Algebra/Construct/Sub/Ring/Ideal.agda
@@ -12,7 +12,7 @@ module Algebra.Construct.Sub.Ring.Ideal {c ℓ} (R : Ring c ℓ) where
 
 open import Algebra.Module.Construct.Sub.Bimodule using (Subbimodule)
 open import Algebra.Module.Construct.TensorUnit using (bimodule)
-open import Level
+open import Level using (suc; _⊔_)
 
 ------------------------------------------------------------------------
 -- Definition
@@ -20,7 +20,6 @@ open import Level
 
 record Ideal c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
   field
-
     subbimodule : Subbimodule {R = R} bimodule c′ ℓ′
 
   open Subbimodule subbimodule public

From 3a75f5f521e698f70eef265c4510b5fdc6cba95b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 9 Nov 2025 10:23:35 +0000
Subject: [PATCH 07/15] comment: extensively on the design rationale

---
 src/Algebra/Construct/Sub/Group.agda | 71 +++++++++++++++++++++++++++-
 1 file changed, 70 insertions(+), 1 deletion(-)

diff --git a/src/Algebra/Construct/Sub/Group.agda b/src/Algebra/Construct/Sub/Group.agda
index a43a2070de..072073a0a8 100644
--- a/src/Algebra/Construct/Sub/Group.agda
+++ b/src/Algebra/Construct/Sub/Group.agda
@@ -2,6 +2,9 @@
 -- The Agda standard library
 --
 -- Definition of subgroup via Group monomorphism
+--
+-- Based on Nathan van Doorn (Taneb)'s original PR
+-- https://github.com/agda/agda-stdlib/pull/2852
 ------------------------------------------------------------------------
 
 {-# OPTIONS --safe --cubical-compatible #-}
@@ -17,14 +20,80 @@ open import Level using (suc; _⊔_)
 private
   module G = Group G
 
+------------------------------------------------------------------------
+-- Definition
+--
+-- Fundamentally, this design is the same as in the above PR:
+-- a `SubX` is given by an `X` monomorphism...
+-- ... to be able to define such, the current library design requires
+-- * *some* `X`-domain of definition for the mono, here given by the
+--   placeholder name `domain`, which otherwise plays no role externally
+-- * an underlying bare ('raw') function defining the mono, here called
+--   (in search of a  canonical name) `ι`, standing for 'injection'
+-- * the juice: that `ι` indeed defines a mono from the domain to the
+--   (underlying defining `rawX` subfield of the) top-level `X` module parameter
+
 record Subgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
   field
+
+-- as above, this name is essentially arbitrary,
+-- exisitng solely to be mentioned in the third field below
+
     domain         : RawGroup c′ ℓ′
-    ι              : _ → G.Carrier
+
+-- this function (obviously) needs a source and target:
+-- * the target, for the sake of the third field, needs to be
+--   `Carrier` subfield of the top-level `X` module parameter
+-- * the source, however, really exists solely to give a type to `ι`
+--   and indeed, the typechecker can infer (from the third field)
+--   that this type *must* be the `Carrier` of the `RawX` `domain`
+
+-- Taneb's design introduces a `private` module
+-- `private module H = RawGroup domain`
+-- for the sake of affording easy/easier named access to its
+-- `Carrier` field, and as preferable to the hideous explicit form
+-- `RawGroup.Carrier domain` which is the definiens of `H.Carrier`
+
+-- Neither is necessary, but can be, and is, reconstructed by the
+-- typechecker by offering instead a placeholder, in exactly the same way
+-- that `domain` exists as a named field solely to express the dependency
+-- in the type of `ι-monomorphism`. In that sense, it is an ephemeral form
+-- derived from `domain`, which moreover will never play a role in client
+-- uses of this module, except as a typing constraint on any application
+-- of `ι`, a constraint which is already inherited (by definitional equality!)
+-- from the type of the `⟦_⟧` parameter to `IsXHomomorphism`...
+
+    ι              : _ → G.Carrier -- where _ = RawGroup.Carrier domain
+
+-- now all the pieces are in place, we can define what we *really* want
+
     ι-monomorphism : IsGroupMonomorphism domain G.rawGroup ι
 
+-- this is 'admin': any client module of `Subgroup` will likely want to
+-- refer to primitive *and* manifest subfields of `IsXMonmorphism`, so
+-- this is automatically made available to clients, but not `open`ed,
+-- so that such affordance is client-definable, as usual.
+
   module ι = IsGroupMonomorphism ι-monomorphism
 
+-- Similarly, but mathematically motivated: any client module of `Subgroup`
+-- will want access to *the `X` defined as the domain of the `IsXMonomorphism`*.
+-- But here, it is both automatically made available to clients, as above,
+-- *and* also `open`ed, so that its affordances are offered to any client
+-- via the 'canonical' names associated with the `X`/`IsX` bundle/structure
+
+-- Taneb's design does this in two steps:
+-- * first, create the `IsX` structure, with name `isX`
+-- * second, create the `X` bundle` via `isX`
+
+-- My own thinking on this has evolved: I would rather go straight for the
+-- bundle, from which `isX : IsX ...` is definable/exported by `open`.
+-- This avoids having to recapitulate the verbose telescope involved in any
+-- `IsX <telescope>` (and any design decisions/commitments around such things),
+-- or having to choose a name for the `isX` field, when, once again, all the
+-- heavy lifting is already made available by the `XHomomorphism` module, so
+-- for general DRY reasons, should not be repeated here.
+
   group : Group _ _
   group = record { isGroup = isGroup ι-monomorphism G.isGroup }
 

From 4d72ed0002558d769ed4ca7478b314efc5a9b410 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 9 Nov 2025 11:24:32 +0000
Subject: [PATCH 08/15] comment: extensively on `NormalSubgroup` (sic)

---
 src/Algebra/Construct/Sub/Group.agda        | 41 +++++++-------
 src/Algebra/Construct/Sub/Group/Normal.agda | 59 ++++++++++++++++++++-
 2 files changed, 78 insertions(+), 22 deletions(-)

diff --git a/src/Algebra/Construct/Sub/Group.agda b/src/Algebra/Construct/Sub/Group.agda
index 072073a0a8..550f0689db 100644
--- a/src/Algebra/Construct/Sub/Group.agda
+++ b/src/Algebra/Construct/Sub/Group.agda
@@ -36,43 +36,44 @@ private
 record Subgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
   field
 
--- as above, this name is essentially arbitrary,
--- exisitng solely to be mentioned in the third field below
+-- As above, the following name is essentially arbitrary, existing
+-- solely to be mentioned in the third field `ι-monomorphism` below.
 
     domain         : RawGroup c′ ℓ′
 
--- this function (obviously) needs a source and target:
--- * the target, for the sake of the third field, needs to be
---   `Carrier` subfield of the top-level `X` module parameter
+-- The next field, a function, (obviously) needs a source and target:
+-- * the target, again for the sake of the third field, needs to be
+--   `Carrier` subfield of the top-level `X` module parameter;
 -- * the source, however, really exists solely to give a type to `ι`
---   and indeed, the typechecker can infer (from the third field)
---   that this type *must* be the `Carrier` of the `RawX` `domain`
+--   and indeed, the typechecker can infer (again from the third field)
+--   that this type *must* be the `Carrier` of the `RawX` `domain`.
 
 -- Taneb's design introduces a `private` module
 -- `private module H = RawGroup domain`
 -- for the sake of affording easy/easier named access to its
 -- `Carrier` field, and as preferable to the hideous explicit form
--- `RawGroup.Carrier domain` which is the definiens of `H.Carrier`
+-- `RawGroup.Carrier domain` which is the definiens of `H.Carrier`.
 
--- Neither is necessary, but can be, and is, reconstructed by the
--- typechecker by offering instead a placeholder, in exactly the same way
+-- Neither is necessary, but instead can be, and is here, reconstructed by
+-- the typechecker by offering instead a placeholder, in exactly the same way
 -- that `domain` exists as a named field solely to express the dependency
 -- in the type of `ι-monomorphism`. In that sense, it is an ephemeral form
--- derived from `domain`, which moreover will never play a role in client
--- uses of this module, except as a typing constraint on any application
--- of `ι`, a constraint which is already inherited (by definitional equality!)
--- from the type of the `⟦_⟧` parameter to `IsXHomomorphism`...
+-- derived from `domain`, which moreover will *never* play a role in client
+-- uses of this module (eg exemplarily in `Algebra.Construct.Sub.Group.Normal),
+-- except as a typing constraint on any application of `ι`, a constraint
+-- which is already inherited (by definitional equality!) from the type of
+-- the `⟦_⟧` parameter to `IsXHomomorphism`...
 
     ι              : _ → G.Carrier -- where _ = RawGroup.Carrier domain
 
--- now all the pieces are in place, we can define what we *really* want
+-- Now all the pieces are in place, we can define what we *really* want:
 
     ι-monomorphism : IsGroupMonomorphism domain G.rawGroup ι
 
--- this is 'admin': any client module of `Subgroup` will likely want to
--- refer to primitive *and* manifest subfields of `IsXMonmorphism`, so
--- this is automatically made available to clients, but not `open`ed,
--- so that such affordance is client-definable, as usual.
+-- The next manifest field is an 'admin' decision: any client module of
+-- `Subgroup` will likely want to refer to primitive *and* manifest subfields
+-- of `IsXMonomorphism`, so this is automatically made available to clients,
+-- but not `open`ed, so that such affordance is client-definable, as usual.
 
   module ι = IsGroupMonomorphism ι-monomorphism
 
@@ -80,7 +81,7 @@ record Subgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
 -- will want access to *the `X` defined as the domain of the `IsXMonomorphism`*.
 -- But here, it is both automatically made available to clients, as above,
 -- *and* also `open`ed, so that its affordances are offered to any client
--- via the 'canonical' names associated with the `X`/`IsX` bundle/structure
+-- via the 'canonical' names associated with the `X`/`IsX` bundle/structure.
 
 -- Taneb's design does this in two steps:
 -- * first, create the `IsX` structure, with name `isX`
diff --git a/src/Algebra/Construct/Sub/Group/Normal.agda b/src/Algebra/Construct/Sub/Group/Normal.agda
index 4ff5f1d18c..e12b9e328a 100644
--- a/src/Algebra/Construct/Sub/Group/Normal.agda
+++ b/src/Algebra/Construct/Sub/Group/Normal.agda
@@ -2,31 +2,86 @@
 -- The Agda standard library
 --
 -- Definition of normal subgroups
+--
+-- Based on Nathan van Doorn (Taneb)'s original PR
+-- https://github.com/agda/agda-stdlib/pull/2852
 ------------------------------------------------------------------------
 
 {-# OPTIONS --safe --cubical-compatible #-}
 
 open import Algebra.Bundles using (Group)
 
+-- This module relocates Taneb's original `Algebra.NormalSubgroup`
+-- to a level one *below* that of `Algebra.Construct.Sub.Group`,
+-- for the 'obvious' inheritance hierarchy 'reason' that a
+-- `NormalSubgroup` is a specialisation of the notion of `Subgroup`.
+
+-- `Normal` as a root name avoids recapitulation of the parent name
+-- `Subgroup`, but also permits/does not frustrate development of a
+-- companion `Construct` sub-hierarchy (intersections etc.) below
+-- `Algebra/Construct/Sub/Group/Normal` as a sub-directory.
+
 module Algebra.Construct.Sub.Group.Normal {c ℓ} (G : Group c ℓ)  where
 
 open import Algebra.Construct.Sub.Group G using (Subgroup)
+open import Function.Base using (typeOf)
 open import Level using (suc; _⊔_)
 
 private
   module G = Group G
 
--- every element of the subgroup commutes in G
+------------------------------------------------------------------------
+-- Definition
+--
+-- IsNormal: every element of the given subgroup commutes in the parent.
+--
+-- This defined as a `record`, as usual in order to improve type inference,
+-- specifically that a `NormalSubgroup` below may (usually) be definable
+-- solely by supplying its `isNormal` field.
+
 record IsNormal {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) : Set (c ⊔ ℓ ⊔ c′) where
+
+-- A design question here is how much of the `Subgroup` structure should/must
+-- be exposed in the course of defining the fields here.
+
+-- Surely we need the name of the function which witnesses 'subX'-ness,
+-- but not the property `ι-isXMonomorphism`.
+
   open Subgroup subgroup using (ι)
+
   field
-    conjugate : ∀ n g → _
+
+-- But it's not obvious that we need the (name of) `Carrier` of the `domain`
+-- of the `Subgroup`, viz. the source of `ι`, except as the type of variables
+-- quantifed here as `n` (as generic name for 'element's of the normal subgroup).
+
+-- As with `Subgroup` itself, this domain `Carrier` type is canonically inferrable
+-- by the typechecker, as in the inline comment. But perhaps this use of `_` might
+-- also be usefully documented as `Function.Base.typeOf n`?
+
+    conjugate : ∀ n g → _ -- where _ = RawGroup.Carrier (Subgroup.domain subgroup)
+
+-- The main field of interest only requires that the `conjugate` field be
+-- of type 'source of `ι`'; but we don't need that type here, otherwise the
+-- `∀ n` quantifier would need an explicit type label, and such inferrability
+-- reinforces the decision nowhere to name this type.
+
     normal : ∀ n g → ι (conjugate n g) G.∙ g G.≈ g G.∙ ι n
 
+-- NormalSubgroup: a Subgroup which IsNormal (sic)
+
 record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
   field
     subgroup : Subgroup c′ ℓ′
     isNormal : IsNormal subgroup
 
+-- But again, and for generic `library-design` reasons, we publicaly export
+-- all the subfields of each field, in order to afford a standardised vocabulary
+-- for all the structure intended to be in scope when using a `NormalSubgroup`.
+
+-- Locally, we have used only name `ι` in the definition of `IsNormal`,
+-- but clients may also want access ot the full signature (eg. esp. the
+-- `ι-isGroupMonomorphism` field which characterises being a subgroup).
+
   open Subgroup subgroup public
   open IsNormal isNormal public

From 18d99ef83b90dd505a7fc6037be53748f50d3909 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 9 Nov 2025 12:53:56 +0000
Subject: [PATCH 09/15] comment: extensively on `AbelianSubgroup`

---
 src/Algebra/Construct/Sub/AbelianGroup.agda | 44 +++++++++++++++++----
 src/Algebra/Construct/Sub/Group/Normal.agda | 14 ++++++-
 2 files changed, 49 insertions(+), 9 deletions(-)

diff --git a/src/Algebra/Construct/Sub/AbelianGroup.agda b/src/Algebra/Construct/Sub/AbelianGroup.agda
index be527587cd..90a93debe4 100644
--- a/src/Algebra/Construct/Sub/AbelianGroup.agda
+++ b/src/Algebra/Construct/Sub/AbelianGroup.agda
@@ -2,6 +2,12 @@
 -- The Agda standard library
 --
 -- Subgroups of Abelian groups: necessarily Normal
+--
+-- This is a strict addition/extension to Nathan van Doorn (Taneb)'s PR
+-- https://github.com/agda/agda-stdlib/pull/2852
+-- and avoids the lemma `Algebra.NormalSubgroup.abelian⇒subgroup-normal`
+-- introduced in PR https://github.com/agda/agda-stdlib/pull/2854
+-- in favour of the direct definition of the field `normal` below.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --safe --cubical-compatible #-}
@@ -10,11 +16,21 @@ open import Algebra.Bundles using (AbelianGroup)
 
 module Algebra.Construct.Sub.AbelianGroup {c ℓ} (G : AbelianGroup c ℓ) where
 
+-- As with the corresponding appeal to `IsGroup` in the module
+-- `Algebra.Construct.Sub.AbelianGroup`, this import drives the export
+-- of the `X` bundle corresponding to the `subX` structure/bundle
+-- being defined here.
+
 open import Algebra.Morphism.GroupMonomorphism using (isAbelianGroup)
 
 private
   module G = AbelianGroup G
 
+-- Here, we could chose simply to expose the `NormalSubgroup` definition
+-- from `Algebra.Construct.Sub.Group.Normal`, but as this module will use
+-- type inference to allow the creation of `NormalSubgroup`s based on their
+-- `isNormal` fields alone, it makes sense also to export the type `IsNormal`.
+
 open import Algebra.Construct.Sub.Group.Normal G.group
   using (IsNormal; NormalSubgroup)
 
@@ -24,25 +40,39 @@ open import Algebra.Construct.Sub.Group G.group public
   using (Subgroup)
 
 -- Then, for any such Subgroup:
--- * it defines an AbelianGroup
--- * and is, in fact, Normal
+-- * it is, in fact, Normal
+-- * and defines an AbelianGroup, not just a Group
 
 module _ {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) where
 
+-- Here, we do need both the underlying function `ι` of the mono, and
+-- the proof `ι-monomorphism`, in order to be able to construct an
+-- `IsAbelianGroup` structure on the way to the `AbelianGroup` bundle.
+
   open Subgroup subgroup public
     using (ι; ι-monomorphism)
 
-  abelianGroup : AbelianGroup c′ ℓ′
-  abelianGroup = record
-    { isAbelianGroup = isAbelianGroup ι-monomorphism G.isAbelianGroup }
-
-  open AbelianGroup abelianGroup public
+-- Here, we eta-contract the use of `G.comm` in defining the `normal` field.
 
   isNormal : IsNormal subgroup
   isNormal = record { normal = λ n → G.comm (ι n) }
 
+-- And the use of `record`s throughout permits this 'boilerplate' construction.
+
   normalSubgroup : NormalSubgroup c′ ℓ′
   normalSubgroup = record { isNormal = isNormal }
 
+-- And the `public` re-export of its substructure.
+
   open NormalSubgroup normalSubgroup public
     using (conjugate; normal)
+
+-- As with `Algebra.Construct.Sub.Group`, there seems no need to create
+-- an intermediate manifest field `isAbelianGroup`, when this may be, and
+-- is, obtained by opening the bundle for `public` export.
+
+  abelianGroup : AbelianGroup c′ ℓ′
+  abelianGroup = record
+    { isAbelianGroup = isAbelianGroup ι-monomorphism G.isAbelianGroup }
+
+  open AbelianGroup abelianGroup public
diff --git a/src/Algebra/Construct/Sub/Group/Normal.agda b/src/Algebra/Construct/Sub/Group/Normal.agda
index e12b9e328a..41dff5e76b 100644
--- a/src/Algebra/Construct/Sub/Group/Normal.agda
+++ b/src/Algebra/Construct/Sub/Group/Normal.agda
@@ -57,7 +57,8 @@ record IsNormal {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) : Set (c ⊔ ℓ
 
 -- As with `Subgroup` itself, this domain `Carrier` type is canonically inferrable
 -- by the typechecker, as in the inline comment. But perhaps this use of `_` might
--- also be usefully documented as `Function.Base.typeOf n`?
+-- also be usefully documented as `Function.Base.typeOf n`? Or is that itself too
+-- 'occult' a usage?
 
     conjugate : ∀ n g → _ -- where _ = RawGroup.Carrier (Subgroup.domain subgroup)
 
@@ -68,7 +69,7 @@ record IsNormal {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) : Set (c ⊔ ℓ
 
     normal : ∀ n g → ι (conjugate n g) G.∙ g G.≈ g G.∙ ι n
 
--- NormalSubgroup: a Subgroup which IsNormal (sic)
+-- NormalSubgroup: a Subgroup which IsNormal (sic).
 
 record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
   field
@@ -85,3 +86,12 @@ record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) wh
 
   open Subgroup subgroup public
   open IsNormal isNormal public
+
+-- NB. Nowhere does this module define, nor need to, the lemma introduced in
+-- Taneb's original PR, viz. `abelian⇒subgroup-normal` of type
+-- `Commutative G._≈_ G._∙_ → (subgroup : Subgroup _ _) → IsNormal subgroup`.
+--
+-- This element of reasoning is itself handled by having a distinct module
+-- `Algebra.Construct.Sub.AbelianGroup` which encapsulates such reasoning
+-- within the scope of (an `Abelian`!)`Group` `G` in which the premise
+-- `Commutative G._≈_ G._∙_` is already known to hold.

From 882c56c96de1c78b3edfb3b1dd5aa84eed1e89e9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 9 Nov 2025 13:32:03 +0000
Subject: [PATCH 10/15] comment: extensively on `Subbimodule`

---
 .../Module/Construct/Sub/Bimodule.agda        | 29 ++++++++++++++++++-
 1 file changed, 28 insertions(+), 1 deletion(-)

diff --git a/src/Algebra/Module/Construct/Sub/Bimodule.agda b/src/Algebra/Module/Construct/Sub/Bimodule.agda
index 19c778a4bf..3c8d5fcf2a 100644
--- a/src/Algebra/Module/Construct/Sub/Bimodule.agda
+++ b/src/Algebra/Module/Construct/Sub/Bimodule.agda
@@ -2,6 +2,15 @@
 -- The Agda standard library
 --
 -- Definition of sub-bimodules
+--
+-- This is based on Nathan van Doorn (Taneb)'s PR
+-- https://github.com/agda/agda-stdlib/pull/2852
+-- but uses the `Algebra.Construct.Sub.AbelianGroup` module
+-- to plumb in that any sub-bimodule of a `Bimodule` defines
+-- a sub-AbelianGroup, hence a `NormalSubgroup`, so that when
+-- an ideal in a `Ring` is defined as a suitable sub-bimodule,
+-- the quotient structure of the additive subgroup is immediate,
+-- on which the quotient `Ring` structure may then be defined.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -32,9 +41,21 @@ open import Algebra.Construct.Sub.AbelianGroup M.+ᴹ-abelianGroup
 record Subbimodule cm′ ℓm′ : Set (cr ⊔ cs ⊔ cm ⊔ ℓm ⊔ suc (cm′ ⊔ ℓm′)) where
   field
     domain         : RawBimodule R.Carrier S.Carrier cm′ ℓm′
-    ι              : _ → M.Carrierᴹ
+
+-- As with `Algebra.Construct.Sub.Group{.Normal}`, we refrain from explicit
+-- naming of the source type of the underlying function. In terms of the
+-- `RawBimodule` signature, this is `Carrierᴹ`, which will also be,
+-- definitionally, the `Carrier` of the associated `(Abelian)Group` sub-bundle
+-- defined by `ι.+ᴹ-isGroupMonomorphism` below.
+
+    ι              : _ → M.Carrierᴹ -- where _ = RawBimodule.Carrierᴹ domain
+
     ι-monomorphism : IsBimoduleMonomorphism domain M.rawBimodule ι
 
+-- As with `Algebra.Construct.Sub.Group`, we create a module out of the
+-- `IsBimoduleMonomorphism` field, allowing us to expose its rich derived
+-- substructures, here specifically, the `+ᴹ-isGroupMonomorphism` definition.
+
   module ι = IsBimoduleMonomorphism ι-monomorphism
 
   bimodule : Bimodule R S _ _
@@ -48,6 +69,12 @@ record Subbimodule cm′ ℓm′ : Set (cr ⊔ cs ⊔ cm ⊔ ℓm ⊔ suc (cm′
   subgroup : Subgroup cm′ ℓm′
   subgroup = record { ι-monomorphism = ι.+ᴹ-isGroupMonomorphism }
 
+-- Exporting these two fields, but *without* their types, allows us to
+-- avoid explicit import of `Algebra.Construct.Sub.Group.Normal`, in
+-- favour of their encapsulation in `Algebra.Construct.Sub.AbelianGroup`.
+
+-- isNormal : Algebra.Construct.Sub.Group.Normal.IsNormal M.+ᴹ-group subgroup
   isNormal = AbelianSubgroup.isNormal subgroup
 
+-- normalSubgroup : Algebra.Construct.Sub.Group.Normal.NormalSubgroup M.+ᴹ-group _ _
   normalSubgroup = AbelianSubgroup.normalSubgroup subgroup

From bc146da4978caf3c5c4c3ba15076037d874caa7e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 9 Nov 2025 13:43:15 +0000
Subject: [PATCH 11/15] comment: the design of `Ideal`

---
 src/Algebra/Construct/Sub/Ring/Ideal.agda      | 16 +++++++++++++++-
 src/Algebra/Module/Construct/Sub/Bimodule.agda |  5 +++--
 2 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/src/Algebra/Construct/Sub/Ring/Ideal.agda b/src/Algebra/Construct/Sub/Ring/Ideal.agda
index 8e40d0d7e1..b345a10e65 100644
--- a/src/Algebra/Construct/Sub/Ring/Ideal.agda
+++ b/src/Algebra/Construct/Sub/Ring/Ideal.agda
@@ -2,12 +2,19 @@
 -- The Agda standard library
 --
 -- Ideals of a ring
+--
+-- Based on Nathan van Doorn (Taneb)'s original PR
+-- https://github.com/agda/agda-stdlib/pull/2855
 ------------------------------------------------------------------------
 
 {-# OPTIONS --safe --cubical-compatible #-}
 
 open import Algebra.Bundles using (Ring)
 
+-- As with `Algebra.Construct.Sub.Group.Normal`, this module
+-- relocates Taneb's original `Algebra.Ideal`
+-- to a level one *below* that of `Algebra.Construct.Sub.Ring`.
+
 module Algebra.Construct.Sub.Ring.Ideal {c ℓ} (R : Ring c ℓ) where
 
 open import Algebra.Module.Construct.Sub.Bimodule using (Subbimodule)
@@ -16,10 +23,17 @@ open import Level using (suc; _⊔_)
 
 ------------------------------------------------------------------------
 -- Definition
--- a (two sided) ideal is exactly a subbimodule of R considered as a bimodule over itself
+--
+-- A (two sided) ideal is exactly a sub-bimodule of R, considered as
+-- a bimodule (the `TensorUnit` for that category) over itself.
 
 record Ideal c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
   field
     subbimodule : Subbimodule {R = R} bimodule c′ ℓ′
 
+-- The definition of `Subbimodule` now exports the `normalSubgroup`
+-- and `abelianGroup` definitions, so that a `Ring` modulo an `Ideal`
+-- already has direct access to the underlying quotient `(Abelian)Group`
+-- structure on the additive group of the ring.
+
   open Subbimodule subbimodule public
diff --git a/src/Algebra/Module/Construct/Sub/Bimodule.agda b/src/Algebra/Module/Construct/Sub/Bimodule.agda
index 3c8d5fcf2a..d270d3ed2c 100644
--- a/src/Algebra/Module/Construct/Sub/Bimodule.agda
+++ b/src/Algebra/Module/Construct/Sub/Bimodule.agda
@@ -8,9 +8,10 @@
 -- but uses the `Algebra.Construct.Sub.AbelianGroup` module
 -- to plumb in that any sub-bimodule of a `Bimodule` defines
 -- a sub-AbelianGroup, hence a `NormalSubgroup`, so that when
--- an ideal in a `Ring` is defined as a suitable sub-bimodule,
+-- an `Ideal` in a `Ring` is defined as a suitable sub-bimodule,
+-- as in https://github.com/agda/agda-stdlib/pull/2855
 -- the quotient structure of the additive subgroup is immediate,
--- on which the quotient `Ring` structure may then be defined.
+-- on which the quotient `Ring` structure may then be based.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}

From 3ac84f3864e2973e0e5dd8dec11e7520efa0fcd8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 9 Nov 2025 18:30:44 +0000
Subject: [PATCH 12/15] comment/refactor: `Ideal`

---
 src/Algebra/Construct/Sub/Ring/Ideal.agda | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Algebra/Construct/Sub/Ring/Ideal.agda b/src/Algebra/Construct/Sub/Ring/Ideal.agda
index b345a10e65..2bae176ace 100644
--- a/src/Algebra/Construct/Sub/Ring/Ideal.agda
+++ b/src/Algebra/Construct/Sub/Ring/Ideal.agda
@@ -13,7 +13,8 @@ open import Algebra.Bundles using (Ring)
 
 -- As with `Algebra.Construct.Sub.Group.Normal`, this module
 -- relocates Taneb's original `Algebra.Ideal`
--- to a level one *below* that of `Algebra.Construct.Sub.Ring`.
+-- to a level one *below* that of `Algebra.Construct.Sub.Ring`,
+-- notwithstanding that we have yet to define `Sub.XRing`s...
 
 module Algebra.Construct.Sub.Ring.Ideal {c ℓ} (R : Ring c ℓ) where
 

From 6522369f675b92f55c3ad85d36f250afc57beb81 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 9 Nov 2025 18:36:45 +0000
Subject: [PATCH 13/15] refactor: simplify `Quotient`s

---
 .../Construct/Quotient/AbelianGroup.agda      |  14 ++-
 src/Algebra/Construct/Quotient/Group.agda     | 118 +++++++++---------
 src/Algebra/Construct/Quotient/Ring.agda      |  49 ++++----
 3 files changed, 94 insertions(+), 87 deletions(-)

diff --git a/src/Algebra/Construct/Quotient/AbelianGroup.agda b/src/Algebra/Construct/Quotient/AbelianGroup.agda
index 25187d25c9..9740242f01 100644
--- a/src/Algebra/Construct/Quotient/AbelianGroup.agda
+++ b/src/Algebra/Construct/Quotient/AbelianGroup.agda
@@ -8,6 +8,7 @@
 
 open import Algebra.Bundles using (Group; AbelianGroup)
 import Algebra.Construct.Sub.AbelianGroup as AbelianSubgroup
+import Algebra.Construct.Quotient.Group as Quotient
 
 module Algebra.Construct.Quotient.AbelianGroup
   {c ℓ} (G : AbelianGroup c ℓ)
@@ -20,16 +21,19 @@ private
 
 -- Re-export the quotient group
 
-open import Algebra.Construct.Quotient.Group G.group (normalSubgroup N) public
+open Quotient G.group (normalSubgroup N) public
+  hiding (_/_)
 
 -- With its additional bundle
 
-quotientAbelianGroup : AbelianGroup c _
-quotientAbelianGroup = record
+abelianGroup : AbelianGroup c _
+abelianGroup = record
   { isAbelianGroup = record
     { isGroup = isGroup
     ; comm = λ g h → ≈⇒≋ (G.comm g h)
     }
-  } where open Group quotientGroup
+  } where open Group group
 
--- Public re-exports, as needed?
+-- Public re-exports
+
+_/_ = abelianGroup
diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda
index 99e22352cf..7d06d200cc 100644
--- a/src/Algebra/Construct/Quotient/Group.agda
+++ b/src/Algebra/Construct/Quotient/Group.agda
@@ -13,8 +13,7 @@ module Algebra.Construct.Quotient.Group
   {c ℓ} (G : Group c ℓ) {c′ ℓ′} (N : NormalSubgroup G c′ ℓ′) where
 
 open import Algebra.Definitions using (Congruent₁; Congruent₂)
-open import Algebra.Morphism.Structures
-  using (IsMagmaHomomorphism; IsMonoidHomomorphism; IsGroupHomomorphism)
+open import Algebra.Morphism.Structures using (IsGroupHomomorphism)
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘_)
 open import Function.Definitions using (Surjective)
@@ -24,103 +23,106 @@ open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
 
 private
   open module G = Group G
-
-open import Algebra.Properties.Group G using (⁻¹-anti-homo-∙)
-open import Algebra.Properties.Monoid monoid
-open import Relation.Binary.Reasoning.Setoid setoid
-
-private
+    using (_≈_; _∙_; ε; _⁻¹)
   open module N = NormalSubgroup N
     using (ι; module ι; conjugate; normal)
 
+open import Algebra.Properties.Group G using (⁻¹-anti-homo-∙)
+open import Algebra.Properties.Monoid G.monoid
+open import Relation.Binary.Reasoning.Setoid G.setoid
+
 infix 0 _by_
 
-data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where
+data _≋_ (x y : G.Carrier) : Set (c ⊔ ℓ ⊔ c′) where
   _by_ : ∀ g → ι g ∙ x ≈ y → x ≋ y
 
 ≈⇒≋ : _≈_ ⇒ _≋_
-≈⇒≋ x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ _)
+≈⇒≋ x≈y = N.ε by G.trans (G.∙-cong ι.ε-homo x≈y) (G.identityˡ _)
 
-≋-refl : Reflexive _≋_
-≋-refl = ≈⇒≋ refl
+refl : Reflexive _≋_
+refl = ≈⇒≋ G.refl
 
-≋-sym : Symmetric _≋_
-≋-sym {x} {y} (g by ιg∙x≈y) = g N.⁻¹ by begin
-  ι (g N.⁻¹) ∙ y      ≈⟨ ∙-cong (ι.⁻¹-homo g) (sym ιg∙x≈y) ⟩
-  ι g ⁻¹ ∙ (ι g ∙ x)  ≈⟨ cancelˡ (inverseˡ (ι g)) x ⟩
+sym : Symmetric _≋_
+sym {x} {y} (g by ιg∙x≈y) = g N.⁻¹ by begin
+  ι (g N.⁻¹) ∙ y      ≈⟨ G.∙-cong (ι.⁻¹-homo g) (G.sym ιg∙x≈y) ⟩
+  ι g ⁻¹ ∙ (ι g ∙ x)  ≈⟨ cancelˡ (G.inverseˡ (ι g)) x ⟩
   x                   ∎
 
-≋-trans : Transitive _≋_
-≋-trans {x} {y} {z} (g by ιg∙x≈y) (h by ιh∙y≈z) = h N.∙ g by begin
-  ι (h N.∙ g) ∙ x ≈⟨ ∙-congʳ (ι.∙-homo h g) ⟩
+trans : Transitive _≋_
+trans {x} {y} {z} (g by ιg∙x≈y) (h by ιh∙y≈z) = h N.∙ g by begin
+  ι (h N.∙ g) ∙ x ≈⟨ G.∙-congʳ (ι.∙-homo h g) ⟩
   (ι h ∙ ι g) ∙ x ≈⟨ uv≈w⇒xu∙v≈xw ιg∙x≈y (ι h) ⟩
   ι h ∙ y         ≈⟨ ιh∙y≈z ⟩
   z               ∎
 
-≋-∙-cong : Congruent₂ _≋_ _∙_
-≋-∙-cong {x} {y} {u} {v} (g by ιg∙x≈y) (h by ιh∙u≈v) = g N.∙ h′ by begin
-  ι (g N.∙ h′) ∙ (x ∙ u) ≈⟨ ∙-congʳ (ι.∙-homo g h′) ⟩
+∙-cong : Congruent₂ _≋_ _∙_
+∙-cong {x} {y} {u} {v} (g by ιg∙x≈y) (h by ιh∙u≈v) = g N.∙ h′ by begin
+  ι (g N.∙ h′) ∙ (x ∙ u) ≈⟨ G.∙-congʳ (ι.∙-homo g h′) ⟩
   (ι g ∙ ι h′) ∙ (x ∙ u) ≈⟨ uv≈wx⇒yu∙vz≈yw∙xz (normal h x) (ι g) u ⟩
-  (ι g ∙ x) ∙ (ι h ∙ u)  ≈⟨ ∙-cong ιg∙x≈y ιh∙u≈v ⟩
+  (ι g ∙ x) ∙ (ι h ∙ u)  ≈⟨ G.∙-cong ιg∙x≈y ιh∙u≈v ⟩
   y ∙ v                  ∎
   where h′ = conjugate h x
 
-≋-⁻¹-cong : Congruent₁ _≋_ _⁻¹
-≋-⁻¹-cong {x} {y} (g by ιg∙x≈y) = h by begin
+⁻¹-cong : Congruent₁ _≋_ _⁻¹
+⁻¹-cong {x} {y} (g by ιg∙x≈y) = h by begin
   ι h ∙ x ⁻¹        ≈⟨ normal (g N.⁻¹) (x ⁻¹) ⟩
-  x ⁻¹ ∙ ι (g N.⁻¹) ≈⟨ ∙-congˡ (ι.⁻¹-homo g) ⟩
+  x ⁻¹ ∙ ι (g N.⁻¹) ≈⟨ G.∙-congˡ (ι.⁻¹-homo g) ⟩
   x ⁻¹ ∙ ι g ⁻¹     ≈⟨ ⁻¹-anti-homo-∙ (ι g) x ⟨
-  (ι g ∙ x) ⁻¹      ≈⟨ ⁻¹-cong ιg∙x≈y ⟩
+  (ι g ∙ x) ⁻¹      ≈⟨ G.⁻¹-cong ιg∙x≈y ⟩
   y ⁻¹              ∎
   where h = conjugate (g N.⁻¹) (x ⁻¹)
 
-quotientGroup : Group c (c ⊔ ℓ ⊔ c′)
-quotientGroup = record
+group : Group c (c ⊔ ℓ ⊔ c′)
+group = record
   { isGroup = record
     { isMonoid = record
       { isSemigroup = record
         { isMagma = record
           { isEquivalence = record
-            { refl = ≋-refl
-            ; sym = ≋-sym
-            ; trans = ≋-trans
+            { refl = refl
+            ; sym = sym
+            ; trans = trans
             }
-          ; ∙-cong = ≋-∙-cong
+          ; ∙-cong = ∙-cong
           }
-        ; assoc = λ x y z → ≈⇒≋ (assoc x y z)
+        ; assoc = λ x y z → ≈⇒≋ (G.assoc x y z)
         }
-      ; identity = ≈⇒≋ ∘ identityˡ , ≈⇒≋ ∘ identityʳ
+      ; identity = ≈⇒≋ ∘ G.identityˡ , ≈⇒≋ ∘ G.identityʳ
       }
-    ; inverse = ≈⇒≋ ∘ inverseˡ , ≈⇒≋ ∘ inverseʳ
-    ; ⁻¹-cong = ≋-⁻¹-cong
+    ; inverse = ≈⇒≋ ∘ G.inverseˡ , ≈⇒≋ ∘ G.inverseʳ
+    ; ⁻¹-cong = ⁻¹-cong
     }
   }
 
-_/_ : Group c (c ⊔ ℓ ⊔ c′)
-_/_ = quotientGroup
+private module Q = Group group
 
-π : Group.Carrier G → Group.Carrier quotientGroup
-π x = x -- because we do all the work in the relation
+-- Public re-exports
 
-π-isMagmaHomomorphism : IsMagmaHomomorphism rawMagma (Group.rawMagma quotientGroup) π
-π-isMagmaHomomorphism = record
-  { isRelHomomorphism = record
-    { cong = ≈⇒≋
-    }
-  ; homo = λ _ _ → ≋-refl
-  }
+_/_ : Group c (c ⊔ ℓ ⊔ c′)
+_/_ = group
 
-π-isMonoidHomomorphism : IsMonoidHomomorphism rawMonoid (Group.rawMonoid quotientGroup) π
-π-isMonoidHomomorphism = record
-  { isMagmaHomomorphism = π-isMagmaHomomorphism
-  ; ε-homo = ≋-refl
-  }
+π : G.Carrier → Q.Carrier
+π x = x -- because we do all the work in the relation _≋_
 
-π-isGroupHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) π
+π-surjective : Surjective _≈_ _≋_ π
+π-surjective g = g , ≈⇒≋
+
+π-isGroupHomomorphism : IsGroupHomomorphism G.rawGroup Q.rawGroup π
 π-isGroupHomomorphism = record
-  { isMonoidHomomorphism = π-isMonoidHomomorphism
-  ; ⁻¹-homo = λ _ → ≋-refl
+  { isMonoidHomomorphism = record
+    { isMagmaHomomorphism = record
+      { isRelHomomorphism = record
+        { cong = ≈⇒≋
+        }
+      ; homo = λ _ _ → refl
+      }
+    ; ε-homo = refl
+    }
+  ; ⁻¹-homo = λ _ → refl
   }
 
-π-surjective : Surjective _≈_ _≋_ π
-π-surjective g = g , ≈⇒≋
+open IsGroupHomomorphism π-isGroupHomomorphism public
+  using ()
+  renaming (isMonoidHomomorphism to π-isMonoidHomomorphism
+           ; isMagmaHomomorphism to π-isMagmaHomomorphism
+           )
diff --git a/src/Algebra/Construct/Quotient/Ring.agda b/src/Algebra/Construct/Quotient/Ring.agda
index 574f68c5ff..6384fd0b27 100644
--- a/src/Algebra/Construct/Quotient/Ring.agda
+++ b/src/Algebra/Construct/Quotient/Ring.agda
@@ -6,20 +6,20 @@
 
 {-# OPTIONS --safe --cubical-compatible #-}
 
-open import Algebra.Bundles using (AbelianGroup; Ring; RawRing)
+open import Algebra.Bundles using (AbelianGroup; Ring)
 open import Algebra.Construct.Sub.Ring.Ideal using (Ideal)
+import Algebra.Construct.Quotient.AbelianGroup as Quotient
 
 module Algebra.Construct.Quotient.Ring
   {c ℓ} (R : Ring c ℓ) {c′ ℓ′} (I : Ideal R c′ ℓ′)
   where
 
+open import Algebra.Definitions using (Congruent₂)
 open import Algebra.Morphism.Structures using (IsRingHomomorphism)
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘_)
 open import Level using (_⊔_)
 
-import Algebra.Construct.Quotient.AbelianGroup as Quotient
-
 private
   module R = Ring R
   module I = Ideal I
@@ -27,50 +27,51 @@ private
 
 
 open R/I public
-  using (_≋_; _by_; ≋-refl; ≈⇒≋
-        ; quotientAbelianGroup
-        ; π; π-isMonoidHomomorphism; π-surjective
-        )
-
-open import Algebra.Definitions _≋_ using (Congruent₂)
+  using (_≋_; _by_; ≈⇒≋; π; π-isMonoidHomomorphism; π-surjective)
+  renaming (abelianGroup to +-abelianGroup)
 
-≋-*-cong : Congruent₂ R._*_
-≋-*-cong {x} {y} {u} {v} (j by ιj+x≈y) (k by ιk+u≈v) = ι j *ₗ k +ᴹ j *ᵣ u +ᴹ x *ₗ k by begin
+*-cong : Congruent₂ _≋_ R._*_
+*-cong {x} {y} {u} {v} (j by ιj+x≈y) (k by ιk+u≈v) =
+  ι j *ₗ k +ᴹ j *ᵣ u +ᴹ x *ₗ k by begin
   ι (ι j *ₗ k +ᴹ j *ᵣ u +ᴹ x *ₗ k) + x * u       ≈⟨ +-congʳ (ι.+ᴹ-homo (ι j *ₗ k +ᴹ j *ᵣ u) (x *ₗ k)) ⟩
   ι (ι j *ₗ k +ᴹ j *ᵣ u) + ι (x *ₗ k) + x * u    ≈⟨ +-congʳ (+-congʳ (ι.+ᴹ-homo (ι j *ₗ k) (j *ᵣ u))) ⟩
   ι (ι j *ₗ k) + ι (j *ᵣ u) + ι (x *ₗ k) + x * u ≈⟨ +-congʳ (+-cong (+-cong (ι.*ₗ-homo (ι j) k) (ι.*ᵣ-homo u j)) (ι.*ₗ-homo x k)) ⟩
   ι j * ι k + ι j * u + x * ι k + x * u          ≈⟨ binomial-expansion (ι j) x (ι k) u ⟨
-  (ι j + x) * (ι k + u)                          ≈⟨ *-cong ιj+x≈y ιk+u≈v ⟩
+  (ι j + x) * (ι k + u)                          ≈⟨ R.*-cong ιj+x≈y ιk+u≈v ⟩
   y * v                                          ∎
   where
-  open R using (_+_; _*_; +-congʳ ;+-cong; *-cong)
+  open R using (_+_; _*_; +-congʳ ;+-cong)
   open import Algebra.Properties.Semiring R.semiring using (binomial-expansion)
   open import Relation.Binary.Reasoning.Setoid R.setoid
   open I using (ι; _*ₗ_; _*ᵣ_; _+ᴹ_)
 
-quotientRawRing : RawRing c (c ⊔ ℓ ⊔ c′)
-quotientRawRing = record { RawRing R.rawRing hiding (_≈_) ; _≈_ = _≋_ }
-
-quotientRing : Ring c (c ⊔ ℓ ⊔ c′)
-quotientRing = record
+ring : Ring c (c ⊔ ℓ ⊔ c′)
+ring = record
   { isRing = record
     { +-isAbelianGroup = isAbelianGroup
-    ; *-cong = ≋-*-cong
+    ; *-cong = *-cong
     ; *-assoc = λ x y z → ≈⇒≋ (R.*-assoc x y z)
     ; *-identity = ≈⇒≋ ∘ R.*-identityˡ , ≈⇒≋ ∘ R.*-identityʳ
     ; distrib = (λ x y z → ≈⇒≋ (R.distribˡ x y z)) , (λ x y z → ≈⇒≋ (R.distribʳ x y z))
     }
-  } where open AbelianGroup quotientAbelianGroup using (isAbelianGroup)
+  } where open AbelianGroup +-abelianGroup using (isAbelianGroup)
+
+private module Q = Ring ring
+
+-- Public re-exports
+
+_/_ : Ring c (c ⊔ ℓ ⊔ c′)
+_/_ = ring
 
-π-isRingHomomorphism : IsRingHomomorphism R.rawRing quotientRawRing π
+π-isRingHomomorphism : IsRingHomomorphism R.rawRing Q.rawRing π
 π-isRingHomomorphism = record
   { isSemiringHomomorphism = record
     { isNearSemiringHomomorphism = record
       { +-isMonoidHomomorphism = π-isMonoidHomomorphism
-      ; *-homo = λ _ _ → ≋-refl
+      ; *-homo = λ _ _ → Q.refl
       }
-    ; 1#-homo = ≋-refl
+    ; 1#-homo = Q.refl
     }
-  ; -‿homo = λ _ → ≋-refl
+  ; -‿homo = λ _ → Q.refl
   }
 

From 6778d542966fc18005bbd8e6681045b58f4d9703 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 9 Nov 2025 19:03:32 +0000
Subject: [PATCH 14/15] refactor: more on `Group`

---
 src/Algebra/Construct/Quotient/Group.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda
index 7d06d200cc..69bbf0af10 100644
--- a/src/Algebra/Construct/Quotient/Group.agda
+++ b/src/Algebra/Construct/Quotient/Group.agda
@@ -114,11 +114,11 @@ _/_ = group
       { isRelHomomorphism = record
         { cong = ≈⇒≋
         }
-      ; homo = λ _ _ → refl
+      ; homo = λ _ _ → Q.refl
       }
-    ; ε-homo = refl
+    ; ε-homo = Q.refl
     }
-  ; ⁻¹-homo = λ _ → refl
+  ; ⁻¹-homo = λ _ → Q.refl
   }
 
 open IsGroupHomomorphism π-isGroupHomomorphism public

From 08560e2de00e6f2e06cafb73e5de3a9b7056ed2b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 9 Nov 2025 22:17:14 +0000
Subject: [PATCH 15/15] update: `CHANGELOG`

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 403d274c0c..6e4cb30764 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -79,7 +79,7 @@ Deprecated names
 New modules
 -----------
 
-* `Algebra.Construct.Quotient.{Abelian}Group` for the definition of quotient (Abelian) groups.
+* `Algebra.Construct.Quotient.{{Abelian}Group|Ring}` for the definition of quotient (Abelian) groups and rings.
 
 * `Algebra.Construct.Sub.{Abelian}Group` for the definition of sub-(Abelian)groups.