diff --git a/lean/Spa/Lattice/IterProd.lean b/lean/Spa/Lattice/IterProd.lean
index 6ebe692..ca442c3 100644
--- a/lean/Spa/Lattice/IterProd.lean
+++ b/lean/Spa/Lattice/IterProd.lean
@@ -1,6 +1,24 @@
 import Spa.Lattice.Prod
 import Spa.Lattice.Unit
 
+/-!
+
+# Iterated Products
+
+Given two types $\alpha$ and $\beta$ and a number $n$, produces
+an iterated product:
+
+$$
+\overbrace{\alpha \times \ldots \times \alpha}^{n\ \text{times}} × \beta
+$$
+
+This is mostly a stepping stone for isomorphisms. In
+`Spa/Lattice/Prod.lean`, By decomposing types such as `Fin n → α` into
+`IterProd α PUnit n`, we can automatically get a proof of their finite
+height via `Spa.FiniteHeightLattice.transport`.
+
+-/
+
 namespace Spa
 
 universe u