## Stream: new members

### Topic: accessing universal set

#### Calle Sönne (Dec 05 2020 at 11:36):

Given a subset in lean, Is there a good way to access the set its contained in without constructing it?
In my case I have a subset of sections:

def sections (F : J ⥤ Type w) : set (Π j, F.obj j) :=
{ u | ∀ {j j'} (f : j ⟶ j'), F.map f (u j) = u j'}


And now I want to access (set (Π j, F.obj j)) as a set. (so not as type Type)

#### Kevin Buzzard (Dec 05 2020 at 11:43):

I don't quite understand the question. set X is the type of all subsets of X. What do you actually have?

#### Calle Sönne (Dec 05 2020 at 11:43):

Kevin Buzzard said:

I don't quite understand the question. set X is the type of all subsets of X. What do you actually have?

I have a term of this type, so a subset, and now I want to get the term of this type which is the whole set

#### Kevin Buzzard (Dec 05 2020 at 11:44):

What is "the whole set"? Do you mean the type, considered as a subset of itself? This is univ : set X.

#### Kevin Buzzard (Dec 05 2020 at 11:45):

There is no set, there is just a type, and the type of its subsets.

#### Calle Sönne (Dec 05 2020 at 11:46):

Kevin Buzzard said:

What is "the whole set"? Do you mean the type, considered as a subset of itself? This is univ : set X.

yes this is what I mean!

#### Kevin Buzzard (Dec 05 2020 at 11:47):

I emphasized that when I taught the intro module this year. When a mathematician says set I argued that they either meant type or subset

Last updated: May 18 2021 at 16:25 UTC