diff --git a/Lattice.agda b/Lattice.agda
index c06b2bc..353e8d5 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -145,3 +145,14 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
         isLattice : IsLattice A _≈_ _⊔_ _⊓_
 
     open IsLattice isLattice public
+
+record FiniteHeightLattice {a} (A : Set a) : Set (lsuc a) where
+    field
+        height : ℕ
+        _≈_ : A → A → Set a
+        _⊔_ : A → A → A
+        _⊓_ : A → A → A
+
+        isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊔_
+
+    open IsFiniteHeightLattice isFiniteHeightLattice public