diff --git a/src/Algebra/Lattice/Bundles/Raw.agda b/src/Algebra/Lattice/Bundles/Raw.agda
index 8b5501cb72..9a8c4a2d22 100644
--- a/src/Algebra/Lattice/Bundles/Raw.agda
+++ b/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)
diff --git a/src/Algebra/Lattice/Construct/NaturalChoice/MaxOp.agda b/src/Algebra/Lattice/Construct/NaturalChoice/MaxOp.agda
index 4d00c28524..b646dc5914 100644
--- a/src/Algebra/Lattice/Construct/NaturalChoice/MaxOp.agda
+++ b/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)
 
diff --git a/src/Algebra/Lattice/Construct/NaturalChoice/MinMaxOp.agda b/src/Algebra/Lattice/Construct/NaturalChoice/MinMaxOp.agda
index b574147807..a191d254e6 100644
--- a/src/Algebra/Lattice/Construct/NaturalChoice/MinMaxOp.agda
+++ b/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
 
 ------------------------------------------------------------------------
diff --git a/src/Algebra/Lattice/Construct/NaturalChoice/MinOp.agda b/src/Algebra/Lattice/Construct/NaturalChoice/MinOp.agda
index ac4328ded3..008627e42d 100644
--- a/src/Algebra/Lattice/Construct/NaturalChoice/MinOp.agda
+++ b/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