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}$