4.3 The set \(\leftrightarrow \) seq bridges
The cd-index machinery in Chapters 2–3 operates on \(\mathrm{seq}\, \mathbb {N}\). The bridges below let us apply it to finset-level objects.
For \(D \subseteq \{ 0, \dots , n-1\} \), \(\texttt{set\_ to\_ seq}(D) = \mathrm{sort}\, (\leq , [\, \mathrm{val}(i) : i \in \mathrm{enum}(D)\, ])\) is the sorted list of underlying naturals of elements of \(D\).
For \(k \in \{ 0, \dots , m-1\} \) and \(D \subseteq \{ 0, \dots , m\} \),
This identifies the finset-level \(\omega (\) with the seq-level \()\texttt{omega\_ seq}\), letting the heavy machinery in \(\texttt{psi\_ cdindex\_ *.v}\) apply to \(\{ \, \texttt{set}\, \} \)-style consumers.
\(\texttt{omega\_ seq}(s)\) is the seq-level analogue of \(\omega (D)\): it lists positions \(k\) such that exactly one of \(\{ k, k+1\} \) appears in \(s\). It is the computational backbone of the omega map and the bridge between \(\omega (\) and bit-strings.