diff --git a/Lattice/IterProd.agda b/Lattice/IterProd.agda
index 14a29ae..dbfccad 100644
--- a/Lattice/IterProd.agda
+++ b/Lattice/IterProd.agda
@@ -98,6 +98,14 @@ module _ (k : ℕ) where
     open Everything (everything k) using (_≈_; _⊔_; _⊓_; isLattice) public
     open Lattice.IsLattice isLattice public
 
+    lattice : Lattice (IterProd k)
+    lattice = record
+        { _≈_ = _≈_
+        ; _⊔_ = _⊔_
+        ; _⊓_ = _⊓_
+        ; isLattice = isLattice
+        }
+
     module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
              (h₁ h₂ : ℕ)
              (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
@@ -117,3 +125,12 @@ module _ (k : ℕ) where
             { isLattice = isLattice
             ; fixedHeight = IsFiniteHeightAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
             }
+
+        finiteHeightLattice : FiniteHeightLattice (IterProd k)
+        finiteHeightLattice = record
+            { height = IsFiniteHeightAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
+            ; _≈_ = _≈_
+            ; _⊔_ = _⊔_
+            ; _⊓_ = _⊓_
+            ; isFiniteHeightLattice = isFiniteHeightLattice
+            }