diff --git a/Lattice.agda b/Lattice.agda
index bdd6a35..4d08965 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -77,6 +77,9 @@ record IsLattice {a} (A : Set a)
         ; ≼-refl to ≽-refl
         )
 
+    FixedHeight : ∀ (h : ℕ) → Set a
+    FixedHeight h = Chain.Height (_≈_) ≈-equiv _≺_ ≺-cong h
+
 record IsFiniteHeightLattice {a} (A : Set a)
     (h : ℕ)
     (_≈_ : A → A → Set a)
@@ -85,10 +88,11 @@ record IsFiniteHeightLattice {a} (A : Set a)
 
     field
         isLattice : IsLattice A _≈_ _⊔_ _⊓_
-        fixedHeight : Chain.Height (_≈_) (IsLattice.≈-equiv isLattice) (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice) h
 
     open IsLattice isLattice public
 
+    field
+        fixedHeight : FixedHeight h
 
 module _ {a b} {A : Set a} {B : Set b}
     (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where