# Zulip Chat Archive

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