In this talk, I will discuss various presentations of finite multisets
as free commutative monoids using higher inductive types in HoTT, and
prove their universal property. Using this, I will construct the
relational model of linear logic, and further show its differential
structure.