diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda
index 30e1ea3..6056e30 100644
--- a/Lattice/AboveBelow.agda
+++ b/Lattice/AboveBelow.agda
@@ -279,6 +279,14 @@ module Plain where
         ; absorb-⊓-⊔ = absorb-⊓-⊔
         }
 
+    lattice : Lattice AboveBelow
+    lattice = record
+        { _≈_ = _≈_
+        ; _⊔_ = _⊔_
+        ; _⊓_ = _⊓_
+        ; isLattice = isLattice
+        }
+
     open IsLattice isLattice using (_≼_; _≺_)
 
     ⊥≺[x] : ∀ (x : A) → ⊥ ≺ [ x ]
@@ -329,3 +337,12 @@ module Plain where
             { isLattice = isLattice
             ; fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest)
             }
+
+        finiteHeightLattice : FiniteHeightLattice AboveBelow
+        finiteHeightLattice = record
+            { height = 2
+            ; _≈_ = _≈_
+            ; _⊔_ = _⊔_
+            ; _⊓_ = _⊓_
+            ; isFiniteHeightLattice = isFiniteHeightLattice
+            }