Cardinal increases the universe level

Stream: mathlib4

[Geoffrey Irving]

Is there a reason Cardinal needs to increase the universe level, or is it just that universe levels haven’t been optimized very much? Currently it’s the quotient of the whole universe, which certainly increases the universe, but the ordinal representation wouldn’t.

[Anatole Dedecker]

I don’t think you can avoid bumping the universe level here. Neither cardinals nor ordinals form a set in set theory after all.

[Geoffrey Irving]

Ah, I see: the Cardinal type itself does have to be one level up. I was misreading as the elements are one level up, but on reflection I don’t think that makes sense.

[Anatole Dedecker]

Formally it doesn’t make sense since elements of Cardinal are not types anymore, but they indeed come from type at the universe level you choose.

[Mario Carneiro]

there are a few lemmas that allow you to work with ordinals and know that they are all indexed by a "small" type (but the type depends on the ordinal, which is why the collection of all of them is not "small")