diff --git a/Lattice.agda b/Lattice.agda
index 353e8d5..54d6dbc 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -153,6 +153,6 @@ record FiniteHeightLattice {a} (A : Set a) : Set (lsuc a) where
         _⊔_ : A → A → A
         _⊓_ : A → A → A
 
-        isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊔_
+        isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
 
     open IsFiniteHeightLattice isFiniteHeightLattice public