Solution (source code)

= Solution

A <poset> $P$ becomes a <category> with the elements of $P$ as objects and exactly one <morphism> $x\to y$ when $x\leq y$, with no <morphism> otherwise. Reflexivity supplies the <identity morphisms> and transitivity supplies <composition in a category>; uniqueness of <morphisms> proves associativity. A <functor> $f:P\to Q$ is exactly a <monotone function>: it must send $x\leq y$ to $f(x)\leq f(y)$, and this condition suffices because all the required <morphisms> are unique. Antisymmetry says that isomorphic objects of this <category> are equal.