Hey John,

> I'm sad that nobody has done Puzzle 180:
> > **Puzzle 180.** Prove that there is a category \\(\textbf{Feas}\\) whose objects are preorders and whose morphisms are feasibility relations, composed as above.


Don't be sad! I tried to do it in [#7](https://forum.azimuthproject.org/discussion/comment/19990/#Comment_19990)!

As I mentioned, associativity of composition reflects a tautology in first order propositional logic:

\[ \exists b. \phi(a,b) \wedge (\exists c. \psi(b,c) \wedge \upsilon(c,d)) \Longleftrightarrow \exists c. (\exists b. \phi(a,b) \wedge \psi(b,c)) \wedge \upsilon(c,d) \]

And the identity feasibility relation is:

\[ \mathbf{1}_X(x,y) := x \leq_X y \]