diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6679049fd0..6e4cb30764 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -79,6 +79,16 @@ Deprecated names
 New modules
 -----------
 
+* `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.
+
+* `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`.
 
 * `Algebra.Properties.BooleanSemiring`.
diff --git a/src/Algebra/Construct/Quotient/AbelianGroup.agda b/src/Algebra/Construct/Quotient/AbelianGroup.agda
new file mode 100644
index 0000000000..9740242f01
--- /dev/null
+++ b/src/Algebra/Construct/Quotient/AbelianGroup.agda
@@ -0,0 +1,39 @@
+------------------------------------------------------------------------
+-- 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
+import Algebra.Construct.Quotient.Group as Quotient
+
+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 Quotient G.group (normalSubgroup N) public
+  hiding (_/_)
+
+-- With its additional bundle
+
+abelianGroup : AbelianGroup c _
+abelianGroup = record
+  { isAbelianGroup = record
+    { isGroup = isGroup
+    ; comm = λ g h → ≈⇒≋ (G.comm g h)
+    }
+  } where open Group group
+
+-- Public re-exports
+
+_/_ = abelianGroup
diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda
new file mode 100644
index 0000000000..69bbf0af10
--- /dev/null
+++ b/src/Algebra/Construct/Quotient/Group.agda
@@ -0,0 +1,128 @@
+------------------------------------------------------------------------
+-- 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 (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
+    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 : G.Carrier) : Set (c ⊔ ℓ ⊔ c′) where
+  _by_ : ∀ g → ι g ∙ x ≈ y → x ≋ y
+
+≈⇒≋ : _≈_ ⇒ _≋_
+≈⇒≋ x≈y = N.ε by G.trans (G.∙-cong ι.ε-homo x≈y) (G.identityˡ _)
+
+refl : Reflexive _≋_
+refl = ≈⇒≋ G.refl
+
+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 ≈⟨ 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) ≈⟨ G.∙-congʳ (ι.∙-homo g h′) ⟩
+  (ι g ∙ ι h′) ∙ (x ∙ u) ≈⟨ uv≈wx⇒yu∙vz≈yw∙xz (normal h x) (ι g) u ⟩
+  (ι 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
+  ι h ∙ x ⁻¹        ≈⟨ normal (g N.⁻¹) (x ⁻¹) ⟩
+  x ⁻¹ ∙ ι (g N.⁻¹) ≈⟨ G.∙-congˡ (ι.⁻¹-homo g) ⟩
+  x ⁻¹ ∙ ι g ⁻¹     ≈⟨ ⁻¹-anti-homo-∙ (ι g) x ⟨
+  (ι g ∙ x) ⁻¹      ≈⟨ G.⁻¹-cong ιg∙x≈y ⟩
+  y ⁻¹              ∎
+  where h = conjugate (g N.⁻¹) (x ⁻¹)
+
+group : Group c (c ⊔ ℓ ⊔ c′)
+group = record
+  { isGroup = record
+    { isMonoid = record
+      { isSemigroup = record
+        { isMagma = record
+          { isEquivalence = record
+            { refl = refl
+            ; sym = sym
+            ; trans = trans
+            }
+          ; ∙-cong = ∙-cong
+          }
+        ; assoc = λ x y z → ≈⇒≋ (G.assoc x y z)
+        }
+      ; identity = ≈⇒≋ ∘ G.identityˡ , ≈⇒≋ ∘ G.identityʳ
+      }
+    ; inverse = ≈⇒≋ ∘ G.inverseˡ , ≈⇒≋ ∘ G.inverseʳ
+    ; ⁻¹-cong = ⁻¹-cong
+    }
+  }
+
+private module Q = Group group
+
+-- Public re-exports
+
+_/_ : Group c (c ⊔ ℓ ⊔ c′)
+_/_ = group
+
+π : G.Carrier → Q.Carrier
+π x = x -- because we do all the work in the relation _≋_
+
+π-surjective : Surjective _≈_ _≋_ π
+π-surjective g = g , ≈⇒≋
+
+π-isGroupHomomorphism : IsGroupHomomorphism G.rawGroup Q.rawGroup π
+π-isGroupHomomorphism = record
+  { isMonoidHomomorphism = record
+    { isMagmaHomomorphism = record
+      { isRelHomomorphism = record
+        { cong = ≈⇒≋
+        }
+      ; homo = λ _ _ → Q.refl
+      }
+    ; ε-homo = Q.refl
+    }
+  ; ⁻¹-homo = λ _ → Q.refl
+  }
+
+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
new file mode 100644
index 0000000000..6384fd0b27
--- /dev/null
+++ b/src/Algebra/Construct/Quotient/Ring.agda
@@ -0,0 +1,77 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Quotient rings
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+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 (_⊔_)
+
+private
+  module R = Ring R
+  module I = Ideal I
+  module R/I = Quotient R.+-abelianGroup I.subgroup
+
+
+open R/I public
+  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
+  ι (ι 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)                          ≈⟨ R.*-cong ιj+x≈y ιk+u≈v ⟩
+  y * v                                          ∎
+  where
+  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 (ι; _*ₗ_; _*ᵣ_; _+ᴹ_)
+
+ring : Ring c (c ⊔ ℓ ⊔ c′)
+ring = 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 +-abelianGroup using (isAbelianGroup)
+
+private module Q = Ring ring
+
+-- Public re-exports
+
+_/_ : Ring c (c ⊔ ℓ ⊔ c′)
+_/_ = ring
+
+π-isRingHomomorphism : IsRingHomomorphism R.rawRing Q.rawRing π
+π-isRingHomomorphism = record
+  { isSemiringHomomorphism = record
+    { isNearSemiringHomomorphism = record
+      { +-isMonoidHomomorphism = π-isMonoidHomomorphism
+      ; *-homo = λ _ _ → Q.refl
+      }
+    ; 1#-homo = Q.refl
+    }
+  ; -‿homo = λ _ → Q.refl
+  }
+
diff --git a/src/Algebra/Construct/Sub/AbelianGroup.agda b/src/Algebra/Construct/Sub/AbelianGroup.agda
new file mode 100644
index 0000000000..90a93debe4
--- /dev/null
+++ b/src/Algebra/Construct/Sub/AbelianGroup.agda
@@ -0,0 +1,78 @@
+------------------------------------------------------------------------
+-- 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 #-}
+
+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)
+
+-- 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 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)
+
+-- 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.agda b/src/Algebra/Construct/Sub/Group.agda
new file mode 100644
index 0000000000..550f0689db
--- /dev/null
+++ b/src/Algebra/Construct/Sub/Group.agda
@@ -0,0 +1,101 @@
+------------------------------------------------------------------------
+-- 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 #-}
+
+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
+
+------------------------------------------------------------------------
+-- 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, the following name is essentially arbitrary, existing
+-- solely to be mentioned in the third field `ι-monomorphism` below.
+
+    domain         : RawGroup c′ ℓ′
+
+-- 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 (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`.
+
+-- 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 (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:
+
+    ι-monomorphism : IsGroupMonomorphism domain G.rawGroup ι
+
+-- 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
+
+-- 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 }
+
+  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..41dff5e76b
--- /dev/null
+++ b/src/Algebra/Construct/Sub/Group/Normal.agda
@@ -0,0 +1,97 @@
+------------------------------------------------------------------------
+-- 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
+
+------------------------------------------------------------------------
+-- 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
+
+-- 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`? Or is that itself too
+-- 'occult' a usage?
+
+    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
+
+-- 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.
diff --git a/src/Algebra/Construct/Sub/Ring/Ideal.agda b/src/Algebra/Construct/Sub/Ring/Ideal.agda
new file mode 100644
index 0000000000..2bae176ace
--- /dev/null
+++ b/src/Algebra/Construct/Sub/Ring/Ideal.agda
@@ -0,0 +1,40 @@
+------------------------------------------------------------------------
+-- 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`,
+-- notwithstanding that we have yet to define `Sub.XRing`s...
+
+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 using (suc; _⊔_)
+
+------------------------------------------------------------------------
+-- Definition
+--
+-- 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
new file mode 100644
index 0000000000..d270d3ed2c
--- /dev/null
+++ b/src/Algebra/Module/Construct/Sub/Bimodule.agda
@@ -0,0 +1,81 @@
+------------------------------------------------------------------------
+-- 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,
+-- 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 based.
+------------------------------------------------------------------------
+
+{-# 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′
+
+-- 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 _ _
+  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 }
+
+-- 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