You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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?
order_hom
is essentially the same as arel_hom
between two instances of≤
.One of two things should happen:
order_hom
should be refactored to be based onrel_hom
, with an interface to show that this is the same thing as a monotone functionorder_hom
s andrel_hom
s, enough that it is easy to linkorder_hom
s andorder_embedding
/order_iso
s.The text was updated successfully, but these errors were encountered: