# Zulip Chat Archive

## 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):

`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