diff --git a/Analysis/Forward/Lattices.agda b/Analysis/Forward/Lattices.agda
index 9b28a5f..9ac2f1b 100644
--- a/Analysis/Forward/Lattices.agda
+++ b/Analysis/Forward/Lattices.agda
@@ -55,12 +55,7 @@ open VariableValuesFiniteMap
         ; ∈k-dec to ∈k-decᵛ
         ; all-equal-keys to all-equal-keysᵛ
         ; Provenance-union to Provenance-unionᵛ
-        )
-    public
-open IsLattice isLatticeᵛ
-    using ()
-    renaming
-        ( ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
+        ; ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
         ; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
         ; ⊔-idemp to ⊔ᵛ-idemp
         )
diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda
index 4d0721c..47609f2 100644
--- a/Analysis/Sign.agda
+++ b/Analysis/Sign.agda
@@ -78,10 +78,9 @@ open AB.Plain 0ˢ using ()
         ; _≼_ to _≼ᵍ_
         ; _⊔_ to _⊔ᵍ_
         ; _⊓_ to _⊓ᵍ_
+        ; ≼-trans to ≼ᵍ-trans
         )
 
-open IsLattice isLatticeᵍ using () renaming (≼-trans to ≼ᵍ-trans)
-
 plus : SignLattice → SignLattice → SignLattice
 plus ⊥ᵍ _ = ⊥ᵍ
 plus _ ⊥ᵍ = ⊥ᵍ
diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda
index 5532e7e..9472414 100644
--- a/Lattice/AboveBelow.agda
+++ b/Lattice/AboveBelow.agda
@@ -321,7 +321,7 @@ module Plain (x : A) where
             ; isLattice = isLattice
             }
 
-    open IsLattice isLattice using (_≼_; _≺_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
+    open IsLattice isLattice using (_≼_; _≺_; ≼-trans; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
 
     ⊥≺[x] : ∀ (x : A) → ⊥ ≺ [ x ]
     ⊥≺[x] x = (≈-refl , λ ())
diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda
index 4692b89..25240ae 100644
--- a/Lattice/FiniteMap.agda
+++ b/Lattice/FiniteMap.agda
@@ -184,7 +184,7 @@ private module WithKeys (ks : List A) where
             ; isLattice = isLattice
             }
 
-    open IsLattice isLattice using (_≼_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
+    open IsLattice isLattice using (_≼_; ⊔-idemp; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
 
     m₁≼m₂⇒m₁[k]≼m₂[k] : ∀ (fm₁ fm₂ : FiniteMap) {k : A} {v₁ v₂ : B} →
                         fm₁ ≼ fm₂ → (k , v₁) ∈ fm₁ → (k , v₂) ∈ fm₂ → v₁ ≼₂ v₂
diff --git a/Lattice/Prod.agda b/Lattice/Prod.agda
index b5c9628..52793a6 100644
--- a/Lattice/Prod.agda
+++ b/Lattice/Prod.agda
@@ -106,6 +106,8 @@ instance
         ; isLattice = isLattice
         }
 
+open IsLattice isLattice using (_≼_; _≺_; ≺-cong) public
+
 module _ {{≈₁-Decidable : IsDecidable _≈₁_}} {{≈₂-Decidable : IsDecidable _≈₂_}} where
     open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec)
     open IsDecidable ≈₂-Decidable using () renaming (R-dec to ≈₂-dec)
@@ -125,7 +127,6 @@ module _ {{≈₁-Decidable : IsDecidable _≈₁_}} {{≈₂-Decidable : IsDeci
              {{fhA : FixedHeight₁ h₁}} {{fhB : FixedHeight₂ h₂}} where
 
         open import Data.Nat.Properties
-        open IsLattice isLattice using (_≼_; _≺_; ≺-cong)
 
         module ChainMapping₁ = ChainMapping joinSemilattice₁ isJoinSemilattice
         module ChainMapping₂ = ChainMapping joinSemilattice₂ isJoinSemilattice