diff --git a/Lattice/MapSet.agda b/Lattice/MapSet.agda
index 37b9e2c..c41de8c 100644
--- a/Lattice/MapSet.agda
+++ b/Lattice/MapSet.agda
@@ -12,7 +12,7 @@ private module UnitMap = Lattice.Map A ⊤ _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A
 open UnitMap using (Map)
 open UnitMap using
     ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_
-    ; isUnionSemilattice; isIntersectSemilattice; isLattice
+    ; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice
     ) public
 
 MapSet : Set a