Zulip Chat Archive

Stream: maths

Topic: from preorder to category


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

view this post on Zulip Reid Barton (Aug 04 2020 at 15:22):

I think we used to have it

view this post on Zulip Reid Barton (Aug 04 2020 at 15:22):

or at least it was discussed before

view this post on Zulip Kenny Lau (Aug 04 2020 at 15:22):

docs#category_theory.preorder.small_category

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

view this post on Zulip Kenny Lau (Aug 04 2020 at 15:23):

so we do have it

view this post on Zulip Reid Barton (Aug 04 2020 at 15:24):

We still do, but we used to, too


Last updated: May 09 2021 at 11:09 UTC