## Stream: Is there code for X?

### Topic: category of POSet

#### Simon Hudon (Aug 17 2020 at 15:43):

Do we have a category of partial orders (or preorders) with monotone functions as morphisms?

#### Simon Hudon (Aug 17 2020 at 15:48):

Nice thanks! Is that a PR about to be merged?

#### Reid Barton (Aug 17 2020 at 15:49):

@Johan Commelin :this:

#### Reid Barton (Aug 17 2020 at 15:50):

It's not already a PR, if that's what you mean.

#### Simon Hudon (Aug 17 2020 at 15:52):

Too bad, I could use that in my PR. I'm bundling monotone functions and I find myself reinventing binary products again

#### Johan Commelin (Aug 17 2020 at 16:43):

@Simon Hudon I can PR those three files on categories of orders

#### Simon Hudon (Aug 17 2020 at 16:44):

That'd be great! Thank you! Do you intend to define the limits of those categories?

#3841

#### Johan Commelin (Aug 17 2020 at 16:49):

@Simon Hudon No, I didn't have any plans on defining limits

#### Simon Hudon (Aug 17 2020 at 16:51):

Ok, I'll take care of it. Thanks for the PR!

#### Aaron Anderson (Aug 17 2020 at 17:27):

FWIW, this this notion of bundled monotone map is pretty similar to the notions of rel_embedding and the order_embedding that I'm redefining. I see no reason not to PR it now, but I might try to generalize it soon to rel_hom for arbitrary relations, with order_hom as a special case.

Last updated: May 07 2021 at 21:10 UTC