Great answers to all the puzzles, Scott!

> **Puzzle 216:** Rewritten as a monotone function, we have \\(\cap_X : 1^\mathrm{op} \times X^\mathrm{op} \times X \to \mathbf{Bool}\\). By the above theorems (puzzle answers), this function is isomorphic to a function \\(X^\mathrm{op} \times X \to \mathbf{Bool}\\). But this is just the hom-functor! So we have

\[ \cap_X (x,x') = \hom(x,x')\]

Right!

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

If you're looking for a monotone function \\(\cap_X: X^\mathrm{op} \times X \to \mathbf{Bool}\\), the obvious thing to try is the hom-functor \\(\text{hom}: X^\mathrm{op} \times X \to \mathbf{Bool}\\).


And indeed, this turns out to work very well, so that's what we'll use!

> In other words,

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