alegbra.definitions (#2601)

Author: jmougeot

src/Algebra/Definitions/RawMonoid.agda

@@ -7,11 +7,11 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles using (RawMonoid)
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
-open import Data.Vec.Functional as Vector using (Vector)
 
 module Algebra.Definitions.RawMonoid {a ℓ} (M : RawMonoid a ℓ) where
 
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
+open import Data.Vec.Functional as Vector using (Vector)
 open RawMonoid M renaming ( _∙_ to _+_ ; ε to 0# )
 
 ------------------------------------------------------------------------

src/Algebra/Definitions/RawSemiring.agda

@@ -7,13 +7,13 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles using (RawSemiring)
+
+module Algebra.Definitions.RawSemiring {a ℓ} (M : RawSemiring a ℓ) where
+
 open import Data.Sum.Base using (_⊎_)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Level using (_⊔_)
 open import Relation.Binary.Core using (Rel)
-
-module Algebra.Definitions.RawSemiring {a ℓ} (M : RawSemiring a ℓ) where
-
 open RawSemiring M renaming (Carrier to A)
 
 ------------------------------------------------------------------------