I dont know what to do with universe constraints

Stream: general

[deepest recursion]

Hello! Ive put together a tiny piece of code for whichlean says it cant do its universe level stuff. Could someone please take a look?

[Andrew Yang]

I will advise against Sort _ and instead declare universe u and write Sort u and at some point you will find out where things went differently from your mental model.

[Andrew Yang]

In particular you might discover that the output universe of Either (you can see it by #print Either) might not be what you imagined.

[deepest recursion]

Ive #printed the Either and it was shown to be Either.{u_1, u_2} (A : Sort u_1) (B : Sort u_2) : Sort (max (max 1 u_1) u_2). I read it as for any instatiation of the Either with arbitrarty types the resulting level should be the greates of two and + 1 because lean wants it for some reason

I cant figure out this one tho

inductive Either (A:Sort _) (B:Sort _) where
 | inl (_:A)
 | inr (_:B)

inductive U : Sort _ -> Sort _ where
  | either (A:Sort _)(B:Sort _) (_:U A) (_: U B) : U (Either A B)
  | pair (A B:Sort _)(_:U A) (_: U B): U (PProd A B)
  | empty : U PEmpty
  | unit : U PUnit
universe l3
def Closed /-{l3}-/ (F:Sort l1 -> Sort l2):Sort ((max l1 (max l2 (max l3 1)))) := ∀ (T:Sort l3), (U T) -> (F T)

Any salvation for this one?

I see the levels as a hindrance tbh. Is there a way to disable em?

[Andrew Yang]

If you don't want to deal with these issues then I suggest you use Type u everywhere for a fixed universe, or even just stick with Type.

[Andrew Yang]

This is what you get if you fill in all the underscores with the right universes:

universe u₁ u₂ u u'

inductive Either (A : Sort u₁) (B : Sort u₂) : Sort (max 1 u₁ u₂) where
 | inl (_:A)
 | inr (_:B)

inductive U : Sort (max 1 u) -> Type (max 1 u) where
  | either (A B : Sort (max 1 u)) (_ : U A) (_ : U B) : U (Either A B)
  | pair (A B : Sort (max 1 u)) (_ : U A) (_ : U B): U (PProd A B)
  | empty : U PEmpty
  | unit : U PUnit

def Closed (F: Sort (max 1 u) -> Sort u') := ∀ T, (U T) -> (F T)

[Andrew Yang]

Or you can just stick in one universe:

inductive Either (A : Type u) (B : Type u) : Type u where
 | inl (_:A)
 | inr (_:B)

inductive U : Type u -> Type (u + 1) where
  | either (A : Type u) (B : Type u) (_ : U A) (_ : U B) : U (Either A B)
  | pair (A B : Type u) (_ : U A) (_ : U B): U (PProd A B)
  | empty : U PEmpty
  | unit : U PUnit

def Closed (F: Type u -> Type u) := ∀ T, (U T) -> (F T)

[deepest recursion]

I ve tried your solution with Sorts and it still trips lean in the same way as my original code. The second piece with Type works, although Ive tweaked one piece a bit.

def Closed (F: Sort _ -> Sort _) := ∀ T, (U T) -> (F T)
example : Closed (fun T => (a b:List T) -> a = b) := by
  admit

This universe stuff is still confusing.

Thanks for writing this out, anyhow.

[Andrew Yang]

I think you should work with Type instead of Sort.

[Kevin Buzzard]

The max 1 u in your original code means "Lean is telling you that the output is a Type and not a Sort" and your examples of PEmpty and PUnit are types so why not just use types? The max 1 u isn't "adding 1" as you say, it's more accurate to say it's "turning the output into a type".

[Kevin Buzzard]

If you look at docs#Sum for example, which is core Lean's way of doing Either, it uses types.