Zulip Chat Archive

Stream: new members

Topic: accessing universal set


view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 11:45):

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

view this post on Zulip 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!

view this post on Zulip 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