ordinals across universes

Stream: new members

[Pedro Sánchez Terraf]

I understand there is a type of ordinals (resp. cardinals) in any given type universe (sort?) u, and that there is a lifting operation from lower to higher sorts. (Please confirm!)

I have seen that apparently there is no associated coercion, in that I can write

import set_theory.cardinal.ordinal

open_locale cardinal
open cardinal

#check (ℵ₀ : cardinal.{2}) = lift.{2 1} (ℵ₀ : cardinal.{1})

but

#check (ℵ₀ : cardinal.{2}) = (ℵ₀ : cardinal.{1})

will fail. Why is there no such coercion defined?

[Mario Carneiro]

because you almost always need to use the universe arguments when using lift and you can't do that if the normal form was \u

[Pedro Sánchez Terraf]

Btw, I really don't know if the above “equalities” are morally right. rfl is not a proof, and the rhs of the successful type-checking prints as ℵ₀.lift

[Mario Carneiro]

note that the universe arguments of lift are not uniquely determined by the input and output types, since the output type is cardinal.{max u v} and max is not injective

[Pedro Sánchez Terraf]

Mario Carneiro said:

you can't do that if the normal form was \u

I'm afraid I do not get the normal form part. I accept a RTFM with a link as response! :wink:

[Mario Carneiro]

https://leanprover-community.github.io/extras/simp.html#simp-normal-form

[Pedro Sánchez Terraf]

Thank you @Mario Carneiro. I'll try to process this and then I'll continue asking