Universe heterogeneous cardinal comparison

Stream: mathlib4

[Violeta Hernández]

This is an old idea of mine that I got reminded of after @staroperator's PR #29351 (they don't seem to be in the Zulip). The thing is that there is a lot of redundancy in the Cardinal/Ordinal APIs caused by the sole reason that cardinals/ordinals in different universes can't be directly compared; you need to use docs#Cardinal.lift or docs#Ordinal.lift to move them to a common universe, then compare them there.

[Aaron Liu]

this reminds me of #mathlib4 > Universe-heterogeneous ordinal and cardinal relations

[Violeta Hernández]

Dammit, I looked for that thread and couldn't find it!

[Violeta Hernández]

Disregard this thread then