diff --git a/CHANGELOG.md b/CHANGELOG.md
index 97eb05989b..e8f0a568f2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -16,6 +16,14 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
+* The modules and morphisms in `Algebra.Module.Morphism.Structures` are now
+  parametrized by _raw_ bundles rather than lawful bundles, in line with other
+  modules defining morphism structures.
+* The definitions in `Algebra.Module.Morphism.Construct.Composition` are now
+  parametrized by _raw_ bundles, and as such take a proof of transitivity.
+* The definitions in `Algebra.Module.Morphism.Construct.Identity` are now
+  parametrized by _raw_ bundles, and as such take a proof of reflexivity.
+
 Other major improvements
 ------------------------
 
diff --git a/src/Algebra/Module/Morphism/Construct/Composition.agda b/src/Algebra/Module/Morphism/Construct/Composition.agda
index 8c39496dd4..ddeeef6893 100644
--- a/src/Algebra/Module/Morphism/Construct/Composition.agda
+++ b/src/Algebra/Module/Morphism/Construct/Composition.agda
@@ -8,24 +8,25 @@
 
 module Algebra.Module.Morphism.Construct.Composition where
 
-open import Algebra.Bundles
-open import Algebra.Module.Bundles
+open import Algebra.Module.Bundles.Raw
 open import Algebra.Module.Morphism.Structures
 open import Algebra.Morphism.Construct.Composition
 open import Function.Base using (_∘_)
 import Function.Construct.Composition as Func
 open import Level using (Level)
+open import Relation.Binary.Definitions using (Transitive)
 
 private
   variable
-    r ℓr s ℓs m₁ ℓm₁ m₂ ℓm₂ m₃ ℓm₃ : Level
+    r s m₁ ℓm₁ m₂ ℓm₂ m₃ ℓm₃ : Level
 
 module _
-  {semiring : Semiring r ℓr}
-  {M₁ : LeftSemimodule semiring m₁ ℓm₁}
-  {M₂ : LeftSemimodule semiring m₂ ℓm₂}
-  {M₃ : LeftSemimodule semiring m₃ ℓm₃}
-  (open LeftSemimodule)
+  {R : Set r}
+  {M₁ : RawLeftSemimodule R m₁ ℓm₁}
+  {M₂ : RawLeftSemimodule R m₂ ℓm₂}
+  {M₃ : RawLeftSemimodule R m₃ ℓm₃}
+  (open RawLeftSemimodule)
+  (≈ᴹ₃-trans : Transitive (_≈ᴹ_ M₃))
   {f : Carrierᴹ M₁ → Carrierᴹ M₂}
   {g : Carrierᴹ M₂ → Carrierᴹ M₃}
   where
@@ -34,8 +35,8 @@ module _
                                  IsLeftSemimoduleHomomorphism M₂ M₃ g →
                                  IsLeftSemimoduleHomomorphism M₁ M₃ (g ∘ f)
   isLeftSemimoduleHomomorphism f-homo g-homo = record
