diff --git a/Lattice.agda b/Lattice.agda
index 057f754..b6c61d8 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -187,3 +187,12 @@ private module NatInstances where
             ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
             }
         }
+
+    ProdSemilattice : {a : Level} → {A B : Set a} → {{ Semilattice A }} → {{ Semilattice B }} → Semilattice (A × B)
+    ProdSemilattice {a} {A} {B} {{slA}} {{slB}} = record
+        { _≼_ = λ (a₁ ,  b₁) (a₂ , b₂) → Semilattice._≼_ slA a₁ a₂ × Semilattice._≼_ slB b₁ b₂
+        ; _⊔_ = λ (a₁ ,  b₁) (a₂ , b₂) → (Semilattice._⊔_ slA a₁ a₂ , Semilattice._⊔_ slB b₁ b₂)
+        ; isSemilattice = record
+            {
+            }
+        }