diff --git a/Lattice/IterProd.agda b/Lattice/IterProd.agda
new file mode 100644
index 0000000..fec8993
--- /dev/null
+++ b/Lattice/IterProd.agda
@@ -0,0 +1,56 @@
+open import Lattice
+
+module Lattice.IterProd {a} {A B : Set a}
+    (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
+    (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
+    (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B)
+    (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
+
+open import Data.Nat using (ℕ; suc)
+open import Data.Product using (_×_)
+open import Utils using (iterate)
+
+IterProd : ℕ → Set a
+IterProd k = iterate k (λ t → A × t) B
+
+-- To make iteration more convenient, package the definitions in Lattice
+-- records, perform the recursion, and unpackage.
+
+private module _ where
+    ALattice : Lattice A
+    ALattice = record
+        { _≈_ = _≈₁_
+        ; _⊔_ = _⊔₁_
+        ; _⊓_ = _⊓₁_
+        ; isLattice = lA
+        }
+
+    BLattice : Lattice B
+    BLattice = record
+        { _≈_ = _≈₂_
+        ; _⊔_ = _⊔₂_
+        ; _⊓_ = _⊓₂_
+        ; isLattice = lB
+        }
+
+    IterProdLattice : ∀ {k : ℕ} → Lattice (IterProd k)
+    IterProdLattice {0} = BLattice
+    IterProdLattice {suc k'} = record
+        { _≈_ = _≈_
+        ; _⊔_ = _⊔_
+        ; _⊓_ = _⊓_
+        ; isLattice = isLattice
+        }
+        where
+            RightLattice : Lattice (IterProd k')
+            RightLattice = IterProdLattice {k'}
+
+            open import Lattice.Prod
+                _≈₁_ (Lattice._≈_ RightLattice)
+                _⊔₁_ (Lattice._⊔_ RightLattice)
+                _⊓₁_ (Lattice._⊓_ RightLattice)
+                lA  (Lattice.isLattice RightLattice)
+
+-- Expose the computed definition in public.
+module _ (k : ℕ) where
+    open Lattice.Lattice (IterProdLattice {k}) public