diff --git a/Lattice/Map.agda b/Lattice/Map.agda
index 980fe4e..4db7709 100644
--- a/Lattice/Map.agda
+++ b/Lattice/Map.agda
@@ -882,6 +882,14 @@ isLattice = record
     ; absorb-⊓-⊔ = absorb-⊓-⊔
     }
 
+lattice : Lattice Map
+lattice = record
+    { _≈_ = _≈_
+    ; _⊔_ = _⊔_
+    ; _⊓_ = _⊓_
+    ; isLattice = isLattice
+    }
+
 ⊔-equal-keys : ∀ {m₁ m₂ : Map} → keys m₁ ≡ keys m₂ → keys m₁ ≡ keys (m₁ ⊔ m₂)
 ⊔-equal-keys km₁≡km₂ = union-equal-keys km₁≡km₂