-    { +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism (≈ᴹ-trans M₃) F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
-    ; *ₗ-homo                 = λ r x → ≈ᴹ-trans M₃ (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
+    { +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism ≈ᴹ₃-trans F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
+    ; *ₗ-homo                 = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
     } where module F = IsLeftSemimoduleHomomorphism f-homo; module G = IsLeftSemimoduleHomomorphism g-homo
 
   isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism M₁ M₂ f →
@@ -55,11 +56,12 @@ module _
     } where module F = IsLeftSemimoduleIsomorphism f-iso; module G = IsLeftSemimoduleIsomorphism g-iso
 
 module _
-  {ring : Ring r ℓr}
-  {M₁ : LeftModule ring m₁ ℓm₁}
-  {M₂ : LeftModule ring m₂ ℓm₂}
-  {M₃ : LeftModule ring m₃ ℓm₃}
-  (open LeftModule)
+  {R : Set r}
+  {M₁ : RawLeftModule R m₁ ℓm₁}
+  {M₂ : RawLeftModule R m₂ ℓm₂}
+  {M₃ : RawLeftModule R m₃ ℓm₃}
+  (open RawLeftModule)
+  (≈ᴹ₃-trans : Transitive (_≈ᴹ_ M₃))
   {f : Carrierᴹ M₁ → Carrierᴹ M₂}
   {g : Carrierᴹ M₂ → Carrierᴹ M₃}
   where
@@ -68,8 +70,8 @@ module _
                              IsLeftModuleHomomorphism M₂ M₃ g →
                              IsLeftModuleHomomorphism M₁ M₃ (g ∘ f)
   isLeftModuleHomomorphism f-homo g-homo = record
-    { +ᴹ-isGroupHomomorphism = isGroupHomomorphism (≈ᴹ-trans M₃) F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
-    ; *ₗ-homo = λ r x → ≈ᴹ-trans M₃ (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
+    { +ᴹ-isGroupHomomorphism = isGroupHomomorphism ≈ᴹ₃-trans F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
+    ; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
     } where module F = IsLeftModuleHomomorphism f-homo; module G = IsLeftModuleHomomorphism g-homo
 
   isLeftModuleMonomorphism : IsLeftModuleMonomorphism M₁ M₂ f →
@@ -89,11 +91,12 @@ module _
     } where module F = IsLeftModuleIsomorphism f-iso; module G = IsLeftModuleIsomorphism g-iso
 
 module _
-  {semiring : Semiring r ℓr}
-  {M₁ : RightSemimodule semiring m₁ ℓm₁}
-  {M₂ : RightSemimodule semiring m₂ ℓm₂}
-  {M₃ : RightSemimodule semiring m₃ ℓm₃}
-  (open RightSemimodule)
+  {R : Set r}
+  {M₁ : RawRightSemimodule R m₁ ℓm₁}
+  {M₂ : RawRightSemimodule R m₂ ℓm₂}
+  {M₃ : RawRightSemimodule R m₃ ℓm₃}
+  (open RawRightSemimodule)
+  (≈ᴹ₃-trans : Transitive (_≈ᴹ_ M₃))
   {f : Carrierᴹ M₁ → Carrierᴹ M₂}
   {g : Carrierᴹ M₂ → Carrierᴹ M₃}
   where
@@ -102,8 +105,8 @@ module _
                                   IsRightSemimoduleHomomorphism M₂ M₃ g →
                                   IsRightSemimoduleHomomorphism M₁ M₃ (g ∘ f)
   isRightSemimoduleHomomorphism f-homo g-homo = record
-    { +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism (≈ᴹ-trans M₃) F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
-    ; *ᵣ-homo                 = λ r x → ≈ᴹ-trans M₃ (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
+    { +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism ≈ᴹ₃-trans F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
+    ; *ᵣ-homo                 = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
     } where module F = IsRightSemimoduleHomomorphism f-homo; module G = IsRightSemimoduleHomomorphism g-homo
 
   isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism M₁ M₂ f →
@@ -123,11 +126,12 @@ module _
     } where module F = IsRightSemimoduleIsomorphism f-iso; module G = IsRightSemimoduleIsomorphism g-iso
 
 module _
-  {ring : Ring r ℓr}
-  {M₁ : RightModule ring m₁ ℓm₁}
-  {M₂ : RightModule ring m₂ ℓm₂}
-  {M₃ : RightModule ring m₃ ℓm₃}
-  (open RightModule)
+  {R : Set r}
+  {M₁ : RawRightModule R m₁ ℓm₁}
+  {M₂ : RawRightModule R m₂ ℓm₂}
+  {M₃ : RawRightModule R m₃ ℓm₃}
+  (open RawRightModule)
+  (≈ᴹ₃-trans : Transitive (_≈ᴹ_ M₃))
   {f : Carrierᴹ M₁ → Carrierᴹ M₂}
   {g : Carrierᴹ M₂ → Carrierᴹ M₃}
   where
@@ -136,8 +140,8 @@ module _
                               IsRightModuleHomomorphism M₂ M₃ g →
                               IsRightModuleHomomorphism M₁ M₃ (g ∘ f)
   isRightModuleHomomorphism f-homo g-homo = record
-    { +ᴹ-isGroupHomomorphism = isGroupHomomorphism (≈ᴹ-trans M₃) F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
-    ; *ᵣ-homo                = λ r x → ≈ᴹ-trans M₃ (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
+    { +ᴹ-isGroupHomomorphism = isGroupHomomorphism ≈ᴹ₃-trans F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
+    ; *ᵣ-homo                = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
     } where module F = IsRightModuleHomomorphism f-homo; module G = IsRightModuleHomomorphism g-homo
 
   isRightModuleMonomorphism : IsRightModuleMonomorphism M₁ M₂ f →
@@ -157,12 +161,13 @@ module _
     } where module F = IsRightModuleIsomorphism f-iso; module G = IsRightModuleIsomorphism g-iso
 
 module _
-  {R-semiring : Semiring r ℓr}
-  {S-semiring : Semiring s ℓs}
-  {M₁ : Bisemimodule R-semiring S-semiring m₁ ℓm₁}
-  {M₂ : Bisemimodule R-semiring S-semiring m₂ ℓm₂}
-  {M₃ : Bisemimodule R-semiring S-semiring m₃ ℓm₃}
-  (open Bisemimodule)
+  {R : Set r}
+  {S : Set s}
+  {M₁ : RawBisemimodule R S m₁ ℓm₁}
+  {M₂ : RawBisemimodule R S m₂ ℓm₂}
+  {M₃ : RawBisemimodule R S m₃ ℓm₃}
+  (open RawBisemimodule)
+  (≈ᴹ₃-trans : Transitive (_≈ᴹ_ M₃))
   {f : Carrierᴹ M₁ → Carrierᴹ M₂}
   {g : Carrierᴹ M₂ → Carrierᴹ M₃}
   where
@@ -171,9 +176,9 @@ module _
                                IsBisemimoduleHomomorphism M₂ M₃ g →
                                IsBisemimoduleHomomorphism M₁ M₃ (g ∘ f)
   isBisemimoduleHomomorphism f-homo g-homo = record
-    { +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism (≈ᴹ-trans M₃) F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
-    ; *ₗ-homo                 = λ r x → ≈ᴹ-trans M₃ (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
-    ; *ᵣ-homo                 = λ r x → ≈ᴹ-trans M₃ (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
+    { +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism ≈ᴹ₃-trans F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
+    ; *ₗ-homo                 = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
+    ; *ᵣ-homo                 = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
     } where module F = IsBisemimoduleHomomorphism f-homo; module G = IsBisemimoduleHomomorphism g-homo
 
   isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism M₁ M₂ f →
@@ -193,12 +198,13 @@ module _
     } where module F = IsBisemimoduleIsomorphism f-iso; module G = IsBisemimoduleIsomorphism g-iso
 
 module _
-  {R-ring : Ring r ℓr}
-  {S-ring : Ring s ℓs}
-  {M₁ : Bimodule R-ring S-ring m₁ ℓm₁}
-  {M₂ : Bimodule R-ring S-ring m₂ ℓm₂}
-  {M₃ : Bimodule R-ring S-ring m₃ ℓm₃}
-  (open Bimodule)
+  {R : Set r}
+  {S : Set s}
+  {M₁ : RawBimodule R S m₁ ℓm₁}
+  {M₂ : RawBimodule R S m₂ ℓm₂}
+  {M₃ : RawBimodule R S m₃ ℓm₃}
+  (open RawBimodule)
+  (≈ᴹ₃-trans : Transitive (_≈ᴹ_ M₃))
   {f : Carrierᴹ M₁ → Carrierᴹ M₂}
   {g : Carrierᴹ M₂ → Carrierᴹ M₃}
   where
@@ -207,9 +213,9 @@ module _
                            IsBimoduleHomomorphism M₂ M₃ g →
                            IsBimoduleHomomorphism M₁ M₃ (g ∘ f)
   isBimoduleHomomorphism f-homo g-homo = record
-    { +ᴹ-isGroupHomomorphism = isGroupHomomorphism (≈ᴹ-trans M₃) F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
-    ; *ₗ-homo                = λ r x → ≈ᴹ-trans M₃ (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
-    ; *ᵣ-homo                = λ r x → ≈ᴹ-trans M₃ (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
+    { +ᴹ-isGroupHomomorphism = isGroupHomomorphism ≈ᴹ₃-trans F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
+    ; *ₗ-homo                = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
+    ; *ᵣ-homo                = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
     } where module F = IsBimoduleHomomorphism f-homo; module G = IsBimoduleHomomorphism g-homo
 
   isBimoduleMonomorphism : IsBimoduleMonomorphism M₁ M₂ f →
@@ -229,11 +235,12 @@ module _
     } where module F = IsBimoduleIsomorphism f-iso; module G = IsBimoduleIsomorphism g-iso
 
 module _
-  {commutativeSemiring : CommutativeSemiring r ℓr}
-  {M₁ : Semimodule commutativeSemiring m₁ ℓm₁}
-  {M₂ : Semimodule commutativeSemiring m₂ ℓm₂}
-  {M₃ : Semimodule commutativeSemiring m₃ ℓm₃}
-  (open Semimodule)
+  {R : Set r}
+  {M₁ : RawSemimodule R m₁ ℓm₁}
+  {M₂ : RawSemimodule R m₂ ℓm₂}
+  {M₃ : RawSemimodule R m₃ ℓm₃}
+  (open RawSemimodule)
+  (≈ᴹ₃-trans : Transitive (_≈ᴹ_ M₃))
   {f : Carrierᴹ M₁ → Carrierᴹ M₂}
   {g : Carrierᴹ M₂ → Carrierᴹ M₃}
   where
@@ -242,7 +249,7 @@ module _
                              IsSemimoduleHomomorphism M₂ M₃ g →
                              IsSemimoduleHomomorphism M₁ M₃ (g ∘ f)
   isSemimoduleHomomorphism f-homo g-homo = record
-    { isBisemimoduleHomomorphism = isBisemimoduleHomomorphism F.isBisemimoduleHomomorphism G.isBisemimoduleHomomorphism
+    { isBisemimoduleHomomorphism = isBisemimoduleHomomorphism ≈ᴹ₃-trans F.isBisemimoduleHomomorphism G.isBisemimoduleHomomorphism
     } where module F = IsSemimoduleHomomorphism f-homo; module G = IsSemimoduleHomomorphism g-homo
 
   isSemimoduleMonomorphism : IsSemimoduleMonomorphism M₁ M₂ f →
@@ -262,11 +269,12 @@ module _
     } where module F = IsSemimoduleIsomorphism f-iso; module G = IsSemimoduleIsomorphism g-iso
 
 module _
-  {commutativeRing : CommutativeRing r ℓr}
-  {M₁ : Module commutativeRing m₁ ℓm₁}
-  {M₂ : Module commutativeRing m₂ ℓm₂}
-  {M₃ : Module commutativeRing m₃ ℓm₃}
-  (open Module)
+  {R : Set r}
+  {M₁ : RawModule R m₁ ℓm₁}
+  {M₂ : RawModule R m₂ ℓm₂}
+  {M₃ : RawModule R m₃ ℓm₃}
+  (open RawModule)
+  (≈ᴹ₃-trans : Transitive (_≈ᴹ_ M₃))
   {f : Carrierᴹ M₁ → Carrierᴹ M₂}
   {g : Carrierᴹ M₂ → Carrierᴹ M₃}
   where
@@ -275,7 +283,7 @@ module _
                          IsModuleHomomorphism M₂ M₃ g →
                          IsModuleHomomorphism M₁ M₃ (g ∘ f)
   isModuleHomomorphism f-homo g-homo = record
-    { isBimoduleHomomorphism = isBimoduleHomomorphism F.isBimoduleHomomorphism G.isBimoduleHomomorphism
+    { isBimoduleHomomorphism = isBimoduleHomomorphism ≈ᴹ₃-trans F.isBimoduleHomomorphism G.isBimoduleHomomorphism
     } where module F = IsModuleHomomorphism f-homo; module G = IsModuleHomomorphism g-homo
 
   isModuleMonomorphism : IsModuleMonomorphism M₁ M₂ f →
diff --git a/src/Algebra/Module/Morphism/Construct/Identity.agda b/src/Algebra/Module/Morphism/Construct/Identity.agda
index 55735c2b24..54a08af98c 100644
--- a/src/Algebra/Module/Morphism/Construct/Identity.agda
+++ b/src/Algebra/Module/Morphism/Construct/Identity.agda
@@ -8,8 +8,7 @@
 
 module Algebra.Module.Morphism.Construct.Identity where
 
-open import Algebra.Bundles
-open import Algebra.Module.Bundles
+open import Algebra.Module.Bundles.Raw
 open import Algebra.Module.Morphism.Structures
   using ( module LeftSemimoduleMorphisms
         ; module LeftModuleMorphisms
@@ -25,13 +24,13 @@ open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
 import Function.Construct.Identity as Id
 open import Level using (Level)
+open import Relation.Binary.Definitions using (Reflexive)
 
 private
   variable
-    r ℓr s ℓs m ℓm : Level
+    r s m ℓm : Level
 
-module _ {semiring : Semiring r ℓr} (M : LeftSemimodule semiring m ℓm) where
-  open LeftSemimodule M using (≈ᴹ-refl)
+module _ {R : Set r} (M : RawLeftSemimodule R m ℓm) (open RawLeftSemimodule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
   open LeftSemimoduleMorphisms M M
 
   isLeftSemimoduleHomomorphism : IsLeftSemimoduleHomomorphism id
@@ -52,8 +51,7 @@ module _ {semiring : Semiring r ℓr} (M : LeftSemimodule semiring m ℓm) where
     ; surjective                   = Id.surjective _
     }
 
-module _ {ring : Ring r ℓr} (M : LeftModule ring m ℓm) where
-  open LeftModule M using (≈ᴹ-refl)
+module _ {R : Set r} (M : RawLeftModule R m ℓm) (open RawLeftModule M) (≈ᴹ-refl : Reflexive _≈ᴹ_)  where
   open LeftModuleMorphisms M M
 
   isLeftModuleHomomorphism : IsLeftModuleHomomorphism id
@@ -74,8 +72,7 @@ module _ {ring : Ring r ℓr} (M : LeftModule ring m ℓm) where
     ; surjective               = Id.surjective _
     }
 
-module _ {semiring : Semiring r ℓr} (M : RightSemimodule semiring m ℓm) where
-  open RightSemimodule M using (≈ᴹ-refl)
+module _ {R : Set r} (M : RawRightSemimodule R m ℓm) (open RawRightSemimodule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
   open RightSemimoduleMorphisms M M
 
   isRightSemimoduleHomomorphism : IsRightSemimoduleHomomorphism id
@@ -96,8 +93,7 @@ module _ {semiring : Semiring r ℓr} (M : RightSemimodule semiring m ℓm) wher
     ; surjective                    = Id.surjective _
     }
 
-module _ {ring : Ring r ℓr} (M : RightModule ring m ℓm) where
-  open RightModule M using (≈ᴹ-refl)
+module _ {R : Set r} (M : RawRightModule R m ℓm) (open RawRightModule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
   open RightModuleMorphisms M M
 
   isRightModuleHomomorphism : IsRightModuleHomomorphism id
@@ -118,8 +114,7 @@ module _ {ring : Ring r ℓr} (M : RightModule ring m ℓm) where
     ; surjective                = Id.surjective _
     }
 
-module _ {R-semiring : Semiring r ℓr} {S-semiring : Semiring s ℓs} (M : Bisemimodule R-semiring S-semiring m ℓm) where
-  open Bisemimodule M using (≈ᴹ-refl)
+module _ {R : Set r} {S : Set s} (M : RawBisemimodule R S m ℓm) (open RawBisemimodule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
   open BisemimoduleMorphisms M M
 
   isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism id
@@ -141,8 +136,7 @@ module _ {R-semiring : Semiring r ℓr} {S-semiring : Semiring s ℓs} (M : Bise
     ; surjective                 = Id.surjective _
     }
 
-module _ {R-ring : Ring r ℓr} {S-ring : Ring r ℓr} (M : Bimodule R-ring S-ring m ℓm) where
-  open Bimodule M using (≈ᴹ-refl)
+module _ {R : Set r} {S : Set s} (M : RawBimodule R S m ℓm) (open RawBimodule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
   open BimoduleMorphisms M M
 
   isBimoduleHomomorphism : IsBimoduleHomomorphism id
@@ -164,13 +158,12 @@ module _ {R-ring : Ring r ℓr} {S-ring : Ring r ℓr} (M : Bimodule R-ring S-ri
     ; surjective             = Id.surjective _
     }
 
-module _ {commutativeSemiring : CommutativeSemiring r ℓr} (M : Semimodule commutativeSemiring m ℓm) where
-  open Semimodule M using (≈ᴹ-refl)
+module _ {R : Set r} (M : RawSemimodule R m ℓm) (open RawSemimodule M) (≈ᴹ-refl : Reflexive _≈ᴹ_)  where
   open SemimoduleMorphisms M M
 
   isSemimoduleHomomorphism : IsSemimoduleHomomorphism id
   isSemimoduleHomomorphism = record
-    { isBisemimoduleHomomorphism = isBisemimoduleHomomorphism _
+    { isBisemimoduleHomomorphism = isBisemimoduleHomomorphism _ ≈ᴹ-refl
     }
 
   isSemimoduleMonomorphism : IsSemimoduleMonomorphism id
@@ -185,13 +178,12 @@ module _ {commutativeSemiring : CommutativeSemiring r ℓr} (M : Semimodule comm
     ; surjective               = Id.surjective _
     }
 
-module _ {commutativeRing : CommutativeRing r ℓr} (M : Module commutativeRing m ℓm) where
-  open Module M using (≈ᴹ-refl)
+module _ {R : Set r} (M : RawModule R m ℓm) (open RawModule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
   open ModuleMorphisms M M
 
   isModuleHomomorphism : IsModuleHomomorphism id
   isModuleHomomorphism = record
-    { isBimoduleHomomorphism = isBimoduleHomomorphism _
+    { isBimoduleHomomorphism = isBimoduleHomomorphism _ ≈ᴹ-refl
     }
 
   isModuleMonomorphism : IsModuleMonomorphism id
diff --git a/src/Algebra/Module/Morphism/ModuleHomomorphism.agda b/src/Algebra/Module/Morphism/ModuleHomomorphism.agda
index 704ec3863c..6bd7f2b4e6 100644
--- a/src/Algebra/Module/Morphism/ModuleHomomorphism.agda
+++ b/src/Algebra/Module/Morphism/ModuleHomomorphism.agda
@@ -17,10 +17,10 @@ module Algebra.Module.Morphism.ModuleHomomorphism
   {r ℓr m ℓm : Level}
   {ring      : CommutativeRing r ℓr}
   (modA modB  : Module ring m ℓm)
-  (open Module modA using () renaming (Carrierᴹ to A))
-  (open Module modB using () renaming (Carrierᴹ to B))
+  (open Module modA using () renaming (Carrierᴹ to A; rawModule to rawModA))
+  (open Module modB using () renaming (Carrierᴹ to B; rawModule to rawModB))
   {f : A → B}
-  (open MorphismStructures.ModuleMorphisms modA modB)
+  (open MorphismStructures.ModuleMorphisms rawModA rawModB)
   (isModuleHomomorphism : IsModuleHomomorphism f)
   where
 
diff --git a/src/Algebra/Module/Morphism/Structures.agda b/src/Algebra/Module/Morphism/Structures.agda
index 96fb5ffa0a..e874f4d341 100644
--- a/src/Algebra/Module/Morphism/Structures.agda
+++ b/src/Algebra/Module/Morphism/Structures.agda
@@ -7,8 +7,7 @@
 
 module Algebra.Module.Morphism.Structures where
 
-open import Algebra.Bundles
-open import Algebra.Module.Bundles
+open import Algebra.Module.Bundles.Raw
 import Algebra.Module.Morphism.Definitions as MorphismDefinitions
 import Algebra.Morphism.Structures as MorphismStructures
 open import Function.Definitions
@@ -16,19 +15,18 @@ open import Level
 
 private
   variable
-    r ℓr s ℓs m₁ m₂ ℓm₁ ℓm₂ : Level
+    r s m₁ m₂ ℓm₁ ℓm₂ : Level
 
 module LeftSemimoduleMorphisms
-  {semiring : Semiring r ℓr}
-  (M₁ : LeftSemimodule semiring m₁ ℓm₁)
-  (M₂ : LeftSemimodule semiring m₂ ℓm₂)
+  {R : Set r}
+  (M₁ : RawLeftSemimodule R m₁ ℓm₁)
+  (M₂ : RawLeftSemimodule R m₂ ℓm₂)
   where
 
-  open Semiring semiring renaming (Carrier to R)
-  open LeftSemimodule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _≈ᴹ_ to _≈ᴹ₁_)
-  open LeftSemimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _≈ᴹ_ to _≈ᴹ₂_)
+  open RawLeftSemimodule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _≈ᴹ_ to _≈ᴹ₁_)
+  open RawLeftSemimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _≈ᴹ_ to _≈ᴹ₂_)
   open MorphismDefinitions R A B _≈ᴹ₂_
-  open MorphismStructures.MonoidMorphisms (LeftSemimodule.+ᴹ-rawMonoid M₁) (LeftSemimodule.+ᴹ-rawMonoid M₂)
+  open MorphismStructures.MonoidMorphisms (RawLeftSemimodule.+ᴹ-rawMonoid M₁) (RawLeftSemimodule.+ᴹ-rawMonoid M₂)
 
   record IsLeftSemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
@@ -74,17 +72,16 @@ module LeftSemimoduleMorphisms
       renaming (isMagmaIsomorphism to +ᴹ-isMagmaIsomorphism)
 
 module LeftModuleMorphisms
-  {ring : Ring r ℓr}
-  (M₁ : LeftModule ring m₁ ℓm₁)
-  (M₂ : LeftModule ring m₂ ℓm₂)
+  {R : Set r}
+  (M₁ : RawLeftModule R m₁ ℓm₁)
+  (M₂ : RawLeftModule R m₂ ℓm₂)
   where
 
-  open Ring ring renaming (Carrier to R)
-  open LeftModule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _≈ᴹ_ to _≈ᴹ₁_)
-  open LeftModule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _≈ᴹ_ to _≈ᴹ₂_)
+  open RawLeftModule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _≈ᴹ_ to _≈ᴹ₁_)
+  open RawLeftModule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _≈ᴹ_ to _≈ᴹ₂_)
   open MorphismDefinitions R A B _≈ᴹ₂_
-  open MorphismStructures.GroupMorphisms (LeftModule.+ᴹ-rawGroup M₁) (LeftModule.+ᴹ-rawGroup M₂)
-  open LeftSemimoduleMorphisms (LeftModule.leftSemimodule M₁) (LeftModule.leftSemimodule M₂)
+  open MorphismStructures.GroupMorphisms (RawLeftModule.+ᴹ-rawGroup M₁) (RawLeftModule.+ᴹ-rawGroup M₂)
+  open LeftSemimoduleMorphisms (RawLeftModule.rawLeftSemimodule M₁) (RawLeftModule.rawLeftSemimodule M₂)
 
   record IsLeftModuleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
@@ -148,16 +145,15 @@ module LeftModuleMorphisms
       }
 
 module RightSemimoduleMorphisms
-  {semiring : Semiring r ℓr}
-  (M₁ : RightSemimodule semiring m₁ ℓm₁)
-  (M₂ : RightSemimodule semiring m₂ ℓm₂)
+  {R : Set r}
+  (M₁ : RawRightSemimodule R m₁ ℓm₁)
+  (M₂ : RawRightSemimodule R m₂ ℓm₂)
   where
 
-  open Semiring semiring renaming (Carrier to R)
-  open RightSemimodule M₁ renaming (Carrierᴹ to A; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_)
-  open RightSemimodule M₂ renaming (Carrierᴹ to B; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_)
+  open RawRightSemimodule M₁ renaming (Carrierᴹ to A; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_)
+  open RawRightSemimodule M₂ renaming (Carrierᴹ to B; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_)
   open MorphismDefinitions R A B _≈ᴹ₂_
-  open MorphismStructures.MonoidMorphisms (RightSemimodule.+ᴹ-rawMonoid M₁) (RightSemimodule.+ᴹ-rawMonoid M₂)
+  open MorphismStructures.MonoidMorphisms (RawRightSemimodule.+ᴹ-rawMonoid M₁) (RawRightSemimodule.+ᴹ-rawMonoid M₂)
 
   record IsRightSemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
@@ -203,17 +199,16 @@ module RightSemimoduleMorphisms
       renaming (isMagmaIsomorphism to +ᴹ-isMagmaIsomorphism)
 
 module RightModuleMorphisms
-  {ring : Ring r ℓr}
-  (M₁ : RightModule ring m₁ ℓm₁)
-  (M₂ : RightModule ring m₂ ℓm₂)
+  {R : Set r}
+  (M₁ : RawRightModule R m₁ ℓm₁)
+  (M₂ : RawRightModule R m₂ ℓm₂)
   where
 
-  open Ring ring renaming (Carrier to R)
-  open RightModule M₁ renaming (Carrierᴹ to A; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_)
-  open RightModule M₂ renaming (Carrierᴹ to B; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_)
+  open RawRightModule M₁ renaming (Carrierᴹ to A; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_)
+  open RawRightModule M₂ renaming (Carrierᴹ to B; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_)
   open MorphismDefinitions R A B _≈ᴹ₂_
-  open MorphismStructures.GroupMorphisms (RightModule.+ᴹ-rawGroup M₁) (RightModule.+ᴹ-rawGroup M₂)
-  open RightSemimoduleMorphisms (RightModule.rightSemimodule M₁) (RightModule.rightSemimodule M₂)
+  open MorphismStructures.GroupMorphisms (RawRightModule.+ᴹ-rawGroup M₁) (RawRightModule.+ᴹ-rawGroup M₂)
+  open RightSemimoduleMorphisms (RawRightModule.rawRightSemimodule M₁) (RawRightModule.rawRightSemimodule M₂)
 
   record IsRightModuleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
@@ -276,21 +271,19 @@ module RightModuleMorphisms
       }
 
 module BisemimoduleMorphisms
-  {R-semiring : Semiring r ℓr}
-  {S-semiring : Semiring s ℓs}
-  (M₁ : Bisemimodule R-semiring S-semiring m₁ ℓm₁)
-  (M₂ : Bisemimodule R-semiring S-semiring m₂ ℓm₂)
+  {R : Set r}
+  {S : Set s}
+  (M₁ : RawBisemimodule R S m₁ ℓm₁)
+  (M₂ : RawBisemimodule R S m₂ ℓm₂)
   where
 
-  open Semiring R-semiring renaming (Carrier to R)
-  open Semiring S-semiring renaming (Carrier to S)
-  open Bisemimodule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_)
-  open Bisemimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_)
+  open RawBisemimodule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_)
+  open RawBisemimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_)
   open MorphismDefinitions R A B _≈ᴹ₂_ using (Homomorphicₗ)
   open MorphismDefinitions S A B _≈ᴹ₂_ using (Homomorphicᵣ)
