Sort universes

Stream: new members

[Danila Kurganov]

Hi,
I'd like to check my understanding of what 'Sort' does when giving it some pre-defined universe. In the output box, is it giving a reply of the universe level predecessor?

Eg:

universe u
#check Sort u
#check Sort (u + 1)

gives Sort u : Type u, and Type u : Type (u + 1) as output.

Does the first line tell us that "Sort u" is the predecessor of "Type u" (when thinking of universe levels), and "Type u" would come before "Type u + 1"? (backwards inductive in nature?)

Also, what does the colon mean in the output? (How should the output be read?)

Thanks,

[Kenny Lau]

T1 : T2 means T1 is a term of type T2

[Mario Carneiro]

Type u is notation for Sort (u+1)

[Kenny Lau]

Sort 0 is Prop and is not data

[Mario Carneiro]

and for each u, Sort u : Sort (u+1), and lean prefers to use Type to write the latter

[Danila Kurganov]

Great, so Sort and Type are sort of opposites(?); if we do an example to confirm what it is:
Say we have these three things: mammals, animals, living things;
sort (living things) should give us mammals (mammals : living things)
type (mammals) should give us living things (mammals: living things)

Would this be a correct way of looking at this?

[Yury G. Kudryashov]

Type u is Sort (u+1)

[Danila Kurganov]

Yury G. Kudryashov said:

Type u is Sort (u+1)

So one is just defined as the other +- 1 level? No need to get a deeper meaning for it seems

[Patrick Massot]

It's simply providing a convenient way to say "any universe but Prop".

[Danila Kurganov]

Ok, thanks - I'll keep this in mind given what I know now.. I don't know Type theory yet, it seems this has something something to do with Russel's Paradox - for now I will accept it on basis and hope it doesn't bug me too much

[Patrick Massot]

The difference between Prop and Type is important. Everything else in this direction can be ignored for a very long time without doing any harm