Cosmology of Lean

Stream: new members

[Dan Abramov]

I've been doing some doodling to understand Lean's type hierarchy.

Not saying this one would be particularly helpful to anyone but I wonder if it captures the right intuitions?

Untitled-2025-02-02-1522 copy.png.png

Note this only deals with concrete universes (not stuff polymorphic over them). It also doesn't do anything with types being dependent.

But broadly, does it appear correct? Is anything misleading or flat out wrong?

Thanks.

[Aaron Liu]

nothing I see is wrong

[Aaron Liu]

...I think

[Niels Voss]

This looks completely right to me. Interestingly, it does actually involve a dependent type: ∀ n, n < 3 is a dependent function type (which lives in Prop due to Prop's impredicativity)

[Eric Wieser]

Set Type 1 is illegal syntax, you mean Set (Type 1)

[Aaron Liu]

Set Type 1 is legal syntax, but it parses as (Set Type) 1 and you will get

Function expected at
  Set Type
but this term has type
  Type 1

Note: Expected a function because this term is being applied to the argument
  1

[Kevin Buzzard]

For me the correct intuition is

Universes | Type                            | Prop
Types     | things mathematicians call sets | theorem statements
Terms     | elements of sets                | proofs

and the facts that Prop has type Type and that Type 37 exists are just implementation issues.