cleaning import Lattice 1 (#2602)

* Cleaning import Lattice 1

* Cleaning import Lattice 1

* Cleaning import Lattice 1

* import cleaning

Author: jmougeot

src/Algebra/Lattice/Bundles/Raw.agda

@@ -8,7 +8,7 @@
 
 module Algebra.Lattice.Bundles.Raw where
 
-open import Algebra.Core
+open import Algebra.Core using (Op₂)
 open import Algebra.Bundles.Raw using (RawMagma)
 open import Level using (suc; _⊔_)
 open import Relation.Binary.Core using (Rel)

src/Algebra/Lattice/Construct/NaturalChoice/MaxOp.agda

@@ -8,13 +8,15 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Construct.NaturalChoice.Base
-import Algebra.Lattice.Construct.NaturalChoice.MinOp as MinOp
+  using (MaxOperator; MaxOp⇒MinOp)
 open import Relation.Binary.Bundles using (TotalPreorder)
 
 module Algebra.Lattice.Construct.NaturalChoice.MaxOp
   {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (maxOp : MaxOperator O)
   where
 
+import Algebra.Lattice.Construct.NaturalChoice.MinOp as MinOp
+
 private
   module Min = MinOp (MaxOp⇒MinOp maxOp)
 

src/Algebra/Lattice/Construct/NaturalChoice/MinMaxOp.agda

@@ -6,8 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Lattice.Bundles
-open import Algebra.Construct.NaturalChoice.Base
+open import Algebra.Construct.NaturalChoice.Base using (MinOperator; MaxOperator)
 open import Relation.Binary.Bundles using (TotalPreorder)
 
 module Algebra.Lattice.Construct.NaturalChoice.MinMaxOp
@@ -22,6 +21,7 @@ open MaxOperator maxOp
 
 open import Algebra.Lattice.Structures _≈_
 open import Algebra.Construct.NaturalChoice.MinMaxOp minOp maxOp
+open import Algebra.Lattice.Bundles using (Lattice; DistributiveLattice)
 open import Relation.Binary.Reasoning.Preorder preorder
 
 ------------------------------------------------------------------------

src/Algebra/Lattice/Construct/NaturalChoice/MinOp.agda

@@ -7,9 +7,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Bundles
-open import Algebra.Lattice.Bundles
-open import Algebra.Construct.NaturalChoice.Base
+open import Algebra.Construct.NaturalChoice.Base using (MinOperator)
 open import Relation.Binary.Bundles using (TotalPreorder)
 
 module Algebra.Lattice.Construct.NaturalChoice.MinOp
@@ -18,8 +16,9 @@ module Algebra.Lattice.Construct.NaturalChoice.MinOp
 open TotalPreorder O
 open MinOperator minOp
 
-open import Algebra.Lattice.Structures _≈_
 open import Algebra.Construct.NaturalChoice.MinOp minOp
+open import Algebra.Lattice.Bundles using (Semilattice)
+open import Algebra.Lattice.Structures _≈_
 
 ------------------------------------------------------------------------
 -- Structures