Jonathan, thanks for
>Thus, M× can't be defined independent of any particular order.

I got lost among 3 trees, and all these is tightly bound to what comes next in Lecture 23 and Lecture 24.

Indeed **any** \$$\rho : X \times X \to X\$$, where we assume that \$$X\$$ is already equipped with order relation \$$\leq_X\$$: \$$(X, \leq_X)\$$, **automatically induces** a natural preorder on \$$X \times X \$$ by requiring
$\rho(x_1, x_2) \leq_X \rho(x'_1, x'_2) \Rightarrow (x_1, x_2) \leq_\rho (x'_1, x'_2)$

where \$$\leq_\rho = \leq_{X \times X}\$$ is an induced order relation on \$$X \times X \$$, making it into preorder: \$$(X \times X, \leq_\rho)\$$. Since this relation is induced, implication also goes backwards:
$(x_1, x_2) \leq_\rho (x'_1, x'_2) \Rightarrow \rho(x_1, x_2) \leq_X \rho(x'_1, x'_2)$
which is exactly a **monotonicity** condition! So things are starting to fall into their places, at last.

And now we can say that among all possible \$$\rho\$$ there indeed exist some functions which additionally support
$C^\times: x_1 \le_X x'_1 \textrm{ and } x_2 \le_X x'_2 \Rightarrow \rho(x_1, x_2) \le_\rho \rho(x'_1, x'_2)$

Okay, now only what I need is to figure out how this condition structures the \$$(X \times X, \leq_\rho) \$$ preorder, and how preorders supporting it differ from others.