diff --git a/Lattice/IterProd.agda b/Lattice/IterProd.agda
index dbfccad..8eb1ec2 100644
--- a/Lattice/IterProd.agda
+++ b/Lattice/IterProd.agda
@@ -11,8 +11,8 @@ module Lattice.IterProd {a} {A B : Set a}
     (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
 open import Agda.Primitive using (lsuc)
-open import Data.Nat using (ℕ; suc; _+_)
-open import Data.Product using (_×_)
+open import Data.Nat using (ℕ; zero; suc; _+_)
+open import Data.Product using (_×_; _,_; proj₁; proj₂)
 open import Utils using (iterate)
 
 open IsLattice lA renaming (FixedHeight to FixedHeight₁)
@@ -30,31 +30,50 @@ IterProd k = iterate k (λ t → A × t) B
 -- that are built up by the two iterations. So, do everything in one iteration.
 -- This requires some odd code.
 
+build : A → B → (k : ℕ) → IterProd k
+build _ b zero = b
+build a b (suc s) = (a , build a b s)
+
 private
     record RequiredForFixedHeight : Set (lsuc a) where
-         field
+        field
             ≈₁-dec : IsDecidable _≈₁_
             ≈₂-dec : IsDecidable _≈₂_
             h₁ h₂ : ℕ
             fhA : FixedHeight₁ h₁
             fhB : FixedHeight₂ h₂
 
-    record IsFiniteHeightAndDecEq {A : Set a} {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) : Set (lsuc a) where
+        ⊥₁ : A
+        ⊥₁ = proj₁ (proj₁ (proj₁ fhA))
+
+        ⊥₂ : B
+        ⊥₂ = proj₁ (proj₁ (proj₁ fhB))
+
+        ⊥k : ∀ (k : ℕ) → IterProd k
+        ⊥k = build ⊥₁ ⊥₂
+
+    record IsFiniteHeightWithBotAndDecEq {A : Set a} {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) (⊥ : A) : Set (lsuc a) where
         field
             height : ℕ
             fixedHeight : IsLattice.FixedHeight isLattice height
             ≈-dec : IsDecidable _≈_
 
-    record Everything (A : Set a) : Set (lsuc a) where
+            ⊥-correct : proj₁ (proj₁ (proj₁ fixedHeight)) ≈ ⊥
+
+    record Everything (k : ℕ) : Set (lsuc a) where
+        T = IterProd k
+
         field
-            _≈_ : A → A → Set a
-            _⊔_ : A → A → A
-            _⊓_ : A → A → A
+            _≈_ : T → T → Set a
+            _⊔_ : T → T → T
+            _⊓_ : T → T → T
 
-            isLattice : IsLattice A _≈_ _⊔_ _⊓_
-            isFiniteHeightIfSupported : RequiredForFixedHeight → IsFiniteHeightAndDecEq isLattice
+            isLattice : IsLattice T _≈_ _⊔_ _⊓_
+            isFiniteHeightIfSupported :
+                ∀ (req : RequiredForFixedHeight) →
+                IsFiniteHeightWithBotAndDecEq isLattice (RequiredForFixedHeight.⊥k req k)
 
-    everything : ∀ (k : ℕ) → Everything (IterProd k)
+    everything : ∀ (k : ℕ) → Everything k
     everything 0 = record
         { _≈_ = _≈₂_
         ; _⊔_ = _⊔₂_
@@ -64,6 +83,7 @@ private
             { height = RequiredForFixedHeight.h₂ req
             ; fixedHeight = RequiredForFixedHeight.fhB req
             ; ≈-dec = RequiredForFixedHeight.≈₂-dec req
+            ; ⊥-correct = IsLattice.≈-refl lB
             }
         }
     everything (suc k') = record
@@ -76,13 +96,14 @@ private
                 fhlRest = Everything.isFiniteHeightIfSupported everythingRest req
             in
                 record
-                    { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightAndDecEq.height fhlRest
+                    { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightWithBotAndDecEq.height fhlRest
                     ; fixedHeight =
                         P.fixedHeight
-                        (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
-                        (RequiredForFixedHeight.h₁ req) (IsFiniteHeightAndDecEq.height fhlRest)
-                        (RequiredForFixedHeight.fhA req) (IsFiniteHeightAndDecEq.fixedHeight fhlRest)
-                    ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
+                        (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
+                        (RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest)
+                        (RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest)
+                    ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
+                    ; ⊥-correct = (IsLattice.≈-refl lA , IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest)
                     }
         }
         where
@@ -121,14 +142,16 @@ module _ (k : ℕ) where
                 ; fhB = fhB
                 }
 
+        fixedHeight = IsFiniteHeightWithBotAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
+
         isFiniteHeightLattice = record
             { isLattice = isLattice
-            ; fixedHeight = IsFiniteHeightAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
+            ; fixedHeight = fixedHeight
             }
 
         finiteHeightLattice : FiniteHeightLattice (IterProd k)
         finiteHeightLattice = record
-            { height = IsFiniteHeightAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
+            { height = IsFiniteHeightWithBotAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
             ; _≈_ = _≈_
             ; _⊔_ = _⊔_
             ; _⊓_ = _⊓_