Keith wrote

> Actually, now that I think about, isn't

> \[ \cap_X(x,x') =\begin{cases}\mathrm{true} & \mathrm{if} \ x \le x' \\\ \mathrm{false} & \mathrm{otherwise} \end{cases}\]

> a bit redundant? \\([x \leq x']\\) is already *the* relation that gives \\(\mathrm{true}\\) when \\(x\\) is less then or equal to \\(x'\\), and \\(\mathrm{false}\\) otherwise.

Yeah, it seems redundant to me. Although, one could argue that really cap is this function \\(1^\mathrm{op} \times \left(X^\mathrm{op} \times X\right)\\):
\[ \cap_X(1, (x,x')) =\begin{cases}\mathrm{true} & \mathrm{if} \ x \le x' \\\ \mathrm{false} & \mathrm{otherwise} \end{cases}\]
where \\(1\\) is the object of the singleton preorder. But cap is isomorphic to the hom-functor which is just a preorder relation on \\(X\\): \\(\hom(x,x') = (x\le x')\\).

John wrote

> It's worth letting newbies know that last two sentences are not the conclusion of some logical argument, but rather a natural guess. The thought process is

I should probably highlight guesses like that more clearly. Thanks for pointing it out.