diff --git a/src/Data/FiniteMultiset.ard b/src/Data/FiniteMultiset.ard
new file mode 100644
index 00000000..ef273fa9
--- /dev/null
+++ b/src/Data/FiniteMultiset.ard
@@ -0,0 +1,28 @@
+\import Algebra.Meta
+\import Paths
+
+\truncated \data FMSet (A : \Type) : \Set
+  | nil
+  | \infixr 5 :: A (FMSet A)
+  | comm (a b : A) (s : FMSet A) : a :: b :: s = b :: a :: s
+
+\func \infixr 6 ++ {A : \Type} (s t : FMSet A) : FMSet A \elim s
+  | nil => t
+  | :: x xs => x :: (xs ++ t)
+  | comm a b s i => comm a b (s ++ t) i
+
+\func ++_nil {A : \Type} (s : FMSet A) : s = s ++ nil
+  | nil => idp
+  | :: x xs => pmap _ (++_nil xs)
+
+\func ++-assoc {A : \Type} (s t u : FMSet A) : (s ++ t) ++ u = s ++ (t ++ u) \elim s
+  | nil => idp
+  | :: x xs => \let p => ++-assoc xs t u \in cong
+
+\func ++-cons {A : \Type} (x : A) (s : FMSet A) : x :: s = s ++ (x :: nil) \elim s
+  | nil => idp
+  | :: a s => \let p => ++-cons x s \in path (comm x a s) *> cong
+
+\func ++-comm {A : \Type} {s t : FMSet A} : s ++ t = t ++ s \elim s
+  | nil => ++_nil t
+  | :: x xs => pmap (x ::) ++-comm *> pmap (__ ++ xs) (++-cons x t) *> ++-assoc _ (_ :: nil) _