The second comment in the discussion is confusing. What's the significance of the order in the tuple? An unordered set should be enough, so the tuples would be obvious permutations. Is the order decoded in the elements, eg. the operator *?
The comment says that you may want to treat the same things in different orders as being the same "thing".
A better, in my opinion, English translation of the univalence axiom is, "identity is equivalent to equivalency" (formally, [(A=B)~(A~B)]). You can find this translation in the HoTT book[0].
Also, check out multisets[1].
[0] http://saunders.phil.cmu.edu/book/hott-online.pdf (PDF page 16, or book page 4)