preorder.comap

Stream: general

[Kevin Buzzard]

Do we already have the function which given a map X -> Y and a preorder on Y, produces a preorder on X? I searched for preorder.comap and found nothing. Is that what it's supposed to be called?

[Scott Morrison]

You'd think this just gets synthesised automatically when preorder is defined. :grinning:

[Scott Morrison]

(More seriously --- how close could we get to that happening? Can we construct derive handlers so a new structure could just be labelled with @[derive comap] and that definition is added?)

[Mario Carneiro]

I think it's called preorder.lift