diff --git a/CHANGELOG.md b/CHANGELOG.md
index c690740a1e..97eb05989b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -33,9 +33,49 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures
+
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts.
+
+* In `Algebra.Module.Construct.DirectProduct`:
+  ```agda
+  rawLeftSemimodule  : RawLeftSemimodule R m ℓm → RawLeftSemimodule m′ ℓm′ → RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+  rawLeftModule      : RawLeftModule R m ℓm → RawLeftModule m′ ℓm′ → RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+  rawRightSemimodule : RawRightSemimodule R m ℓm → RawRightSemimodule m′ ℓm′ → RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+  rawRightModule     : RawRightModule R m ℓm → RawRightModule m′ ℓm′ → RawRightModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+  rawBisemimodule    : RawBisemimodule R m ℓm → RawBisemimodule m′ ℓm′ → RawBisemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+  rawBimodule        : RawBimodule R m ℓm → RawBimodule m′ ℓm′ → RawBimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+  rawSemimodule      : RawSemimodule R m ℓm → RawSemimodule m′ ℓm′ → RawSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+  rawModule          : RawModule R m ℓm → RawModule m′ ℓm′ → RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+  ```
+
+* In `Algebra.Module.Construct.TensorUnit`:
+  ```agda
+  rawLeftSemimodule  : RawLeftSemimodule _ c ℓ
+  rawLeftModule      : RawLeftModule _ c ℓ
+  rawRightSemimodule : RawRightSemimodule _ c ℓ
+  rawRightModule     : RawRightModule _ c ℓ
+  rawBisemimodule    : RawBisemimodule _ _ c ℓ
+  rawBimodule        : RawBimodule _ _ c ℓ
+  rawSemimodule      : RawSemimodule _ c ℓ
+  rawModule          : RawModule _ c ℓ
+  ```
+
+* In `Algebra.Module.Construct.Zero`:
+  ```agda
+  rawLeftSemimodule  : RawLeftSemimodule R c ℓ
+  rawLeftModule      : RawLeftModule R c ℓ
+  rawRightSemimodule : RawRightSemimodule R c ℓ
+  rawRightModule     : RawRightModule R c ℓ
+  rawBisemimodule    : RawBisemimodule R c ℓ
+  rawBimodule        : RawBimodule R c ℓ
+  rawSemimodule      : RawSemimodule R c ℓ
+  rawModule          : RawModule R c ℓ
+  ```
+
 * In `Data.Fin.Properties`:
   ```agda
   nonZeroIndex : Fin n → ℕ.NonZero n
diff --git a/src/Algebra/Module/Bundles.agda b/src/Algebra/Module/Bundles.agda
index f36e5bccd0..56b01fcf97 100644
--- a/src/Algebra/Module/Bundles.agda
+++ b/src/Algebra/Module/Bundles.agda
@@ -28,6 +28,7 @@ module Algebra.Module.Bundles where
 open import Algebra.Bundles
 open import Algebra.Core
 open import Algebra.Definitions using (Involutive)
+import Algebra.Module.Bundles.Raw as Raw
 open import Algebra.Module.Core
 open import Algebra.Module.Structures
 open import Algebra.Module.Definitions
@@ -42,6 +43,16 @@ private
   variable
     r ℓr s ℓs : Level
 
+------------------------------------------------------------------------
+-- Re-export definitions of 'raw' bundles
+
+open Raw public
+  using ( RawLeftSemimodule; RawLeftModule
+        ; RawRightSemimodule; RawRightModule
+        ; RawBisemimodule; RawBimodule
+        ; RawSemimodule; RawModule
+        )
+
 ------------------------------------------------------------------------
 -- Left modules
 ------------------------------------------------------------------------
@@ -62,10 +73,6 @@ record LeftSemimodule (semiring : Semiring r ℓr) m ℓm
     0ᴹ : Carrierᴹ
     isLeftSemimodule : IsLeftSemimodule semiring _≈ᴹ_ _+ᴹ_ 0ᴹ _*ₗ_
 
-  infix 4 _≉ᴹ_
-  _≉ᴹ_ : Rel Carrierᴹ _
-  a ≉ᴹ b = ¬ (a ≈ᴹ b)
-
   open IsLeftSemimodule isLeftSemimodule public
 
   +ᴹ-commutativeMonoid : CommutativeMonoid m ℓm
@@ -80,8 +87,17 @@ record LeftSemimodule (semiring : Semiring r ℓr) m ℓm
     ; magma     to +ᴹ-magma
     ; rawMagma  to +ᴹ-rawMagma
     ; rawMonoid to +ᴹ-rawMonoid
+    ; _≉_ to _≉ᴹ_
     )
 
+  rawLeftSemimodule : RawLeftSemimodule Carrier m ℓm
+  rawLeftSemimodule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ₗ_ = _*ₗ_
+    ; 0ᴹ = 0ᴹ
+    }
+
 record LeftModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
   open Ring ring
 
@@ -106,7 +122,7 @@ record LeftModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ 
 
   open LeftSemimodule leftSemimodule public
     using ( +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma
-          ; +ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_)
+          ; +ᴹ-rawMagma; +ᴹ-rawMonoid; rawLeftSemimodule; _≉ᴹ_)
 
   +ᴹ-abelianGroup : AbelianGroup m ℓm
   +ᴹ-abelianGroup = record { isAbelianGroup = +ᴹ-isAbelianGroup }
@@ -114,6 +130,15 @@ record LeftModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ 
   open AbelianGroup +ᴹ-abelianGroup public
     using () renaming (group to +ᴹ-group; rawGroup to +ᴹ-rawGroup)
 
+  rawLeftModule : RawLeftModule Carrier m ℓm
+  rawLeftModule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ₗ_ = _*ₗ_
+    ; 0ᴹ = 0ᴹ
+    ; -ᴹ_ = -ᴹ_
+    }
+
 ------------------------------------------------------------------------
 -- Right modules
 ------------------------------------------------------------------------
@@ -134,10 +159,6 @@ record RightSemimodule (semiring : Semiring r ℓr) m ℓm
     0ᴹ : Carrierᴹ
     isRightSemimodule : IsRightSemimodule semiring _≈ᴹ_ _+ᴹ_ 0ᴹ _*ᵣ_
 
-  infix 4 _≉ᴹ_
-  _≉ᴹ_ : Rel Carrierᴹ _
-  a ≉ᴹ b = ¬ (a ≈ᴹ b)
-
   open IsRightSemimodule isRightSemimodule public
 
   +ᴹ-commutativeMonoid : CommutativeMonoid m ℓm
@@ -152,8 +173,17 @@ record RightSemimodule (semiring : Semiring r ℓr) m ℓm
     ; magma     to +ᴹ-magma
     ; rawMagma  to +ᴹ-rawMagma
     ; rawMonoid to +ᴹ-rawMonoid
+    ; _≉_ to _≉ᴹ_
     )
 
+  rawRightSemimodule : RawRightSemimodule Carrier m ℓm
+  rawRightSemimodule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ᵣ_ = _*ᵣ_
+    ; 0ᴹ = 0ᴹ
+    }
+
 record RightModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
   open Ring ring
 
@@ -178,7 +208,7 @@ record RightModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔
 
   open RightSemimodule rightSemimodule public
     using ( +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma
-          ; +ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_)
+          ; +ᴹ-rawMagma; +ᴹ-rawMonoid; rawRightSemimodule; _≉ᴹ_)
 
   +ᴹ-abelianGroup : AbelianGroup m ℓm
   +ᴹ-abelianGroup = record { isAbelianGroup = +ᴹ-isAbelianGroup }
@@ -186,6 +216,15 @@ record RightModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔
   open AbelianGroup +ᴹ-abelianGroup public
     using () renaming (group to +ᴹ-group; rawGroup to +ᴹ-rawGroup)
 
+  rawRightModule : RawRightModule Carrier m ℓm
+  rawRightModule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ᵣ_ = _*ᵣ_
+    ; 0ᴹ = 0ᴹ
+    ; -ᴹ_ = -ᴹ_
+    }
+
 ------------------------------------------------------------------------
 -- Bimodules
 ------------------------------------------------------------------------
@@ -220,7 +259,19 @@ record Bisemimodule (R-semiring : Semiring r ℓr) (S-semiring : Semiring s ℓs
 
   open LeftSemimodule leftSemimodule public
     using ( +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma; +ᴹ-rawMagma
-          ; +ᴹ-rawMonoid; _≉ᴹ_)
+          ; +ᴹ-rawMonoid; rawLeftSemimodule; _≉ᴹ_)
+
+  open RightSemimodule rightSemimodule public
+    using ( rawRightSemimodule )
+
+  rawBisemimodule : RawBisemimodule R.Carrier S.Carrier m ℓm
+  rawBisemimodule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ₗ_ = _*ₗ_
+    ; _*ᵣ_ = _*ᵣ_
+    ; 0ᴹ = 0ᴹ
+    }
 
 record Bimodule (R-ring : Ring r ℓr) (S-ring : Ring s ℓs) m ℓm
                 : Set (r ⊔ s ⊔ ℓr ⊔ ℓs ⊔ suc (m ⊔ ℓm)) where
@@ -254,13 +305,26 @@ record Bimodule (R-ring : Ring r ℓr) (S-ring : Ring s ℓs) m ℓm
   open LeftModule leftModule public
     using ( +ᴹ-abelianGroup; +ᴹ-commutativeMonoid; +ᴹ-group; +ᴹ-monoid
           ; +ᴹ-semigroup; +ᴹ-magma; +ᴹ-rawMagma; +ᴹ-rawMonoid; +ᴹ-rawGroup
-          ; _≉ᴹ_)
+          ; rawLeftSemimodule; rawLeftModule; _≉ᴹ_)
+
+  open RightModule rightModule public
+    using ( rawRightSemimodule; rawRightModule )
 
   bisemimodule : Bisemimodule R.semiring S.semiring m ℓm
   bisemimodule = record { isBisemimodule = isBisemimodule }
 
   open Bisemimodule bisemimodule public
-    using (leftSemimodule; rightSemimodule)
+    using (leftSemimodule; rightSemimodule; rawBisemimodule)
+
+  rawBimodule : RawBimodule R.Carrier S.Carrier m ℓm
+  rawBimodule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ₗ_ = _*ₗ_
+    ; _*ᵣ_ = _*ᵣ_
+    ; 0ᴹ = 0ᴹ
+    ; -ᴹ_ = -ᴹ_
+    }
 
 ------------------------------------------------------------------------
 -- Modules over commutative structures
@@ -296,7 +360,9 @@ record Semimodule (commutativeSemiring : CommutativeSemiring r ℓr) m ℓm
   open Bisemimodule bisemimodule public
     using ( leftSemimodule; rightSemimodule
           ; +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma
-          ; +ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_)
+          ; +ᴹ-rawMagma; +ᴹ-rawMonoid; rawLeftSemimodule; rawRightSemimodule
+          ; rawBisemimodule; _≉ᴹ_
+          )
 
   open SetR ≈ᴹ-setoid
 
@@ -314,6 +380,9 @@ record Semimodule (commutativeSemiring : CommutativeSemiring r ℓr) m ℓm
     m *ᵣ (y * x)  ≈⟨ ≈ᴹ-sym (*ᵣ-assoc m y x) ⟩
     m *ᵣ y *ᵣ x   ∎
 
+  rawSemimodule : RawSemimodule Carrier m ℓm
+  rawSemimodule = rawBisemimodule
+
 record Module (commutativeRing : CommutativeRing r ℓr) m ℓm
               : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
   open CommutativeRing commutativeRing
@@ -343,9 +412,13 @@ record Module (commutativeRing : CommutativeRing r ℓr) m ℓm
     using ( leftModule; rightModule; leftSemimodule; rightSemimodule
           ; +ᴹ-abelianGroup; +ᴹ-group; +ᴹ-commutativeMonoid; +ᴹ-monoid
           ; +ᴹ-semigroup; +ᴹ-magma ; +ᴹ-rawMonoid; +ᴹ-rawMagma
-          ; +ᴹ-rawGroup; _≉ᴹ_)
+          ; +ᴹ-rawGroup; rawLeftSemimodule; rawLeftModule; rawRightSemimodule
+          ; rawRightModule; rawBisemimodule; rawBimodule; _≉ᴹ_)
 
   semimodule : Semimodule commutativeSemiring m ℓm
   semimodule = record { isSemimodule = isSemimodule }
 
-  open Semimodule semimodule public using (*ₗ-comm; *ᵣ-comm)
+  open Semimodule semimodule public using (*ₗ-comm; *ᵣ-comm; rawSemimodule)
+
+  rawModule : RawModule Carrier m ℓm
+  rawModule = rawBimodule
diff --git a/src/Algebra/Module/Bundles/Raw.agda b/src/Algebra/Module/Bundles/Raw.agda
new file mode 100644
index 0000000000..b9cc108915
--- /dev/null
+++ b/src/Algebra/Module/Bundles/Raw.agda
@@ -0,0 +1,251 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definitions of 'raw' bundles for module-like algebraic structures
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Algebra.Module.Bundles.Raw where
+
+open import Algebra.Bundles.Raw
+open import Algebra.Core
+open import Algebra.Module.Core
+open import Level
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Binary.Core using (Rel)
+
+private
+  variable
+    r ℓr s ℓs : Level
+
+------------------------------------------------------------------------
+-- Raw left modules
+------------------------------------------------------------------------
+
+record RawLeftSemimodule (R : Set r) m ℓm : Set (r ⊔ suc (m ⊔ ℓm)) where
+  infixr 7 _*ₗ_
+  infixl 6 _+ᴹ_
+  infix 4 _≈ᴹ_
+
+  field
+    Carrierᴹ : Set m
+    _≈ᴹ_ : Rel Carrierᴹ ℓm
+    _+ᴹ_ : Op₂ Carrierᴹ
+    _*ₗ_ : Opₗ R Carrierᴹ
+    0ᴹ : Carrierᴹ
+
+  +ᴹ-rawMonoid : RawMonoid m ℓm
+  +ᴹ-rawMonoid = record
+    { _≈_ = _≈ᴹ_
+    ; _∙_ = _+ᴹ_
+    ; ε = 0ᴹ
+    }
+
+  open RawMonoid +ᴹ-rawMonoid public
+    using ()
+    renaming (rawMagma to +ᴹ-rawMagma; _≉_ to _≉ᴹ_)
+
+record RawLeftModule (R : Set r) m ℓm : Set (r ⊔ suc (m ⊔ ℓm)) where
+  infix 8 -ᴹ_
+  infixr 7 _*ₗ_
+  infixl 6 _+ᴹ_
+  infix 4 _≈ᴹ_
+
+  field
+    Carrierᴹ : Set m
+    _≈ᴹ_ : Rel Carrierᴹ ℓm
+    _+ᴹ_ : Op₂ Carrierᴹ
+    _*ₗ_ : Opₗ R Carrierᴹ
+    0ᴹ : Carrierᴹ
+    -ᴹ_ : Op₁ Carrierᴹ
+
+  rawLeftSemimodule : RawLeftSemimodule R m ℓm
+  rawLeftSemimodule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ₗ_ = _*ₗ_
+    ; 0ᴹ = 0ᴹ
+    }
+
+  open RawLeftSemimodule rawLeftSemimodule public
+    using (+ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_)
+
+  +ᴹ-rawGroup : RawGroup m ℓm
+  +ᴹ-rawGroup = record
+    { _≈_ = _≈ᴹ_
+    ; _∙_ = _+ᴹ_
+    ; ε = 0ᴹ
+    ; _⁻¹ = -ᴹ_
+    }
+
+------------------------------------------------------------------------
+-- Raw right modules
+------------------------------------------------------------------------
+
+record RawRightSemimodule (R : Set r) m ℓm : Set (r ⊔ suc (m ⊔ ℓm)) where
+  infixl 7 _*ᵣ_
+  infixl 6 _+ᴹ_
+  infix 4 _≈ᴹ_
+
+  field
+    Carrierᴹ : Set m
+    _≈ᴹ_ : Rel Carrierᴹ ℓm
+    _+ᴹ_ : Op₂ Carrierᴹ
+    _*ᵣ_ : Opᵣ R Carrierᴹ
+    0ᴹ : Carrierᴹ
+
+  +ᴹ-rawMonoid : RawMonoid m ℓm
+  +ᴹ-rawMonoid = record
+    { _≈_ = _≈ᴹ_
+    ; _∙_ = _+ᴹ_
+    ; ε = 0ᴹ
+    }
+
+  open RawMonoid +ᴹ-rawMonoid public
+    using ()
+    renaming (rawMagma to +ᴹ-rawMagma; _≉_ to _≉ᴹ_)
+
+record RawRightModule (R : Set r) m ℓm : Set (r ⊔ suc (m ⊔ ℓm)) where
+  infix 8 -ᴹ_
+  infixl 7 _*ᵣ_
+  infixl 6 _+ᴹ_
+  infix 4 _≈ᴹ_
+
+  field
+    Carrierᴹ : Set m
+    _≈ᴹ_ : Rel Carrierᴹ ℓm
+    _+ᴹ_ : Op₂ Carrierᴹ
+    _*ᵣ_ : Opᵣ R Carrierᴹ
+    0ᴹ : Carrierᴹ
+    -ᴹ_ : Op₁ Carrierᴹ
+
+  rawRightSemimodule : RawRightSemimodule R m ℓm
+  rawRightSemimodule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ᵣ_ = _*ᵣ_
+    ; 0ᴹ = 0ᴹ
+    }
+
+  open RawRightSemimodule rawRightSemimodule public
+    using (+ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_)
+
+  +ᴹ-rawGroup : RawGroup m ℓm
+  +ᴹ-rawGroup = record
+    { _≈_ = _≈ᴹ_
+    ; _∙_ = _+ᴹ_
+    ; ε = 0ᴹ
+    ; _⁻¹ = -ᴹ_
+    }
+
+------------------------------------------------------------------------
+-- Bimodules
+------------------------------------------------------------------------
+
+record RawBisemimodule (R : Set r) (S : Set s) m ℓm : Set (r ⊔ s ⊔ suc (m ⊔ ℓm)) where
+  infixr 7 _*ₗ_
+  infixl 7 _*ᵣ_
+  infixl 6 _+ᴹ_
+  infix 4 _≈ᴹ_
+
+  field
+    Carrierᴹ : Set m
+    _≈ᴹ_ : Rel Carrierᴹ ℓm
+    _+ᴹ_ : Op₂ Carrierᴹ
+    _*ₗ_ : Opₗ R Carrierᴹ
+    _*ᵣ_ : Opᵣ S Carrierᴹ
+    0ᴹ : Carrierᴹ
+
+  rawLeftSemimodule : RawLeftSemimodule R m ℓm
+  rawLeftSemimodule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ₗ_ = _*ₗ_
+    ; 0ᴹ = 0ᴹ
+    }
+
+  rawRightSemimodule : RawRightSemimodule S m ℓm
+  rawRightSemimodule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ᵣ_ = _*ᵣ_
+    ; 0ᴹ = 0ᴹ
+    }
+
+  open RawLeftSemimodule rawLeftSemimodule public
+    using (+ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_)
+
+record RawBimodule (R : Set r) (S : Set s) m ℓm : Set (r ⊔ s ⊔ suc (m ⊔ ℓm)) where
+  infix 8 -ᴹ_
+  infixr 7 _*ₗ_
+  infixl 7 _*ᵣ_
+  infixl 6 _+ᴹ_
+  infix 4 _≈ᴹ_
+
+  field
+    Carrierᴹ : Set m
+    _≈ᴹ_ : Rel Carrierᴹ ℓm
+    _+ᴹ_ : Op₂ Carrierᴹ
+    _*ₗ_ : Opₗ R Carrierᴹ
+    _*ᵣ_ : Opᵣ S Carrierᴹ
+    0ᴹ : Carrierᴹ
+    -ᴹ_ : Op₁ Carrierᴹ
+
+  rawLeftModule : RawLeftModule R m ℓm
+  rawLeftModule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ₗ_ = _*ₗ_
+    ; 0ᴹ = 0ᴹ
+    ; -ᴹ_ = -ᴹ_
+    }
+ 
+  rawRightModule : RawRightModule S m ℓm
+  rawRightModule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ᵣ_ = _*ᵣ_
+    ; 0ᴹ = 0ᴹ
+    ; -ᴹ_ = -ᴹ_
+    }
+
+  rawBisemimodule : RawBisemimodule R S m ℓm
+  rawBisemimodule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ₗ_ = _*ₗ_
+    ; _*ᵣ_ = _*ᵣ_
+    ; 0ᴹ = 0ᴹ
+    }
+
+  open RawBisemimodule rawBisemimodule public
+    using (+ᴹ-rawMagma; +ᴹ-rawMonoid; rawLeftSemimodule; rawRightSemimodule; _≉ᴹ_)
+
+  open RawLeftModule rawLeftModule public
+    using (+ᴹ-rawGroup)
+
+------------------------------------------------------------------------
+-- Modules over commutative structures
+------------------------------------------------------------------------
+
+RawSemimodule : ∀ (R : Set r) m ℓm → Set (r ⊔ suc (m ⊔ ℓm))
+RawSemimodule R = RawBisemimodule R R
+
+module RawSemimodule {R : Set r} {m ℓm} (M : RawSemimodule R m ℓm) where
+  open RawBisemimodule M public
+
+  rawBisemimodule : RawBisemimodule R R m ℓm
+  rawBisemimodule = M
+
+RawModule : ∀ (R : Set r) m ℓm → Set (r ⊔ suc(m ⊔ ℓm))
+RawModule R = RawBimodule R R
+
+module RawModule {R : Set r} {m ℓm} (M : RawModule R m ℓm) where
+  open RawBimodule M public
+
+  rawBimodule : RawBimodule R R m ℓm
+  rawBimodule = M
+
+  rawSemimodule : RawSemimodule R m ℓm
+  rawSemimodule = rawBisemimodule
diff --git a/src/Algebra/Module/Construct/DirectProduct.agda b/src/Algebra/Module/Construct/DirectProduct.agda
index 429a2d11ca..473e240801 100644
--- a/src/Algebra/Module/Construct/DirectProduct.agda
+++ b/src/Algebra/Module/Construct/DirectProduct.agda
@@ -14,7 +14,7 @@ module Algebra.Module.Construct.DirectProduct where
 open import Algebra.Bundles
 open import Algebra.Construct.DirectProduct
 open import Algebra.Module.Bundles
-open import Data.Product.Base using (map; _,_; proj₁; proj₂)
+open import Data.Product.Base using (map; zip; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Level
 
@@ -22,6 +22,83 @@ private
   variable
     r s ℓr ℓs m m′ ℓm ℓm′ : Level
 
+------------------------------------------------------------------------
+-- Raw bundles
+
+rawLeftSemimodule : {R : Set r} →
+                    RawLeftSemimodule R m ℓm →
+                    RawLeftSemimodule R m′ ℓm′ →
+                    RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+rawLeftSemimodule M N = record
+  { _≈ᴹ_ = Pointwise M._≈ᴹ_ N._≈ᴹ_
+  ; _+ᴹ_ = zip M._+ᴹ_ N._+ᴹ_
+  ; _*ₗ_ = λ r → map (r M.*ₗ_) (r N.*ₗ_)
+  ; 0ᴹ = M.0ᴹ , N.0ᴹ
+  } where module M = RawLeftSemimodule M; module N = RawLeftSemimodule N
+
+rawLeftModule : {R : Set r} →
+                RawLeftModule R m ℓm →
+                RawLeftModule R m′ ℓm′ →
+                RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+rawLeftModule M N = record
+  { RawLeftSemimodule (rawLeftSemimodule M.rawLeftSemimodule N.rawLeftSemimodule)
+  ; -ᴹ_ = map M.-ᴹ_ N.-ᴹ_
+  } where module M = RawLeftModule M; module N = RawLeftModule N
+
+
+rawRightSemimodule : {R : Set r} →
+                    RawRightSemimodule R m ℓm →
+                    RawRightSemimodule R m′ ℓm′ →
+                    RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+rawRightSemimodule M N = record
+  { _≈ᴹ_ = Pointwise M._≈ᴹ_ N._≈ᴹ_
+  ; _+ᴹ_ = zip M._+ᴹ_ N._+ᴹ_
+  ; _*ᵣ_ = λ mn r → map (M._*ᵣ r) (N._*ᵣ r) mn
+  ; 0ᴹ = M.0ᴹ , N.0ᴹ
+  } where module M = RawRightSemimodule M; module N = RawRightSemimodule N
+
+rawRightModule : {R : Set r} →
+                RawRightModule R m ℓm →
+                RawRightModule R m′ ℓm′ →
+                RawRightModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+rawRightModule M N = record
+  { RawRightSemimodule (rawRightSemimodule M.rawRightSemimodule N.rawRightSemimodule)
+  ; -ᴹ_ = map M.-ᴹ_ N.-ᴹ_
+  } where module M = RawRightModule M; module N = RawRightModule N
+
+rawBisemimodule : {R : Set r} {S : Set s} →
+                    RawBisemimodule R S m ℓm →
+                    RawBisemimodule R S m′ ℓm′ →
+                    RawBisemimodule R S (m ⊔ m′) (ℓm ⊔ ℓm′)
+rawBisemimodule M N = record
+  { _≈ᴹ_ = Pointwise M._≈ᴹ_ N._≈ᴹ_
+  ; _+ᴹ_ = zip M._+ᴹ_ N._+ᴹ_
+  ; _*ₗ_ = λ r → map (r M.*ₗ_) (r N.*ₗ_)
+  ; _*ᵣ_ = λ mn r → map (M._*ᵣ r) (N._*ᵣ r) mn
+  ; 0ᴹ = M.0ᴹ , N.0ᴹ
+  } where module M = RawBisemimodule M; module N = RawBisemimodule N
+
+rawBimodule : {R : Set r} {S : Set s} →
+                RawBimodule R S m ℓm →
+                RawBimodule R S m′ ℓm′ →
+                RawBimodule R S (m ⊔ m′) (ℓm ⊔ ℓm′)
+rawBimodule M N = record
+  { RawBisemimodule (rawBisemimodule M.rawBisemimodule N.rawBisemimodule)
+  ; -ᴹ_ = map M.-ᴹ_ N.-ᴹ_
+  } where module M = RawBimodule M; module N = RawBimodule N
+
+rawSemimodule : {R : Set r} →
+                RawSemimodule R m ℓm →
+                RawSemimodule R m′ ℓm′ →
+                RawSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+rawSemimodule M N = rawBisemimodule M N
+
+rawModule : {R : Set r} →
+            RawModule R m ℓm →
+            RawModule R m′ ℓm′ →
+            RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+rawModule M N = rawBimodule M N
+
 ------------------------------------------------------------------------
 -- Bundles
 
diff --git a/src/Algebra/Module/Construct/TensorUnit.agda b/src/Algebra/Module/Construct/TensorUnit.agda
index c76f2a39ba..6c97b67de0 100644
--- a/src/Algebra/Module/Construct/TensorUnit.agda
+++ b/src/Algebra/Module/Construct/TensorUnit.agda
@@ -19,6 +19,62 @@ private
   variable
     c ℓ : Level
 
+------------------------------------------------------------------------
+-- Raw bundles
+
+rawLeftSemimodule : {R : RawSemiring c ℓ} → RawLeftSemimodule _ c ℓ
+rawLeftSemimodule {R = R} = record
+  { _≈ᴹ_ = _≈_
+  ; _+ᴹ_ = _+_
+  ; _*ₗ_ = _*_
+  ; 0ᴹ = 0#
+  } where open RawSemiring R
+
+rawLeftModule : {R : RawRing c ℓ} → RawLeftModule _ c ℓ
+rawLeftModule {R = R} = record
+  { RawLeftSemimodule (rawLeftSemimodule {R = rawSemiring})
+  ; -ᴹ_ = -_
+  } where open RawRing R
+
+rawRightSemimodule : {R : RawSemiring c ℓ} → RawRightSemimodule _ c ℓ
+rawRightSemimodule {R = R} = record
+  { _≈ᴹ_ = _≈_
+  ; _+ᴹ_ = _+_
+  ; _*ᵣ_ = _*_
+  ; 0ᴹ = 0#
+  } where open RawSemiring R
+
+rawRightModule : {R : RawRing c ℓ} → RawRightModule _ c ℓ
+rawRightModule {R = R} = record
+  { RawRightSemimodule (rawRightSemimodule {R = rawSemiring})
+  ; -ᴹ_ = -_
+  } where open RawRing R
+
+rawBisemimodule : {R : RawSemiring c ℓ} → RawBisemimodule _ _ c ℓ
+rawBisemimodule {R = R} = record
+  { _≈ᴹ_ = _≈_
+  ; _+ᴹ_ = _+_
+  ; _*ₗ_ = _*_
+  ; _*ᵣ_ = _*_
+  ; 0ᴹ = 0#
+  } where open RawSemiring R
+
+rawBimodule : {R : RawRing c ℓ} → RawBimodule _ _ c ℓ
+rawBimodule {R = R} = record
+  { RawBisemimodule (rawBisemimodule {R = rawSemiring})
+  ; -ᴹ_ = -_
+  } where open RawRing R
+
+
+rawSemimodule : {R : RawSemiring c ℓ} → RawSemimodule _ c ℓ
+rawSemimodule {R = R} = rawBisemimodule {R = R}
+
+rawModule : {R : RawRing c ℓ} → RawModule _ c ℓ
+rawModule {R = R} = rawBimodule {R = R}
+
+------------------------------------------------------------------------
+-- Bundles
+
 leftSemimodule : {R : Semiring c ℓ} → LeftSemimodule R c ℓ
 leftSemimodule {R = semiring} = record
   { Carrierᴹ = Carrier
diff --git a/src/Algebra/Module/Construct/Zero.agda b/src/Algebra/Module/Construct/Zero.agda
index 624cd04598..256f70e8c0 100644
--- a/src/Algebra/Module/Construct/Zero.agda
+++ b/src/Algebra/Module/Construct/Zero.agda
@@ -35,14 +35,33 @@ module ℤero where
   _≈ᴹ_     : Rel Carrierᴹ ℓ
   _ ≈ᴹ _ = ⊤
 
-open ℤero
-
 ------------------------------------------------------------------------
--- Raw bundles NOT YET IMPLEMENTED issue #1828
-{-
-rawModule : RawModule c ℓ
+-- Raw bundles
+
+rawLeftSemimodule : {R : Set r} → RawLeftSemimodule R c ℓ
+rawLeftSemimodule = record { ℤero }
+
+rawLeftModule : {R : Set r} → RawLeftModule R c ℓ
+rawLeftModule = record { ℤero }
+
+rawRightSemimodule : {R : Set r} → RawRightSemimodule R c ℓ
+rawRightSemimodule = record { ℤero }
+
+rawRightModule : {R : Set r} → RawRightModule R c ℓ
+rawRightModule = record { ℤero }
+
+rawBisemimodule : {R : Set r} {S : Set s} → RawBisemimodule R S c ℓ
+rawBisemimodule = record { ℤero }
+
+rawBimodule : {R : Set r} {S : Set s} → RawBimodule R S c ℓ
+rawBimodule = record { ℤero }
+
+rawSemimodule : {R : Set r} → RawSemimodule R c ℓ
+rawSemimodule = record { ℤero }
+
+rawModule : {R : Set r} → RawModule R c ℓ
 rawModule = record { ℤero }
--}
+
 ------------------------------------------------------------------------
 -- Bundles