accessing universal set

Stream: new members

[Calle Sönne]

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]

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]

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]

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

[Kevin Buzzard]

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

[Calle Sönne]

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]

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