fix

Author: jmougeot

src/Algebra/Lattice/Bundles.agda

@@ -18,10 +18,11 @@ module Algebra.Lattice.Bundles where
 open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Bundles using (Band)
 import Algebra.Lattice.Bundles.Raw as Raw
-open import Algebra.Lattice.Structures using
-  ( IsSemilattice; IsMeetSemilattice; IsJoinSemilattice
-  ; IsBoundedSemilattice; IsBoundedMeetSemilattice; IsBoundedJoinSemilattice
-  ; IsLattice; IsDistributiveLattice; IsBooleanAlgebra)
+open import Algebra.Lattice.Structures
+  using ( IsSemilattice; IsMeetSemilattice; IsJoinSemilattice
+        ; IsBoundedSemilattice; IsBoundedMeetSemilattice
+        ; IsBoundedJoinSemilattice; IsLattice; IsDistributiveLattice
+        ; IsBooleanAlgebra)
 open import Level using (suc; _⊔_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Core using (Rel)

src/Algebra/Module/Construct/Idealization.agda

@@ -40,8 +40,8 @@ module Algebra.Module.Construct.Idealization
 open import Algebra.Core using (Op₂)
 import Algebra.Consequences.Setoid as Consequences using (comm∧assoc⇒middleFour)
 import Algebra.Definitions as Definitions
-  using (Congruent₂; _DistributesOverˡ_; _DistributesOverʳ_; _DistributesOver_;
-  LeftIdentity; RightIdentity; Identity; Associative)
+  using (Congruent₂; _DistributesOverˡ_; _DistributesOverʳ_; _DistributesOver_
+        ; LeftIdentity; RightIdentity; Identity; Associative)
 import Algebra.Module.Construct.DirectProduct as DirectProduct using (bimodule)
 import Algebra.Module.Construct.TensorUnit as TensorUnit using (bimodule)
 open import Algebra.Structures using (IsAbelianGroup; IsRing)

src/Algebra/Module/Construct/TensorUnit.agda

@@ -12,13 +12,13 @@
 module Algebra.Module.Construct.TensorUnit where
 
 open import Algebra.Bundles
-  using (RawSemiring; RawRing; Semiring; Ring; CommutativeSemiring;
-  CommutativeRing)
+  using (RawSemiring; RawRing; Semiring; Ring; CommutativeSemiring
+        ; CommutativeRing)
 open import Algebra.Module.Bundles
-  using (RawSemimodule; RawLeftSemimodule; RawRightSemimodule; RawBisemimodule;
-  RawLeftModule; RawRightModule; RawBimodule; RawModule; LeftSemimodule;
-  RightSemimodule; Bisemimodule; Semimodule; LeftModule; RightModule; Bimodule;
-  Module)
+  using (RawSemimodule; RawLeftSemimodule; RawRightSemimodule; RawBisemimodule
+        ; RawLeftModule; RawRightModule; RawBimodule; RawModule; LeftSemimodule
+        ; RightSemimodule; Bisemimodule; Semimodule; LeftModule; RightModule; Bimodule
+        ; Module)
 open import Level  using (Level; _⊔_)
 
 private

src/Algebra/Module/Construct/Zero.agda

@@ -89,4 +89,3 @@ bimodule = record { ℤero }
 
 ⟨module⟩ : {R : CommutativeRing r ℓr} → Module R c ℓ
 ⟨module⟩ = record { ℤero }
-