fillter types?

Stream: general

[Kenny Lau]

So we don't need to write the universes every time and Lean automatically generates them for us (the names would be u_1, etc)... what if Lean did the same to types?

[Chris Hughes]

Generally Lean just gives every Type a different universe variable. You don't want it giving every variable a different Type. It seems like a much harder problem.