Zulip Chat Archive

Stream: general

Topic: type hierarchy


Shi Zhengyu (Jan 14 2022 at 18:12):

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 (Jan 14 2022 at 18:13):

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

Kevin Buzzard (Jan 14 2022 at 19:08):

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 (Jan 14 2022 at 19:25):

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 (Jan 14 2022 at 19:50):

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.


Last updated: Dec 20 2023 at 11:08 UTC