diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0cdb36f8c6..486778805c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -605,6 +605,8 @@ Non-backwards compatible changes
 
 * New modules:
   ```
+  Algebra.Construct.Initial
+  Algebra.Construct.Terminal
   Data.List.Effectful.Transformer
   Data.List.NonEmpty.Effectful.Transformer
   Data.Maybe.Effectful.Transformer
@@ -870,6 +872,14 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Algebra.Construct.Zero`:
+  ```agda
+  rawMagma   ↦  Algebra.Construct.Terminal.rawMagma
+  magma      ↦  Algebra.Construct.Terminal.magma
+  semigroup  ↦  Algebra.Construct.Terminal.semigroup
+  band       ↦  Algebra.Construct.Terminal.band
+  ```
+
 * In `Codata.Guarded.Stream.Properties`:
   ```agda
   map-identity  ↦  map-id
diff --git a/src/Algebra/Construct/Initial.agda b/src/Algebra/Construct/Initial.agda
new file mode 100644
index 0000000000..7851eb1b62
--- /dev/null
+++ b/src/Algebra/Construct/Initial.agda
@@ -0,0 +1,97 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances of algebraic structures where the carrier is ⊥.
+-- In mathematics, this is usually called 0.
+--
+-- From monoids up, these are zero-objects – i.e, the initial
+-- object is the terminal object in the relevant category.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Algebra.Construct.Initial {c ℓ : Level} where
+
+open import Algebra.Bundles
+  using (Magma; Semigroup; Band)
+open import Algebra.Bundles.Raw
+  using (RawMagma)
+open import Algebra.Core using (Op₂)
+open import Algebra.Definitions using (Congruent₂)
+open import Algebra.Structures using (IsMagma; IsSemigroup; IsBand)
+open import Data.Empty.Polymorphic
+open import Relation.Binary using (Rel; Reflexive; Symmetric; Transitive; IsEquivalence)
+
+
+------------------------------------------------------------------------
+-- Re-export those algebras which are also terminal
+
+open import Algebra.Construct.Terminal {c} {ℓ} public
+  hiding (rawMagma; magma; semigroup; band)
+
+------------------------------------------------------------------------
+-- Gather all the functionality in one place
+
+module ℤero where
+
+  infixl 7 _∙_
+  infix  4 _≈_
+
+  Carrier : Set c
+  Carrier = ⊥
+
+  _≈_     : Rel Carrier ℓ
+  _≈_ ()
+
+  _∙_     : Op₂ Carrier
+  _∙_ ()
+
+  refl : Reflexive _≈_
+  refl {x = ()}
+
+  sym : Symmetric _≈_
+  sym {x = ()}
+
+  trans : Transitive _≈_
+  trans {i = ()}
+
+  ∙-cong : Congruent₂ _≈_ _∙_
+  ∙-cong {x = ()}
+
+open ℤero
+
+------------------------------------------------------------------------
+-- Raw bundles
+
+rawMagma : RawMagma c ℓ
+rawMagma = record { ℤero }
+
+------------------------------------------------------------------------
+-- Structures
+
+isEquivalence : IsEquivalence _≈_
+isEquivalence = record { ℤero }
+
+isMagma : IsMagma _≈_ _∙_
+isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong }
+
+isSemigroup : IsSemigroup _≈_ _∙_
+isSemigroup = record { isMagma = isMagma ; assoc = λ () }
+
+isBand : IsBand _≈_ _∙_
+isBand = record { isSemigroup = isSemigroup ; idem = λ () }
+
+------------------------------------------------------------------------
+-- Bundles
+
+magma : Magma c ℓ
+magma = record { isMagma = isMagma }
+
+semigroup : Semigroup c ℓ
+semigroup = record { isSemigroup = isSemigroup }
+
+band : Band c ℓ
+band = record { isBand = isBand }
+
diff --git a/src/Algebra/Construct/Terminal.agda b/src/Algebra/Construct/Terminal.agda
new file mode 100644
index 0000000000..f914a010b5
--- /dev/null
+++ b/src/Algebra/Construct/Terminal.agda
@@ -0,0 +1,86 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances of algebraic structures where the carrier is ⊤.
+-- In mathematics, this is usually called 0 (1 in the case of Group).
+--
+-- From monoids up, these are zero-objects – i.e, both the initial
+-- and the terminal object in the relevant category.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Algebra.Construct.Terminal {c ℓ : Level} where
+
+open import Algebra.Bundles
+open import Data.Unit.Polymorphic
+open import Relation.Binary.Core using (Rel)
+
+------------------------------------------------------------------------
+-- Gather all the functionality in one place
+
+module 𝕆ne where
+
+  infix  4 _≈_
+  Carrier : Set c
+  Carrier = ⊤
+
+  _≈_     : Rel Carrier ℓ
+  _ ≈ _ = ⊤
+
+------------------------------------------------------------------------
+-- Raw bundles
+
+rawMagma : RawMagma c ℓ
+rawMagma = record { 𝕆ne }
+
+rawMonoid : RawMonoid c ℓ
+rawMonoid = record { 𝕆ne }
+
+rawGroup : RawGroup c ℓ
+rawGroup = record { 𝕆ne }
+
+rawSemiring : RawSemiring c ℓ
+rawSemiring = record { 𝕆ne }
+
+rawRing : RawRing c ℓ
+rawRing = record { 𝕆ne }
+
+------------------------------------------------------------------------
+-- Bundles
+
+magma : Magma c ℓ
+magma = record { 𝕆ne }
+
+semigroup : Semigroup c ℓ
+semigroup = record { 𝕆ne }
+
+band : Band c ℓ
+band = record { 𝕆ne }
+
+commutativeSemigroup : CommutativeSemigroup c ℓ
+commutativeSemigroup = record { 𝕆ne }
+
+monoid : Monoid c ℓ
+monoid = record { 𝕆ne }
+
+commutativeMonoid : CommutativeMonoid c ℓ
+commutativeMonoid = record { 𝕆ne }
+
+idempotentCommutativeMonoid : IdempotentCommutativeMonoid c ℓ
+idempotentCommutativeMonoid = record { 𝕆ne }
+
+group : Group c ℓ
+group = record { 𝕆ne }
+
+abelianGroup : AbelianGroup c ℓ
+abelianGroup = record { 𝕆ne }
+
+semiring : Semiring c ℓ
+semiring = record { 𝕆ne }
+
+ring : Ring c ℓ
+ring = record { 𝕆ne }
+
diff --git a/src/Algebra/Construct/Zero.agda b/src/Algebra/Construct/Zero.agda
index 12f5c87ffe..dccfd9d0c6 100644
--- a/src/Algebra/Construct/Zero.agda
+++ b/src/Algebra/Construct/Zero.agda
@@ -2,13 +2,15 @@
 -- The Agda standard library
 --
 -- Instances of algebraic structures where the carrier is ⊤.
--- In mathematics, this is usually called 0.
+-- In mathematics, this is usually called 0 (1 in the case of Group).
 --
 -- From monoids up, these are are zero-objects – i.e, both the initial
 -- and the terminal object in the relevant category.
--- For structures without an identity element, we can't necessarily
--- produce a homomorphism out of 0, because there is an instance of such
--- a structure with an empty Carrier.
+--
+-- For structures without an identity element, the terminal algebra is
+-- *not*  initial, because there is an instance of such a structure
+-- with an empty Carrier. Accordingly, such definitions are now deprecated
+-- in favour of those defined in `Algebra.Construct.Terminal`.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
@@ -17,47 +19,51 @@ open import Level using (Level)
 
 module Algebra.Construct.Zero {c ℓ : Level} where
 
+open import Algebra.Bundles.Raw
+  using (RawMagma)
 open import Algebra.Bundles
-open import Data.Unit.Polymorphic
+  using (Magma; Semigroup; Band)
 
 ------------------------------------------------------------------------
--- Raw bundles
+-- Re-export those algebras which are both initial and terminal
 
-rawMagma : RawMagma c ℓ
-rawMagma = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
+open import Algebra.Construct.Terminal public
+  hiding (rawMagma; magma; semigroup; band)
 
-rawMonoid : RawMonoid c ℓ
-rawMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new definitions re-exported from
+-- `Algebra.Construct.Terminal` as continuing support for the below is
+-- not guaranteed.
 
-rawGroup : RawGroup c ℓ
-rawGroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
+-- Version 2.0
 
-------------------------------------------------------------------------
--- Bundles
+rawMagma : RawMagma c ℓ
+rawMagma = Algebra.Construct.Terminal.rawMagma
+
+{-# WARNING_ON_USAGE rawMagma
+"Warning: rawMagma was deprecated in v2.0.
+Please use Algebra.Construct.Terminal.rawMagma instead."
+#-}
 
 magma : Magma c ℓ
-magma = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
+magma = Algebra.Construct.Terminal.magma
+{-# WARNING_ON_USAGE magma
+"Warning: magma was deprecated in v2.0.
+Please use Algebra.Construct.Terminal.magma instead."
+#-}
 
 semigroup : Semigroup c ℓ
-semigroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
+semigroup = Algebra.Construct.Terminal.semigroup
+{-# WARNING_ON_USAGE semigroup
+"Warning: semigroup was deprecated in v2.0.
+Please use Algebra.Construct.Terminal.semigroup instead."
+#-}
 
 band : Band c ℓ
-band = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
-
-commutativeSemigroup : CommutativeSemigroup c ℓ
-commutativeSemigroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
-
-monoid : Monoid c ℓ
-monoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
-
-commutativeMonoid : CommutativeMonoid c ℓ
-commutativeMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
-
-idempotentCommutativeMonoid : IdempotentCommutativeMonoid c ℓ
-idempotentCommutativeMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
-
-group : Group c ℓ
-group = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
-
-abelianGroup : AbelianGroup c ℓ
-abelianGroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
+band = Algebra.Construct.Terminal.band
+{-# WARNING_ON_USAGE semigroup
+"Warning: semigroup was deprecated in v2.0.
+Please use Algebra.Construct.Terminal.semigroup instead."
+#-}
diff --git a/src/Algebra/Module/Construct/Zero.agda b/src/Algebra/Module/Construct/Zero.agda
index ada60892c5..ae5e3e7df3 100644
--- a/src/Algebra/Module/Construct/Zero.agda
+++ b/src/Algebra/Module/Construct/Zero.agda
@@ -17,56 +17,56 @@ module Algebra.Module.Construct.Zero {c ℓ : Level} where
 open import Algebra.Bundles
 open import Algebra.Module.Bundles
 open import Data.Unit.Polymorphic
+open import Relation.Binary.Core using (Rel)
 
 private
   variable
     r s ℓr ℓs : Level
 
+------------------------------------------------------------------------
+-- gather all the functionality in one place
+
+module ℤero where
+
+  infix  4 _≈ᴹ_
+  Carrierᴹ : Set c
+  Carrierᴹ = ⊤
+
+  _≈ᴹ_     : Rel Carrierᴹ ℓ
+  _ ≈ᴹ _ = ⊤
+
+open ℤero
+
+------------------------------------------------------------------------
+-- Raw bundles NOT YET IMPLEMENTED issue #1828
+{-
+rawModule : RawModule c ℓ
+rawModule = record { ℤero }
+-}
+------------------------------------------------------------------------
+-- Bundles
+
 leftSemimodule : {R : Semiring r ℓr} → LeftSemimodule R c ℓ
-leftSemimodule = record
-  { Carrierᴹ = ⊤
-  ; _≈ᴹ_ = λ _ _ → ⊤
-  }
+leftSemimodule = record { ℤero }
 
 rightSemimodule : {S : Semiring s ℓs} → RightSemimodule S c ℓ
-rightSemimodule = record
-  { Carrierᴹ = ⊤
-  ; _≈ᴹ_ = λ _ _ → ⊤
-  }
+rightSemimodule = record { ℤero }
 
 bisemimodule :
   {R : Semiring r ℓr} {S : Semiring s ℓs} → Bisemimodule R S c ℓ
-bisemimodule = record
-  { Carrierᴹ = ⊤
-  ; _≈ᴹ_ = λ _ _ → ⊤
-  }
+bisemimodule = record { ℤero }
 
 semimodule : {R : CommutativeSemiring r ℓr} → Semimodule R c ℓ
-semimodule = record
-  { Carrierᴹ = ⊤
-  ; _≈ᴹ_ = λ _ _ → ⊤
-  }
+semimodule = record { ℤero }
 
 leftModule : {R : Ring r ℓr} → LeftModule R c ℓ
-leftModule = record
-  { Carrierᴹ = ⊤
-  ; _≈ᴹ_ = λ _ _ → ⊤
-  }
+leftModule = record { ℤero }
 
 rightModule : {S : Ring s ℓs} → RightModule S c ℓ
-rightModule = record
-  { Carrierᴹ = ⊤
-  ; _≈ᴹ_ = λ _ _ → ⊤
-  }
+rightModule = record { ℤero }
 
 bimodule : {R : Ring r ℓr} {S : Ring s ℓs} → Bimodule R S c ℓ
-bimodule = record
-  { Carrierᴹ = ⊤
-  ; _≈ᴹ_ = λ _ _ → ⊤
-  }
+bimodule = record { ℤero }
 
 ⟨module⟩ : {R : CommutativeRing r ℓr} → Module R c ℓ
-⟨module⟩ = record
-  { Carrierᴹ = ⊤
-  ; _≈ᴹ_ = λ _ _ → ⊤
-  }
+⟨module⟩ = record { ℤero }
diff --git a/src/Data/Unit.agda b/src/Data/Unit.agda
index fd03e9bcad..22a97b4af9 100644
--- a/src/Data/Unit.agda
+++ b/src/Data/Unit.agda
@@ -8,8 +8,6 @@
 
 module Data.Unit where
 
-import Relation.Binary.PropositionalEquality as PropEq
-
 ------------------------------------------------------------------------
 -- Re-export contents of base module
 
diff --git a/src/Data/Unit/Base.agda b/src/Data/Unit/Base.agda
index b30cd40d40..49ae91be88 100644
--- a/src/Data/Unit/Base.agda
+++ b/src/Data/Unit/Base.agda
@@ -6,8 +6,6 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-open import Agda.Builtin.Equality using (_≡_)
-
 module Data.Unit.Base where
 
 ------------------------------------------------------------------------