mathlib

mathlib copied to clipboard

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.