## Stream: new members

### Topic: ordinals across universes

#### Pedro Sánchez Terraf (Nov 07 2022 at 21:37):

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 (Nov 07 2022 at 21:38):

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 (Nov 07 2022 at 21:39):

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 (Nov 07 2022 at 21:40):

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 (Nov 07 2022 at 21:41):

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 (Nov 07 2022 at 21:41):

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

#### Pedro Sánchez Terraf (Nov 07 2022 at 21:51):

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

Last updated: Dec 20 2023 at 11:08 UTC