-  open MorphismStructures.MonoidMorphisms (Bisemimodule.+ᴹ-rawMonoid M₁) (Bisemimodule.+ᴹ-rawMonoid M₂)
-  open LeftSemimoduleMorphisms (Bisemimodule.leftSemimodule M₁) (Bisemimodule.leftSemimodule M₂)
-  open RightSemimoduleMorphisms (Bisemimodule.rightSemimodule M₁) (Bisemimodule.rightSemimodule M₂)
+  open MorphismStructures.MonoidMorphisms (RawBisemimodule.+ᴹ-rawMonoid M₁) (RawBisemimodule.+ᴹ-rawMonoid M₂)
+  open LeftSemimoduleMorphisms (RawBisemimodule.rawLeftSemimodule M₁) (RawBisemimodule.rawLeftSemimodule M₂)
+  open RightSemimoduleMorphisms (RawBisemimodule.rawRightSemimodule M₁) (RawBisemimodule.rawRightSemimodule M₂)
 
   record IsBisemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ s ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
@@ -358,22 +351,20 @@ module BisemimoduleMorphisms
       }
 
 module BimoduleMorphisms
-  {R-ring : Ring r ℓr}
-  {S-ring : Ring s ℓs}
-  (M₁ : Bimodule R-ring S-ring m₁ ℓm₁)
-  (M₂ : Bimodule R-ring S-ring m₂ ℓm₂)
+  {R : Set r}
+  {S : Set s}
+  (M₁ : RawBimodule R S m₁ ℓm₁)
+  (M₂ : RawBimodule R S m₂ ℓm₂)
   where
 
