noob questions about ∃

Stream: new members

[Jason Orendorff]

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?

[Kevin Buzzard]

There's the inhabited typeclass

[Kevin Buzzard]

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

[Rob Lewis]

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.

[Jason Orendorff]

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

[Jason Orendorff]

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

[Rob Lewis]

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.

[Mario Carneiro]

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

[Kevin Buzzard]

So the worst of both worlds?

[Mario Carneiro]

I suppose so, depending on your POV

[Reid Barton]

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

[David Wärn]

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.