Zulip Chat Archive

Stream: new members

Topic: Sort universes


view this post on Zulip Danila Kurganov (May 20 2020 at 15:46):

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,

view this post on Zulip Kenny Lau (May 20 2020 at 15:46):

T1 : T2 means T1 is a term of type T2

view this post on Zulip Mario Carneiro (May 20 2020 at 15:46):

Type u is notation for Sort (u+1)

view this post on Zulip Kenny Lau (May 20 2020 at 15:46):

Sort 0 is Prop and is not data

view this post on Zulip Mario Carneiro (May 20 2020 at 15:47):

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

view this post on Zulip Danila Kurganov (May 20 2020 at 16:25):

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?

view this post on Zulip Yury G. Kudryashov (May 20 2020 at 16:27):

Type u is Sort (u+1)

view this post on Zulip Danila Kurganov (May 20 2020 at 16:31):

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

view this post on Zulip Patrick Massot (May 20 2020 at 16:32):

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

view this post on Zulip Danila Kurganov (May 20 2020 at 16:41):

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

view this post on Zulip Patrick Massot (May 20 2020 at 16:49):

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


Last updated: May 10 2021 at 18:22 UTC