-  open Ring R-ring renaming (Carrier to R)
-  open Ring S-ring renaming (Carrier to S)
-  open Bimodule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_)
-  open Bimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_)
+  open RawBimodule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_)
+  open RawBimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_)
   open MorphismDefinitions R A B _≈ᴹ₂_ using (Homomorphicₗ)
   open MorphismDefinitions S A B _≈ᴹ₂_ using (Homomorphicᵣ)
-  open MorphismStructures.GroupMorphisms (Bimodule.+ᴹ-rawGroup M₁) (Bimodule.+ᴹ-rawGroup M₂)
-  open LeftModuleMorphisms (Bimodule.leftModule M₁) (Bimodule.leftModule M₂)
-  open RightModuleMorphisms (Bimodule.rightModule M₁) (Bimodule.rightModule M₂)
-  open BisemimoduleMorphisms (Bimodule.bisemimodule M₁) (Bimodule.bisemimodule M₂)
+  open MorphismStructures.GroupMorphisms (RawBimodule.+ᴹ-rawGroup M₁) (RawBimodule.+ᴹ-rawGroup M₂)
+  open LeftModuleMorphisms (RawBimodule.rawLeftModule M₁) (RawBimodule.rawLeftModule M₂)
+  open RightModuleMorphisms (RawBimodule.rawRightModule M₁) (RawBimodule.rawRightModule M₂)
+  open BisemimoduleMorphisms (RawBimodule.rawBisemimodule M₁) (RawBimodule.rawBisemimodule M₂)
 
   record IsBimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ s ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
