categories with morphisms in Prop

Stream: mathlib4

[Chris Henson]

Two questions:

1. Could someone explain the design decision to have docs#CategoryTheory.Category universe polymorphic over Type (as opposed to Sort)?
2. Given this decision, what is the best way to work with categories whose morphisms are in Prop? It seems the choices are to do some lifting (like in docs#Preorder.smallCategory) or refactor to use Type.

[Kenny Lau]

I'm not a developer but I would explain it by saying that Prop is a really "weak" universe and we usually think of morphisms as having "data"

[Aaron Liu]

You can always PLift into a type

[Yaël Dillies]

Chris Henson said:

1. what is the best way to work with categories whose morphisms are in Prop?

You should (probably) put a Preorder instance on such a category and use the results in the file Mathlib.CategoryTheory.Category.Preorder

[Joël Riou]

Note: a few people (not me) have tried to allow morphisms in categories to be in Sort v instead of Type v, but it failed because of subtleties about universes in Lean.

[Chris Henson]

Yaël Dillies said:

You should (probably) put a Preorder instance on such a category and use the results in the file Mathlib.CategoryTheory.Category.Preorder

This is interesting. The context here is that my morphisms are typing derivations (for various locally nameless formalizations of lambda calculi I've done). So it feels a bit odd to define a preorder on them, but maybe this is the best way to use an existing API?

[Chris Henson]

Joël Riou said:

Note: a few people (not me) have tried to allow morphisms in categories to be in Sort v instead of Type v, but it failed because of subtleties about universes in Lean.

Would anyone who has attempted this be able to talk a bit more about the universe issues they encountered? Is this because of (non) cumulative universes or something more subtle?

[Kevin Buzzard]

IIRC the last time we tried to make the switch was in the Lean 3 days so it might be the case that the data coming from an answer to why it failed is no longer relevant

[Chris Hughes]

I tried this change years ago here. There is a small amount of information about what broke. It seems like something to do with the fact that categories arising from preorders are no longer "small" by Lean's definition of small_category at the time. I guess maybe that made it harder to take limits over these diagrams because some categories only have "small" limits. But this is something to do with the funny definition of small_category which is that the homs and the objects live in the same universe, which isn't really what determines if we can take limits. I may be completely wrong about what the issues were there, but that is my guess.

[Markus Himmel]

There is more information and some links in this thread: #new members > ✔ Universe Restriction on CategoryTheory.Category