List/permutation ≃ FreeComMonoid

[marcinjangrzybowski]

• basic properties of permutations (defined as FinData.Fin n ≃ FinData.Fin m)
• ↔ - equivalence relation of "being a permutation of" on List
• List/↔ ≃ FreeComMonoid (via isomorphism of List/↔ and FiniteMultiset)

[mzeuner]

This looks cool and I'm also interested to see how this relates to groupoid truncation.

Did you see that we have another relation on lists that gives you finite multisets in the quotient: https://github.com/agda/cubical/blob/master/Cubical/Relation/ZigZag/Applications/MultiSet.agda

This relation arises automatically from the multiset structure on lists and the functional relation to association lists, but when you unfold it essentially relates two lists that contain the same elements with the same multiplicity. Do you think it would be hard to prove that the two relations are logically equivalent?

[marcinjangrzybowski]

Do you think it would be hard to prove that the two relations are logically equivalent?

I do not expect it to be hard since the other relation brings Discreate A to the table, with this _↔_ relations become decidable.

I will include, proof, thanks for the idea!