diff --git a/Lattice/Unit.agda b/Lattice/Unit.agda
index d736dbe..c16bcc5 100644
--- a/Lattice/Unit.agda
+++ b/Lattice/Unit.agda
@@ -89,6 +89,14 @@ isLattice = record
     ; absorb-⊓-⊔ = absorb-⊓-⊔
     }
 
+lattice : Lattice ⊤
+lattice = record
+    { _≈_ = _≈_
+    ; _⊔_ = _⊔_
+    ; _⊓_ = _⊓_
+    ; isLattice = isLattice
+    }
+
 open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice)
 
 private
@@ -104,3 +112,12 @@ isFiniteHeightLattice = record
     { isLattice = isLattice
     ; fixedHeight = (((tt , tt) , longestChain) , isLongest)
     }
+
+finiteHeightLattice : FiniteHeightLattice ⊤
+finiteHeightLattice = record
+    { height = 0
+    ; _≈_ = _≈_
+    ; _⊔_ = _⊔_
+    ; _⊓_ = _⊓_
+    ; isFiniteHeightLattice = isFiniteHeightLattice
+    }