fix: tidy up

Author: jamesmckinna

src/Algebra/Construct/Sub/Ring/Ideal.agda

@@ -12,15 +12,14 @@ module Algebra.Construct.Sub.Ring.Ideal {c ℓ} (R : Ring c ℓ) where
 
 open import Algebra.Module.Construct.Sub.Bimodule using (Subbimodule)
 open import Algebra.Module.Construct.TensorUnit using (bimodule)
-open import Level
+open import Level using (suc; _⊔_)
 
 ------------------------------------------------------------------------
 -- Definition
 -- a (two sided) ideal is exactly a subbimodule of R considered as a bimodule over itself
 
 record Ideal c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
   field
-
     subbimodule : Subbimodule {R = R} bimodule c′ ℓ′
 
   open Subbimodule subbimodule public