style

Author: Taneb

src/Algebra/Construct/Sub/Group.agda

@@ -10,14 +10,14 @@ open import Algebra.Bundles using (Group; RawGroup)
 
 module Algebra.Construct.Sub.Group {c ℓ} (G : Group c ℓ) where
 
-private
-  module G = Group G
-
 open import Algebra.Structures using (IsGroup)
 open import Algebra.Morphism.Structures using (IsGroupMonomorphism)
 import Algebra.Morphism.GroupMonomorphism as GroupMonomorphism
 open import Level using (suc; _⊔_)
 
+private
+  module G = Group G
+
 record Subgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
   field
     domain : RawGroup c′ ℓ′

src/Algebra/Module/Construct/Sub/Bimodule.agda

@@ -9,18 +9,21 @@
 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
+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.Structures using (IsBimodule)
+open import Algebra.Module.Morphism.Structures using (IsBimoduleMonomorphism)
+import Algebra.Module.Morphism.BimoduleMonomorphism as BimoduleMonomorphism
+open import Level using (suc; _⊔_)
 
 private
   module R = Ring R
   module S = Ring S
   module M = Bimodule M
 
 open import Algebra.Construct.Sub.Group M.+ᴹ-group
-open import Algebra.Module.Structures using (IsBimodule)
-open import Algebra.Module.Morphism.Structures using (IsBimoduleMonomorphism)
-import Algebra.Module.Morphism.BimoduleMonomorphism as BimoduleMonomorphism
-open import Level using (suc; _⊔_)
 
 record Subbimodule cm′ ℓm′ : Set (cr ⊔ cs ⊔ cm ⊔ ℓm ⊔ suc (cm′ ⊔ ℓm′)) where
   field