## Stream: new members

### Topic: Sort universes

#### 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,

#### Kenny Lau (May 20 2020 at 15:46):

T1 : T2 means T1 is a term of type T2

#### Mario Carneiro (May 20 2020 at 15:46):

Type u is notation for Sort (u+1)

#### Kenny Lau (May 20 2020 at 15:46):

Sort 0 is Prop and is not data

#### 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

#### 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?

#### Yury G. Kudryashov (May 20 2020 at 16:27):

Type u is Sort (u+1)

#### 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

#### Patrick Massot (May 20 2020 at 16:32):

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

#### 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

#### 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