## Stream: general

### Topic: preorder.comap

#### Kevin Buzzard (Mar 19 2019 at 18:07):

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 (Mar 20 2019 at 00:09):

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

#### Scott Morrison (Mar 20 2019 at 00:11):

(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 (Mar 20 2019 at 00:31):

I think it's called preorder.lift

Last updated: May 11 2021 at 14:11 UTC