diff --git a/Lattice/MapSet.agda b/Lattice/MapSet.agda
index c41de8c..17285da 100644
--- a/Lattice/MapSet.agda
+++ b/Lattice/MapSet.agda
@@ -5,15 +5,25 @@ open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 
 module Lattice.MapSet {a : Level} (A : Set a) (≡-dec-A : Decidable (_≡_ {a} {A})) where
 
-open import Lattice.Unit using (⊤) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice)
+open import Data.List using (List; map)
+open import Data.Product using (proj₁)
+open import Function using (_∘_)
+
+open import Lattice.Unit using (⊤; tt) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice)
 import Lattice.Map
 
 private module UnitMap = Lattice.Map A ⊤ _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A ⊤-isLattice
 open UnitMap using (Map)
 open UnitMap using
-    ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_
+    ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_; empty
     ; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice
     ) public
 
 MapSet : Set a
 MapSet = Map
+
+to-List : MapSet → List A
+to-List = map proj₁ ∘ proj₁
+
+insert : A → MapSet → MapSet
+insert k = UnitMap.insert k tt