diff --git a/Lattice.agda b/Lattice.agda
index 132ad0f..af572aa 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -24,6 +24,12 @@ record IsSemilattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A) : Set a where
 
+    _≼_ : A → A → Set a
+    a ≼ b = Σ A (λ c → (a ⊔ c) ≈ b)
+
+    _≺_ : A → A → Set a
+    a ≺ b = (a ≼ b) × (¬ a ≈ b)
+
     field
         ≈-equiv : IsEquivalence A _≈_
 
@@ -46,7 +52,7 @@ record IsLattice {a} (A : Set a)
         absorb-⊓-⊔ : (x y : A) → (x ⊓ (x ⊔ y)) ≈ x
 
     open IsSemilattice joinSemilattice public
-    open IsSemilattice meetSemilattice public hiding (≈-equiv; ≈-refl; ≈-sym; ≈-trans) renaming
+    open IsSemilattice meetSemilattice public using () renaming
         ( ⊔-assoc to ⊓-assoc
         ; ⊔-comm to ⊓-comm
         ; ⊔-idemp to ⊓-idemp
@@ -58,15 +64,9 @@ record IsFiniteHeightLattice {a} (A : Set a)
     (_⊔_ : A → A → A)
     (_⊓_ : A → A → A) : Set (lsuc a) where
 
-    _≼_ : A → A → Set a
-    a ≼ b = Σ A (λ c → (a ⊔ c) ≈ b)
-
-    _≺_ : A → A → Set a
-    a ≺ b = (a ≼ b) × (¬ a ≈ b)
-
     field
         isLattice : IsLattice A _≈_ _⊔_ _⊓_
-        fixedHeight : Height _≺_ h
+        fixedHeight : Height (IsLattice._≺_ isLattice) h
 
     open IsLattice isLattice public