More constructions of free commutative monoids

[vikraman]

We've got a few working now, but there are more ways to construct them we could try, and prove their universal property in our framework.

From here: https://drops.dagstuhl.de/opus/volltexte/2023/18395/pdf/LIPIcs-ITP-2023-20.pdf

• 3.2: as a quotient of lists by a permutation relation
• 3.3: as functions Fin n -> X quotiented by permutations

This second one is quite interesting, and there's some partial code in my repo.

From here: https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/papers/freshlists_aplas2023.pdf

• using fresh lists, and some assumptions on decidable equality(?)

[vikraman]

Association lists: https://github.com/agda/cubical/blob/master/Cubical/Relation/ZigZag/Applications/MultiSet.agda

• they don't prove the universal property, and assume decidable equality, we can try to see if it can be done without that assumption

[pufferffish]

Formalizing constructions that require decidable equality would involve changing the universal algebra framework so they are dropped, quotient of free monoid, quotient of lists by a permutation relation, and functions Fin n -> X quotiented by permutations have been formalized