Stream: Is there code for X?

Topic: Simple Subtype

Marcus Rossel (Dec 29 2020 at 12:59):

Let i : { x : ℕ // ∃ (h : p x), q x } for some propositions p and q over ℕ.
Is there a way to extract an instance i' : { x : ℕ // p x } from this (allowing classical)?
Or else, is there a nice way of getting to i' starting with just ∃ (h : p x), q x?

Eric Wieser (Dec 29 2020 at 13:11):

Your second question is missing the binder that introduces x

Eric Wieser (Dec 29 2020 at 13:13):

But I think the answer to the first is simply let \<i', hi'\> := i in \<i', let \<hp, hq\> := hi' in hp\>

Eric Wieser (Dec 29 2020 at 13:15):

You have to destructure the two parts separately, rather than using let \<i', hp, hq\> := i which will give an error about elimination not being into prop

Eric Wieser (Dec 29 2020 at 13:16):

(\< is the vs-code input shortcut)

Yury G. Kudryashov (Jan 03 2021 at 21:41):

I think, ⟨i, i.2.snd⟩ should work.

Last updated: May 16 2021 at 05:21 UTC