diff --git a/Lattice/IterProd.agda b/Lattice/IterProd.agda
index e5d0856..6e03454 100644
--- a/Lattice/IterProd.agda
+++ b/Lattice/IterProd.agda
@@ -21,17 +21,14 @@ IterProd k = iterate k (λ t → A × t) B
 -- records, perform the recursion, and unpackage.
 
 private module _ where
-    BLattice : Lattice B
-    BLattice = record
+    lattice : ∀ {k : ℕ} → Lattice (IterProd k)
+    lattice {0} = record
         { _≈_ = _≈₂_
         ; _⊔_ = _⊔₂_
         ; _⊓_ = _⊓₂_
         ; isLattice = lB
         }
-
-    IterProdLattice : ∀ {k : ℕ} → Lattice (IterProd k)
-    IterProdLattice {0} = BLattice
-    IterProdLattice {suc k'} = record
+    lattice {suc k'} = record
         { _≈_ = _≈_
         ; _⊔_ = _⊔_
         ; _⊓_ = _⊓_
@@ -39,7 +36,7 @@ private module _ where
         }
         where
             Right : Lattice (IterProd k')
-            Right = IterProdLattice {k'}
+            Right = lattice {k'}
 
             open import Lattice.Prod
                 _≈₁_ (Lattice._≈_ Right)
@@ -48,7 +45,7 @@ private module _ where
                 lA  (Lattice.isLattice Right)
 
 module _ (k : ℕ) where
-    open Lattice.Lattice (IterProdLattice {k}) public
+    open Lattice.Lattice (lattice {k}) public
 
 module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
          (h₁ h₂ : ℕ)
@@ -67,8 +64,8 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
 
             open IsFiniteHeightLattice isFiniteHeightLattice public
 
-        BFiniteHeightLattice : FiniteHeightAndDecEq B
-        BFiniteHeightLattice = record
+        finiteHeightAndDec : ∀ {k : ℕ} → FiniteHeightAndDecEq (IterProd k)
+        finiteHeightAndDec {0} = record
             { height = h₂
             ; _≈_ = _≈₂_
             ; _⊔_ = _⊔₂_
@@ -79,10 +76,7 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
                 }
             ; ≈-dec = ≈₂-dec
             }
-
-        IterProdFiniteHeightLattice : ∀ {k : ℕ} → FiniteHeightAndDecEq (IterProd k)
-        IterProdFiniteHeightLattice {0} = BFiniteHeightLattice
-        IterProdFiniteHeightLattice {suc k'} = record
+        finiteHeightAndDec {suc k'} = record
             { height = h₁ + FiniteHeightAndDecEq.height Right
             ; _≈_ = P._≈_
             ; _⊔_ = P._⊔_
@@ -94,7 +88,7 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
             ; ≈-dec = ≈-dec ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
             }
             where
-                Right = IterProdFiniteHeightLattice {k'}
+                Right = finiteHeightAndDec {k'}
 
                 open import Lattice.Prod
                     _≈₁_ (FiniteHeightAndDecEq._≈_ Right)
@@ -103,10 +97,10 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
                     lA  (FiniteHeightAndDecEq.isLattice Right) as P
 
     module _ (k : ℕ) where
-        open FiniteHeightAndDecEq (IterProdFiniteHeightLattice {k}) using (isFiniteHeightLattice) public
+        open FiniteHeightAndDecEq (finiteHeightAndDec {k}) using (isFiniteHeightLattice) public
 
         private
-            FHD = IterProdFiniteHeightLattice {k}
+            FHD = finiteHeightAndDec {k}
 
         finiteHeightLattice : FiniteHeightLattice (IterProd k)
         finiteHeightLattice = record