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