[posterboy]

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 *?

[lmm]

You need to be able to write the group axioms down, so you need to distinguish the three elements. E.g. one of the axioms is 1 ∈ G, which means something very different from G ∈ 1. It all bottoms out in set theory, but (G, 1, X) really is a different set from (G, X, 1) (e.g. they might be represented as the sets {{G, 1, X}, {G, 1}, {G}} and {{G, 1, X}, {G, X}, {G}} respectively) so you do need to decide which is the "canonical" representation of that group, or else you need a rule that allows you to tell whether two different sets are representations of the same group.

[jsprogrammer]

Everything (written, anyway) contains an order.

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)

[1] https://en.m.wikipedia.org/wiki/Multiset