preorder_hom vs rel_hom

Stream: general

[Yaël Dillies]

I've just read #5525 and it struck me that docs#order_embedding and docs#order_iso are already abbreviations of rel_embedding (≤) (≤) and rel_iso (≤) (≤). I am a few propositions on what we would do and I would just like some opinion before I move forward:

• rename preorder_hom to order_hom
• make preorder_homan abbreviation of rel_hom (≤) (≤)
• change the notation of preorder_hom from →ₘ to →o (or change the three order_something to →ₒ, ↪ₒ and ≃ₒ because it looks nicer)
• Instead of having order.preorder_hom for preorder_hom and order.order_iso for the five other ones, have data.rel_homfor the rel_something and order.order_hom for the order_something.