Sort u

Stream: new members

[J. O.]

I was reading through the lean 4 manual and came across Sort u : the universe of types at universe level u. I don't really understand Sort, and the what the universe level is. Also, (x : α) → β : the type of functions taking an element x of α to an element of β, where β is an expression whose type is a Sort. What does it mean to return type Sort. I never had something like this in the languages I've worked with

[J. O.]

im honestly confused with lean's type system

[J. O.]

this whole monstrosity:

Prop abbreviates Sort 0, Type abbreviates Sort 1, and Type u abbreviates Sort (u + 1) when u is a universe variable. We say "α is a type" to express α : Type u for some u, and we say "p is a proposition" to express p : Prop. Using the propositions as types correspondence, given p : Prop, we refer to an expression t : p as a proof of p. In contrast, given α : Type u for some u and t : α, we sometimes refer to t as data.

[J. O.]

even these are a bit confusing image.png

[J. O.]

Like Sort u is also Type u

[J. O.]

is understanding lean's type system at the beginning very important?

[J. O.]

but mainly, what is

universe u

[Julian Berman]

It's not terribly important I think, but others may recommend knowing just a bit. Essentially some of the complexity here comes from some mathematics -- perhaps to start, have you ever heard of Russell's paradox?

[J. O.]

Julian Berman said:

It's not terribly important I think, but others may recommend knowing just a bit. Essentially some of the complexity here comes from some mathematics -- perhaps to start, have you ever heard of Russell's paradox?

I never heard of Russels Paradox. Im gonna give it a read

[J. O.]

How does the paradox relate to the type system?

[Julian Berman]

universes essentially are a way to "fix" this paradox (or truthfully a related one, called Girard's paradox which mathlib even has a proof of!)

[Julian Berman]

I'd say in short you should understand a few things, and then can expand -- first, Prop is the type of propositions (statements which have a proof or do not). Things like 2 = 2, 2 = 7 or more complicated mathematical statements

[Julian Berman]

Type is more similar to what you're likely familiar with from other programming languages. E.g. Nat is the type of natural numbers.

[Julian Berman]

And then why or when you need types that live in "universes" higher than 1 is the aforementioned paradox, which is relevant when doing specific kinds of math.

[Julian Berman]

But I think you can likely get quite far just knowing the bit about Prop and Type -- (in fact if you haven't already, doing the natural number game is a nice way to get started, albeit with Lean 3, and it I believe mentions nothing beyond these?).

[Chris B]

There's a nice graphic in this post: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/question.20about.20bool.20vs.20Prop/near/264049001

[Julian Berman]

Oh, cool, that's indeed nice and I hadn't seen it myself!

[Chris B]

J. O. said:

Like Sort u is also Type u

The notation a : A means a is an element of type A, not a is also A.

[J. O.]

thanks

[Kevin Buzzard]

@J. O. Have you looked at #tpil ? It is written for people with a computer science background and answers a lot of basic questions. It has discussions about type universes.