Free Commutative Monoids in Homotopy Type Theory

We develop a constructive theory of finite multisets, defining them as free commutative monoids in Homotopy Type Theory. We formalise two algebraic presentations of this construction using 1-HITs, establishing the universal property for each and thereby their equivalence. These presentations correspond to equational theories including a commutation axiom. In this setting, we prove important structural combinatorial properties of singleton multisets arising from concatenations and projections of multisets. This is done in generality, without assuming decidable equality on the carrier set. Further, as applications, we present a constructive formalisation of the relational model of differential linear logic and use it to characterise the equality type of multisets. This leads us to the introduction of a novel conditional equational presentation of the finite-multiset construction.