Zulip Chat Archive

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