Zulip Chat Archive

Stream: maths

Topic: from preorder to category

Kenny Lau (Aug 04 2020 at 15:21):

How problematic will it be if I were to have an instance of category P from preorder P?

Reid Barton (Aug 04 2020 at 15:22):

I think we used to have it

Reid Barton (Aug 04 2020 at 15:22):

or at least it was discussed before

Kenny Lau (Aug 04 2020 at 15:22):

docs#category_theory.preorder.small_category

Kenny Lau (Aug 04 2020 at 15:23):

bad link, but it's here: https://github.com/leanprover-community/mathlib/blob/8e0d111ff84b84b237392ec824d93ee7d8f917c8/src/category_theory/category/default.lean#L206

Kenny Lau (Aug 04 2020 at 15:23):

so we do have it

Reid Barton (Aug 04 2020 at 15:24):

We still do, but we used to, too

Last updated: Dec 20 2023 at 11:08 UTC