Unordered pairs in Homotopy Type Theory

Question

It's conceptually simple to state what an "unordered pair" is supposed to be in set theory. Yet, in homotopy type theory I have trouble formalizing this. A first naive try in agda syntax:

data UPair (A : Type ℓ) : Type ℓ where
  mkpair : (x y : A) → UPair A
  uswap : ∀ a b → mkpair a b ≡ mkpair b a

This fails, since there are actually two different paths between e.g. mkpair 1 2 and mkpair 2 1, that is we have uswap 1 2 and sym (uswap 2 1). Again, these can be forced equal by a one-higher path constructor, but one would have to continue for ever.

Obviously, if A is an n-truncated type, we can stop at some point. Generally truncating at some level fails because it might forget some non-trivial paths in A. Take for example the set-truncation of the above type and A = S¹, the circle, then the path i. mkpair (loop i) base is lost and identified with refl (mkpair base base).

Can we generally write down the type of unordered pairs of a parameter A : Type ℓ? Can the resulting type live inside the universe ℓ?

---

Clarification:

Let A· = (A , a) be a pointed type. Define UPA· = (UPair A, mkpair a a) as a pointed type. I would then expect Ωₜ UPA· ≡ UPair (Ωₜ A·). These correspond to singleton sets.

Let A∙ = (A, a, b) be a bipointed type with a ≢ b. Then I expect that the map (a ≡ a) × (b ≡ b) → mkpair a b ≡ mkpair b a given by (pa , pb) → (λ i → mkpair (pa i) (pb i)) ∙ uswap a b is an equivalence.

Answer 1

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$.

Answer 2

The set of unordered pairs of A can be defined using a higher-inductive type with set-truncation, just as you suggested, somewhat like this (I am writing this off the top of my head without verifying it in Agda, but you'll get the point):

data UPair (A : Type ℓ) : Type ℓ where
  mkpair : (x y : A) → UPair A
  uswap : ∀ a b → mkpair a b ≡ mkpair b a
  trunc : ∀ (u v : UPair A) (p q : u ≡ v) → p ≡ q

It is obvious that UPair A is a set (is a $0$-type) because trunc directly witnessess this fact. You do not have to add any higher-path constructors.