diff --git a/CHANGELOG.md b/CHANGELOG.md
index 381bd0eb9c..4181d2f342 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -155,6 +155,8 @@ New modules
 
 * `Algebra.Module.Properties.{Bimodule|LeftModule|RightModule}`.
 
+* `Algebra.Morphism.Construct.DirectProduct`.
+
 * `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`.
 
 * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.
diff --git a/src/Algebra/Morphism/Construct/DirectProduct.agda b/src/Algebra/Morphism/Construct/DirectProduct.agda
new file mode 100644
index 0000000000..4c69593499
--- /dev/null
+++ b/src/Algebra/Morphism/Construct/DirectProduct.agda
@@ -0,0 +1,142 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The projection morphisms for algebraic structures arising from the
+-- direct product construction
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+module Algebra.Morphism.Construct.DirectProduct where
+
+open import Algebra.Bundles using (RawMagma; RawMonoid)
+open import Algebra.Construct.DirectProduct using (rawMagma; rawMonoid)
+open import Algebra.Morphism.Structures
+  using ( module MagmaMorphisms
+        ; module MonoidMorphisms
+        )
+open import Data.Product as Product
+  using (_,_)
+open import Level using (Level)
+open import Relation.Binary.Definitions using (Reflexive)
+import Relation.Binary.Morphism.Construct.Product as RP
+
+private
+  variable
+    a b c ℓ₁ ℓ₂ ℓ₃ : Level
+
+------------------------------------------------------------------------
+-- Magmas
+
+module Magma (M : RawMagma a ℓ₁) (N : RawMagma b ℓ₂) where
+  open MagmaMorphisms
+
+  private
+    module M = RawMagma M
+    module N = RawMagma N
+
+  module Proj₁ (refl : Reflexive M._≈_) where
+
+    isMagmaHomomorphism : IsMagmaHomomorphism (rawMagma M N) M Product.proj₁
+    isMagmaHomomorphism = record
+      { isRelHomomorphism = RP.proj₁
+      ; homo              = λ _ _ → refl
+      }
+
+  module Proj₂ (refl : Reflexive N._≈_) where
+
+    isMagmaHomomorphism : IsMagmaHomomorphism (rawMagma M N) N Product.proj₂
+    isMagmaHomomorphism = record
+      { isRelHomomorphism = RP.proj₂
+      ; homo              = λ _ _ → refl
+      }
+
+  module Pair (P : RawMagma c ℓ₃) where
+
+    isMagmaHomomorphism : ∀ {f g} →
+                          IsMagmaHomomorphism P M f →
+                          IsMagmaHomomorphism P N g →
+                          IsMagmaHomomorphism P (rawMagma M N) (Product.< f , g >)
+    isMagmaHomomorphism F G = record
+      { isRelHomomorphism = RP.< F.isRelHomomorphism , G.isRelHomomorphism >
+      ; homo              = λ x y → F.homo x y , G.homo x y
+      }
+      where
+        module F = IsMagmaHomomorphism F
+        module G = IsMagmaHomomorphism G
+
+-- Package for export
+module Magma-Export {M : RawMagma a ℓ₁} {N : RawMagma b ℓ₂} where
+  open Magma
+
+  private
+    module M = RawMagma M
+    module N = RawMagma N
+
+  module _ {refl : Reflexive M._≈_} where
+    proj₁ = Proj₁.isMagmaHomomorphism M M refl
+
+  module _ {refl : Reflexive N._≈_} where
+    proj₂ = Proj₂.isMagmaHomomorphism M N refl
+
+  module _ {P : RawMagma c ℓ₃} where
+    <_,_> = Pair.isMagmaHomomorphism M N P
+
+------------------------------------------------------------------------
+-- Monoids
+
+module Monoid (M : RawMonoid a ℓ₁) (N : RawMonoid b ℓ₂) where
+  open MonoidMorphisms
+
+  private
+    module M = RawMonoid M
+    module N = RawMonoid N
+
+  module Proj₁ (refl : Reflexive M._≈_) where
+
+    isMonoidHomomorphism : IsMonoidHomomorphism (rawMonoid M N) M Product.proj₁
+    isMonoidHomomorphism = record
+      { isMagmaHomomorphism = Magma.Proj₁.isMagmaHomomorphism M.rawMagma N.rawMagma refl
+      ; ε-homo              = refl
+      }
+
+  module Proj₂ (refl : Reflexive N._≈_) where
+
+    isMonoidHomomorphism : IsMonoidHomomorphism (rawMonoid M N) N Product.proj₂
+    isMonoidHomomorphism = record
+      { isMagmaHomomorphism = Magma.Proj₂.isMagmaHomomorphism M.rawMagma N.rawMagma refl
+      ; ε-homo              = refl
+      }
+
+  module Pair (P : RawMonoid c ℓ₃) where
+
+    private
+      module P = RawMonoid P
+
+    isMonoidHomomorphism : ∀ {f g} →
+                          IsMonoidHomomorphism P M f →
+                          IsMonoidHomomorphism P N g →
+                          IsMonoidHomomorphism P (rawMonoid M N) (Product.< f , g >)
+    isMonoidHomomorphism F G = record
+      { isMagmaHomomorphism = Magma.Pair.isMagmaHomomorphism M.rawMagma N.rawMagma P.rawMagma F.isMagmaHomomorphism G.isMagmaHomomorphism
+      ; ε-homo              = F.ε-homo , G.ε-homo }
+      where
+        module F = IsMonoidHomomorphism F
+        module G = IsMonoidHomomorphism G
+
+-- Package for export
+module Monoid-Export {M : RawMonoid a ℓ₁} {N : RawMonoid b ℓ₂} where
+  open Monoid
+
+  private
+    module M = RawMonoid M
+    module N = RawMonoid N
+
+  module _ {refl : Reflexive M._≈_} where
+    proj₁ = Proj₁.isMonoidHomomorphism M M refl
+
+  module _ {refl : Reflexive N._≈_} where
+    proj₂ = Proj₂.isMonoidHomomorphism M N refl
+
+  module _ {P : RawMonoid c ℓ₃} where
+    <_,_> = Pair.isMonoidHomomorphism M N P