diff --git a/Lattice/IterProd.agda b/Lattice/IterProd.agda
index 6e03454..00cbe43 100644
--- a/Lattice/IterProd.agda
+++ b/Lattice/IterProd.agda
@@ -20,7 +20,7 @@ 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
+module _ where
     lattice : ∀ {k : ℕ} → Lattice (IterProd k)
     lattice {0} = record
         { _≈_ = _≈₂_