  We develop a constructive theory of finite multisets in Homotopy Type Theory,
defining them as free commutative monoids. After recalling basic structural
properties of the free commutative-monoid construction, we formalise and
establish the categorical universal property of two, necessarily equivalent,
algebraic presentations of free commutative monoids using 1-HITs. These
presentations correspond to two different equational theories invariably
including commutation axioms. In this setting, we prove important structural
combinatorial properties of finite multisets. These properties are established
in full generality without assuming decidable equality on the carrier set.
  As an application, we present a constructive formalisation of the relational
model of classical linear logic and its differential structure. This leads to
constructively establishing that free commutative monoids are conical
refinement monoids. Thereon we obtain a characterisation of the equality type
of finite multisets and a new presentation of the free commutative-monoid
construction as a set-quotient of the list construction. These developments
crucially rely on the commutation relation of creation/annihilation operators
associated with the free commutative-monoid construction seen as a
combinatorial Fock space.
