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.

翻译：我们在同伦类型论中发展了有限多重集的构造性理论，将其定义为自由交换幺半群。在回顾自由交换幺半群构造的基本结构性质之后，我们使用1-HIT形式化并建立了两种必然等价的自由交换幺半群代数表示的范畴泛性质。这些表示对应两个包含交换公理的不同等式理论。在此框架下，我们证明了有限多重集的重要结构组合性质。这些性质在不假设载体集具有可判等性的完全一般性下得以建立。作为应用，我们给出了经典线性逻辑关系模型及其微分结构的构造性形式化。由此构造性地确立了自由交换幺半群是锥形精炼幺半群。进而我们获得了有限多重集相等类型的特征刻画，以及将自由交换幺半群构造作为列表构造的集合商的新的表示。这些发展关键依赖于与自由交换幺半群构造（视为组合Fock空间）相关联的产生/湮灭算子的交换关系。