Zulip Chat Archive

Stream: new members

Topic: noob questions about ∃


view this post on Zulip Jason Orendorff (Jun 10 2020 at 14:57):

I have to admit, I'm not totally clear on the subtleties of supporting both constructive and classical logic, but bottom line, classical.some is noncomputable, so I think ∃ in Lean must "mean" the classical, non-constructive ∃.

Is there a stronger form of ∃ that carries a value, so that it supports a computable analogue of classical.some?

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 14:58):

There's the inhabited typeclass

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 14:59):

The point is that ∃ x, P has type Prop and you can't constructively get back to Type land from there.

view this post on Zulip Rob Lewis (Jun 10 2020 at 15:00):

Is there a stronger form of ∃ that carries a value, so that it supports a computable analogue of classical.some?

Σ, but it's not Prop-valued.

view this post on Zulip Jason Orendorff (Jun 10 2020 at 15:00):

right, I am definitely not looking for Sigma. thanks.

view this post on Zulip Jason Orendorff (Jun 10 2020 at 15:01):

However, not understanding the split between Prop and Type may be why I'm confused

view this post on Zulip Rob Lewis (Jun 10 2020 at 15:09):

You can't have a Prop-valued exists with a projection to Type that preserves values. Prop is proof irrelevant, so any two proofs of ∃ x, P are equal, even if they're proved with different witnesses. A function that recovers the witnesses would have different values on equal inputs.

view this post on Zulip Mario Carneiro (Jun 10 2020 at 15:14):

There is also trunc {x // P}, which is in Type but is nevertheless a subsingleton like ∃ x, P

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 15:14):

So the worst of both worlds?

view this post on Zulip Mario Carneiro (Jun 10 2020 at 15:15):

I suppose so, depending on your POV

view this post on Zulip Reid Barton (Jun 10 2020 at 15:33):

trunc {x // P} is the one that corresponds to the existential quantifier as used in the HoTT book, for example.

view this post on Zulip David Wärn (Jun 10 2020 at 18:12):

The upshot of trunc is that you get computable unique choice. So if you e.g. have f : X -> Y with inj : injective f and surj : \Pi y, trunc { x // f x = y } then you get a computable inverse g : Y -> X, from trunc.rec.


Last updated: May 15 2021 at 02:11 UTC