Unify (or at least connect) `order_hom` and `rel_hom`

[awainverse]

order_hom is essentially the same as a rel_hom between two instances of ≤. One of two things should happen:

• order_hom should be refactored to be based on rel_hom, with an interface to show that this is the same thing as a monotone function
• An API should be built out for translating between order_homs and rel_homs, enough that it is easy to link order_homs and order_embedding/order_isos.

[YaelDillies]

Now that I worked a lot on order homs (building the order categories), I feel like the first option is the wrong one. Building on top of rel_hom means that we don't have custom field names and we can't extend order_hom. Instead, we must extend @rel_hom α β (≤) (≤).

I will work on redefining order_embedding and order_iso away from rel_embedding and rel_iso.

I'm not sure we need the second option much either, because rel_homs are used so little in mathlib. But maybe one day we will want to translate between orders and graphs?