sort-valued hom in category

Stream: mathlib4

[Kenny Lau]

why does docs#CategoryTheory.Category not take Sort-valued hom?

[Aaron Liu]

I think it used to

[Kevin Buzzard]

We tried in Lean 3 and it didn't go well; AFAIK nobody tried in Lean 4.

[Kenny Lau]

do you remember what the problem was?

[Yaël Dillies]

Universe levels become more complicated, and in particular the universe unification algorithm didn't know how to solve for the universe levels in many common cases

[Joël Riou]

See #new members > ✔ Universe Restriction on CategoryTheory.Category @ 💬

[Aaron Liu]

I found mathlib3#1412

[Kenny Lau]

have we fixed the Category.{v} C bug yet? i.e. do we still have to write .{v} for the code to be performant?

[Aaron Liu]

I don't see this as a bug

[Chris Henson]

I've been referred to that issue and thread previously and still don't quite understand the problem. Would someone be willing to explain it again here?

[Artie Khovanov]

The bottom universe level - the universe of propositions - works differently to the others, which can cause problems in certain situations where Lean doesn't know whether a type is in the bottom universe. The obvious fix - which is to force these problematic types to not be in the bottom universe - causes a mess.
(did I understand right?)

[Aaron Liu]

Artie Khovanov said:

The bottom universe level - the universe of propositions - works differently to the others, which can cause problems in certain situations where Lean doesn't know whether a type is in the bottom universe. The obvious fix - which is to force these problematic types to not be in the bottom universe - causes a mess.
(did I understand right?)

Not sure what kind of mess you mean but this is the solution currently in mathlib and sometimes it's annoying to work with

[François G. Dorais]

Probably not helpful since it is counterintuitive: the basic category data should be the homomorphisms not the objects.

[François G. Dorais]

(That philosophy usually fixes all universe issues for me.)

[Kenny Lau]

@François G. Dorais we do place the homomorphisms first, which is why we have [Category.{v} C]

[Kenny Lau]

maybe using [Category.{v} C] will fix the problem we experienced in the past with sort-based hom?

[François G. Dorais]

I'm thinking about class Category {α : Sort _} (β : α → α → Sort _) where ... No need for .{v} since the homs are the principal argument.

[Kenny Lau]

it is expensive to unify functions

[François G. Dorais]

Works fine for me. But it's radically different.

[François G. Dorais]

I do use wrappers to ease class synthesis.

[Kenny Lau]

yes, we should use one-param structures

[Joël Riou]

It seems very unlikely that this could make it into mathlib.