Unordered pairs in Homotopy Type Theory
The type of unordered pairs in a type $A$ is defined to be $$\sum_{(X:\mathcal{U})}\sum_{(H:\|X\simeq \mathsf{bool}\|)}A^X.$$ In other words, an undordered pair in $A$ is simply a map $X\to A$ from a type $X$ that merely has two elements.

Note that in general, this is not a set, because the type of 2-element types is not a set but a 1-type. The way to think about this is that unordered pairs have some symmetries (swapping the order of the elements in the unordered pairs) that should be taken into account in homotopy type theory.

Note that the type of unordered pairs can also be used to define the type of fully coherent commutative binary operations on a type $A$. This type is simply $$\Big(\sum_{(X:\mathcal{U})}\sum_{(H:\|X\simeq\mathsf{bool}\|)}A^X\Big)\to A.$$
In other words, a fully coherent commutative binary operation on $A$ is an operation on the unordered pairs of $A$.