Unordered pairs in Homotopy Type Theory

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.

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

• Another application of the same idea is the type of non-planar binary trees: it is the inductive type $T$ equipped with a base point $r:T$ and an operation $\mathsf{unordered{-}pairs}(T)\to T$ Apr 12, 2020 at 19:02
• At first sight, this seems like a straightforward definition with the correct paths, at least I think I can see how to define mkpair and a better version of uswap that doesn't have the problems I had. Very insightful. This generalizes to n-tuples (and other container types) where equivalence is permutations?! Apr 12, 2020 at 19:13
• It generalizes indeed. The type of unordered lists of elements in $A$ is defined to be $S(A):=\sum_{X:\mathbb{F}}A^X$ where $\mathbb{F}$ is the type of all merely finite types. The type $S(A)$ should be the free symmetric monoid on $A$, although to state that, you'd have to solve an infinite coherence problem. Apr 12, 2020 at 19:37
• Nevertheless, you can still pretty easily define some of the low-dimensional structure on $S(A)$, that you'd expect from the free symmetric monoid. Apr 12, 2020 at 19:40

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.

• Maybe I'm overthinking. This is somewhat unsatisfactory since UPair A ≡ UPair ∥ A ∥₀ for any A, so it is the set of unordered sets (though perfectly good for that). Apr 12, 2020 at 12:15
• If A is not a set, then what do you expect UPair A to be, mathematically speaking? For instance, what is UPair S¹? Apr 12, 2020 at 14:11
• Since the loop space Ω S¹ is Int, I would expect Ω (UPair S¹) to be UPair Int. Apr 12, 2020 at 14:23
• UPair S¹ should be like the torus S¹ x S¹ but you can swap the two directions "up" and "around". Apr 12, 2020 at 14:29
• Naive informal descriptions do not reveal what higher-path structure you might be thinking of. What does this "swap" mean, are you talking about a homotopy pushout of some sort, or what? For instance, would you expect UPair A to have the same truncation level as A? Apr 12, 2020 at 14:37