@@ -492,14 +483,14 @@ module BimoduleMorphisms
       }
 
 module SemimoduleMorphisms
-  {commutativeSemiring : CommutativeSemiring r ℓr}
-  (M₁ : Semimodule commutativeSemiring m₁ ℓm₁)
-  (M₂ : Semimodule commutativeSemiring m₂ ℓm₂)
+  {R : Set r}
+  (M₁ : RawSemimodule R m₁ ℓm₁)
+  (M₂ : RawSemimodule R m₂ ℓm₂)
   where
 
-  open Semimodule M₁ renaming (Carrierᴹ to A; _≈ᴹ_ to _≈ᴹ₁_)
-  open Semimodule M₂ renaming (Carrierᴹ to B; _≈ᴹ_ to _≈ᴹ₂_)
-  open BisemimoduleMorphisms (Semimodule.bisemimodule M₁) (Semimodule.bisemimodule M₂)
+  open RawSemimodule M₁ renaming (Carrierᴹ to A; _≈ᴹ_ to _≈ᴹ₁_)
+  open RawSemimodule M₂ renaming (Carrierᴹ to B; _≈ᴹ_ to _≈ᴹ₂_)
+  open BisemimoduleMorphisms (RawSemimodule.rawBisemimodule M₁) (RawSemimodule.rawBisemimodule M₂)
 
   record IsSemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
