Working with universes

Stream: new members

[Fox Thomson]

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]

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]

That works, thank you!