## Stream: new members

### Topic: lifting "down"

#### Calle Sönne (Jan 18 2020 at 17:00):

How do I, as opposed to ulift, lift "down" a type? In my case I have an element in a set of sets and I want to treat it as a set.

#### Kenny Lau (Jan 18 2020 at 17:04):

you can't; that's the whole point

#### Kenny Lau (Jan 18 2020 at 17:04):

but an element in a set of sets can definitely be treated as a set (MWE?)

MWE?

#### Reid Barton (Jan 18 2020 at 17:09):

An element in a set of sets is a set

#### Kenny Lau (Jan 18 2020 at 17:10):

MWE = minimal working example

#### Reid Barton (Jan 18 2020 at 17:10):

I think you should explain your question in Lean and not English

#### Calle Sönne (Jan 18 2020 at 17:12):

lemma MWE (α : Type*) (opens : set (set α)) (U : opens) (T : set α) : U = T:=


#### Calle Sönne (Jan 18 2020 at 17:12):

Maybe it is my instinct to want to lift down as opposed to up

#### Calle Sönne (Jan 18 2020 at 17:13):

the MWE gives an error

#### Kenny Lau (Jan 18 2020 at 17:14):

U.1

#### Calle Sönne (Jan 18 2020 at 17:14):

and my question is how do I resolve this

#### Kenny Lau (Jan 18 2020 at 17:14):

it's not ulift

#### Calle Sönne (Jan 18 2020 at 17:16):

wait what does .1 do in this case?

#### Calle Sönne (Jan 18 2020 at 17:16):

Usually when I use it it is to access the carrier of some structure

#### Calle Sönne (Jan 18 2020 at 17:16):

but set is defined as a function

#### Kenny Lau (Jan 18 2020 at 17:18):

the way you coerce opens to a type is to use subtype

#### Kenny Lau (Jan 18 2020 at 17:18):

opens is not a type

#### Calle Sönne (Jan 18 2020 at 17:19):

oh

Last updated: May 15 2021 at 02:11 UTC