Free Commutative Monoids in Homotopy Type Theory