## Stream: new members

### Topic: coercion from set of subtype to set

#### Jason KY. (May 26 2020 at 12:35):

I am trying to create a coercion from a set of subtype A to set and I somehow got it to work but I don't understand why it does work :/
Here is my #mwe

variables {X : Type*}

instance {A : set X} : has_coe (set (subtype A)) (set X) :=
⟨λ U, {x | ∀ x : subtype A, x ∈ U}⟩


If I hover over x in vs code, it says x : X but I would expect x to have type subtype A.

On the other hand I would expect the following code to work since I would think x.1 will have type X but it doesn't seem to be the case.

variables {X : Type*}

instance {A : set X} : has_coe (set (subtype A)) (set X) :=
⟨λ U, {x.1 | ∀ x : subtype A, x ∈ U}⟩


#### Reid Barton (May 26 2020 at 12:37):

In each example, you have two variables called x

#### Reid Barton (May 26 2020 at 12:38):

{x |  already binds x, which I think you were trying to achieve again with the forall. For example {x | x >= 0} makes sense.

#### Jason KY. (May 26 2020 at 12:39):

Something like this? ⟨λ U, {x.1 | x : subtype A, x ∈ U}⟩

#### Reid Barton (May 26 2020 at 12:41):

You can only put a variable before the |, not an expression

#### Jason KY. (May 26 2020 at 12:45):

I don't think I understand how to extract the value of x : subtype A, i.e. get something of type X from x.

instance {A : set X} : has_coe (set (subtype A)) (set X) :=
⟨λ U, {y | ∃ x ∈ U, x.1 = y}⟩


I thought the above should work but its complaining invalid field notation

#### Reid Barton (May 26 2020 at 12:46):

I think that's because Lean is dense about inference involving ∈? Otherwise it looks correct to me

#### Reid Barton (May 26 2020 at 12:46):

The error message is probably telling you that Lean doesn't know x is a subtype A

#### Jason KY. (May 26 2020 at 12:48):

Vs code says it's of type subtype A  when I hover over it so it's very strange lean doesn't know.
I got it to work by adding it though :)

variables {X : Type*}

instance {A : set X} : has_coe (set (subtype A)) (set X) :=
⟨λ U, {y | ∃ (x : subtype A) (H : x ∈ U), x.val = y}⟩


#### Kenny Lau (May 26 2020 at 12:49):

1. subtype A isn't idiomatic. just use coercion
2.
import data.set.basic

variables {X : Type*}

instance {A : set X} : has_coe (set A) (set X) :=
⟨λ S, subtype.val '' S⟩


#### Jason KY. (May 26 2020 at 12:53):

Wow, I did not expect lean would convert set X to Type* (which is what I needed) so easily. Nice!

Last updated: May 14 2021 at 23:14 UTC