@@ -544,15 +535,15 @@ module SemimoduleMorphisms
             )
 
 module ModuleMorphisms
-  {commutativeRing : CommutativeRing r ℓr}
-  (M₁ : Module commutativeRing m₁ ℓm₁)
-  (M₂ : Module commutativeRing m₂ ℓm₂)
+  {R : Set r}
+  (M₁ : RawModule R m₁ ℓm₁)
+  (M₂ : RawModule R m₂ ℓm₂)
   where
 
-  open Module M₁ renaming (Carrierᴹ to A; _≈ᴹ_ to _≈ᴹ₁_)
-  open Module M₂ renaming (Carrierᴹ to B; _≈ᴹ_ to _≈ᴹ₂_)
-  open BimoduleMorphisms (Module.bimodule M₁) (Module.bimodule M₂)
-  open SemimoduleMorphisms (Module.semimodule M₁) (Module.semimodule M₂)
+  open RawModule M₁ renaming (Carrierᴹ to A; _≈ᴹ_ to _≈ᴹ₁_)
+  open RawModule M₂ renaming (Carrierᴹ to B; _≈ᴹ_ to _≈ᴹ₂_)
+  open BimoduleMorphisms (RawModule.rawBimodule M₁) (RawModule.rawBimodule M₂)
+  open SemimoduleMorphisms (RawModule.rawBisemimodule M₁) (RawModule.rawBisemimodule M₂)
 
   record IsModuleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field