Zulip Chat Archive

Stream: general

Topic: preorder.comap


view this post on Zulip 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?

view this post on Zulip Scott Morrison (Mar 20 2019 at 00:09):

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

view this post on Zulip 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?)

view this post on Zulip Mario Carneiro (Mar 20 2019 at 00:31):

I think it's called preorder.lift


Last updated: May 11 2021 at 14:11 UTC