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.