Zulip Chat Archive

Stream: new members

Topic: lifting "down"


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

view this post on Zulip Kenny Lau (Jan 18 2020 at 17:04):

you can't; that's the whole point

view this post on Zulip Kenny Lau (Jan 18 2020 at 17:04):

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

view this post on Zulip Calle Sönne (Jan 18 2020 at 17:09):

MWE?

view this post on Zulip Reid Barton (Jan 18 2020 at 17:09):

An element in a set of sets is a set

view this post on Zulip Kenny Lau (Jan 18 2020 at 17:10):

MWE = minimal working example

view this post on Zulip Reid Barton (Jan 18 2020 at 17:10):

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

view this post on Zulip Calle Sönne (Jan 18 2020 at 17:12):

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

view this post on Zulip Calle Sönne (Jan 18 2020 at 17:12):

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

view this post on Zulip Calle Sönne (Jan 18 2020 at 17:13):

the MWE gives an error

view this post on Zulip Kenny Lau (Jan 18 2020 at 17:14):

U.1

view this post on Zulip Calle Sönne (Jan 18 2020 at 17:14):

and my question is how do I resolve this

view this post on Zulip Kenny Lau (Jan 18 2020 at 17:14):

it's not ulift

view this post on Zulip Calle Sönne (Jan 18 2020 at 17:16):

wait what does .1 do in this case?

view this post on Zulip Calle Sönne (Jan 18 2020 at 17:16):

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

view this post on Zulip Calle Sönne (Jan 18 2020 at 17:16):

but set is defined as a function

view this post on Zulip Kenny Lau (Jan 18 2020 at 17:18):

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

view this post on Zulip Kenny Lau (Jan 18 2020 at 17:18):

opens is not a type

view this post on Zulip Calle Sönne (Jan 18 2020 at 17:19):

oh


Last updated: May 15 2021 at 02:11 UTC