set on a subtype as set on the type?

Stream: Is there code for X?

[Michael Stoll]

If I have a type a and s : set a, then I can consider t : ↥s. So t is a subset if s considered as a subtype of a, which I should be able to conside as a subset of a, i.e., ↑t : set a. But this does not work, and I also couldn't find a definition that would convert t into a set a. Am I overlooking something?

[Michael Stoll]

def coe_set_of_subtype {α} (a : set α) (b : set ↥a) : set α :=
λ x, Π (h : x ∈ a), ({val := x, property := h} : ↥a) ∈ b

This is a case that showed me why pi types are useful :light_bulb: -- something along the lines of x ∈ a ∧ ... does not work.

[Yakov Pechersky]

(coe '' b : set \alpha), or (coe '' t : set a) for your initial sentence

[Michael Stoll]

OK (and sorry for changing notation). Should there be a has_coe instance for this?

[Yakov Pechersky]

Perhaps a has_lift or has_lift_t, ala docs#lift_list

[Reid Barton]

Your definition doesn't do what you want--exercise: what subset of α did you actually define?
There is a very similar definition however that does work.

[Yakov Pechersky]

Is the Pi definition b \union a\compl? With the "similar definition" using Sigma (or Exists) instead.

[Michael Stoll]

You are right (and I just proved it :smile:)

[Yaël Dillies]

You can write this as a \himp b btw

[Michael Stoll]

Typing "\himp" in VSCode gives me "⟶imp"

[Yaël Dillies]

Oh shoot. See docs#himp_himp

[Michael Stoll]

It shouldn't be necessary to learn about Heyting algebras to do what I want...

[Yaël Dillies]

I'm just saying that b ∪ aᶜ can be more concisely written a ⇨ b.

[Michael Stoll]

But here a and b have different types, so this gives a type error.

[Michael Stoll]

(BTW, there doesn't seem to be a VSCode shortcut for typing ⇨. At least, hovering over it does not show any hint (other than the docstring for has_himp.himp).)

[Yaël Dillies]

I was referring to Yakov's message.

[Yaël Dillies]

I meant to add a shortcut to the extension, but I haven't yet gotten around to doing it.