A Fresh Look at Commutativity: Free Algebraic Structures via Fresh Lists

We show how types of free idempotent commutative monoids and free commutative monoids can be constructed in ordinary dependent type theory, without the need for quotient types or setoids, and prove that these constructions realise finite sets and multisets, respectively. Both constructions arise as generalisations of C. Coquand's data type of fresh lists. We also show how many other free structures also can be realised by other instantiations. All of our results have been formalised in Agda.