type hierarchy

Stream: general

[Shi Zhengyu]

Hi all,
I am having a little trouble understanding type hierarchy in Lean. Is it wrong to claim that If definition of (A: Type i) is dependent on definition of (B: Type j), then i > j must hold? I tried it myself with example below but it actually pass the type test. Why?

inductive myType: Type 0 | none | some: ℕ -> myType

Thanks!

[Shi Zhengyu]

I just tried some other examples, it seems suffice to have i >= j.

[Kevin Buzzard]

Indeed your claim is false in the sense that I'm very happy that if X is in universe u then so is option X. Set-theoretically if X is a set then X union {*} is also a set.

[Chris B]

Shi Zhengyu said:

I guess what I'm not understanding is why not just force them to stay in different hierarchies

Is the idea that a constructor of myType in Type n+1 should only be able to quantify over elements of types <= Type n? How would you handle List (Option A) vs. Option (List A)?

[Kevin Buzzard]

The way I usually think about this is "if I were doing this in set theory, would it still be a set?" If so then there's no universe bumping taking place.