Stream: new members

Topic: Working with universes

Fox Thomson (Jul 24 2020 at 16:58):

I'm having trouble with using universes and ordinals. I want to lift an ordinal one universe higher and then compare it to an ordinal of that universe but I get an error as lean isn't able to figure out what universe to use in the lift. If I explicitly say I want it of type max u u+1 then I get an error which I think is from max u u+1 reducing to u+1 too early.

-- without explicit type
def compliment {α : Type} (M : α → ordinal.{u}) : set ordinal.{u+1} := { O : ordinal | ¬ ∃ a : α, (M a).lift = O }

-- with explicit type
def compliment {α : Type} (M : α → ordinal.{u}) : set ordinal.{u+1} := { O : ordinal | ¬ ∃ a : α, ((M a).lift : ordinal.{max u u+1}) = O }


Mario Carneiro (Jul 25 2020 at 00:04):

Unfortunately, you can't use the target type to pin down the universes here, because max is not injective. You have to write (M a).lift.{u (u+1)}

Fox Thomson (Jul 26 2020 at 10:29):

That works, thank you!

Last updated: May 15 2021 at 02:11 UTC