Let $X$ denote a non-empty set. Write $\mathcal{L}$ for the class of all ordered pairs $(L,f)$ where:
- $L$ is a linear poset (possibly empty), and
- $f$ is an arbitrary function $L \rightarrow X.$
Then $\mathcal{L}$ forms a "complete monoid." What I mean by this is that firstly, we can take products of infinitely many elements. In particular, for any linear poset $I$ and any family $\lambda:I \rightarrow\mathcal{L}$, write $\prod_{i \in I} \lambda_i$ for the concatenation of all the $\lambda_i$'s in the order determined by $\lambda$ and $I$. Secondly, (possibly) infinite products clearly satisfy some kind of infinitary associativity law. It should be of the form:
$$\prod_{i \in I}\prod_{j \in J(i)}(\lambda_i)_j = \prod_{\mathrm{something}}\mathrm{something}$$
Where:
- $I$ is an arbitrary linear poset
- $J(i)$ is a linear poset dependent on $i \in I$
- $(\lambda_i)_j$ is an element of $\cal L$ dependent on $i \in I$ and $j \in J(i)$.
Anyway, I'm having trouble writing down this law correctly.
Question. What is the correct statement of the infinitary associativity law?
Let's define the ordered sum of a poset-indexed family of posets!
The ordered sum of such a family $J = \{J(i)\}_{i \in I}$, which I shall denote by either $\bigoplus J$ or $\bigoplus_{i \in I} J(i)$, is the poset whose underlying set is
$$\bigoplus_{i \in I}J(i) = \{(i ,j)\mid i \in I \text{ and } j \in J(i)\}$$
and whose ordering $\le_{\oplus J}$ is defined lexicographically such that
$$(i, j) \le_{\bigoplus J} (k, l) \iff (i <_I k) \text{ or } (i = k \text{ and } j \le_{J(i)} l) $$
When $I$ is a linear poset and when each $J(i)$ is a linear poset, it is possible to verify that $\bigoplus J$ is a linear poset. In this case,
$$\prod_{i \in I}\prod_{j \in J(i)} (\lambda_i)_j = \prod_{(i, j) \in \bigoplus J} (\lambda_i)_j$$
Edit:
Note that the underlying set of $\bigoplus J$ is the set coproduct of the underlying sets of each $J(i)$. However, $\bigoplus J$ is not a poset coproduct of each $J(i)$.