# Zulip Chat Archive

## Stream: new members

### Topic: noob questions about ∃

#### 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`

?

#### Kevin Buzzard (Jun 10 2020 at 14:58):

There's the `inhabited`

typeclass

#### 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.

#### 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.

#### Jason Orendorff (Jun 10 2020 at 15:00):

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

#### Jason Orendorff (Jun 10 2020 at 15:01):

However, not understanding the split between `Prop`

and `Type`

may be why I'm confused

#### 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.

#### 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`

#### Kevin Buzzard (Jun 10 2020 at 15:14):

So the worst of both worlds?

#### Mario Carneiro (Jun 10 2020 at 15:15):

I suppose so, depending on your POV

#### 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.

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