diff --git a/Lattice.agda b/Lattice.agda
index 6c2f8b3..f5c1c5a 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -238,6 +238,9 @@ module IsSemilatticeInstances where
             _⊔_ : Map → Map → Map
             m₁ ⊔ m₂ = union _⊔₂_ m₁ m₂
 
+            _⊓_ : Map → Map → Map
+            m₁ ⊓ m₂ = intersect _⊔₂_ m₁ m₂
+
         module MapEquiv = IsEquivalenceInstances.ForMap A B ≡-dec-A _≈₂_ (IsSemilattice.≈-equiv sB)
 
         MapIsUnionSemilattice : IsSemilattice Map _≈_ _⊔_
@@ -248,6 +251,14 @@ module IsSemilatticeInstances where
             ; ⊔-idemp = union-idemp _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-idemp
             }
 
+        MapIsIntersectSemilattice : IsSemilattice Map _≈_ _⊓_
+        MapIsIntersectSemilattice = record
+            { ≈-equiv = MapEquiv.LiftEquivalence
+            ; ⊔-assoc = intersect-assoc _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-assoc
+            ; ⊔-comm = intersect-comm _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-comm
+            ; ⊔-idemp = intersect-idemp _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-idemp
+            }
+
 module IsLatticeInstances where
     module ForNat where
         open Nat