# Zulip Chat Archive

## Stream: new members

### Topic: Existential quantifier and first projection

#### Martin C. Martin (Aug 10 2022 at 18:07):

`Exists`

isn't built in, but defined in core. The definition is equivalent to:

```
inductive Exists {α : Sort u} (q : α → Prop) : Prop
| intro : ∀ (a : α), q a → Exists
```

This is the same as the definition of `sigma`

(or `psigma`

), except for the extra `: Prop`

at the end.

Because `Exists`

lives in `Prop`

... this causes it to have some weird definition, where it's not a dependent product type like the sigmas, and you can't extract the witness (first argument to constructor) or second argument to the constructor, whose type might include the value of the witness.

How does that work under the covers? Are there special rules for inductive types that live in `Prop`

to enforce the "there's only zero or one object of this type"? Something about an eliminator? Do inductive types in `Prop`

essentially not have any internal structure?

Also, I thought the type hierarchy had to be strictly increasing, in the sense that any type that depends on `Sort u`

must live in a `Sort`

bigger than `u`

, to avoid Russel's paradox? Do the restrictions on inductive types living in `Prop`

avoid this?

#### Jireh Loreaux (Aug 10 2022 at 19:13):

I'm not the person to answer this question for you, but there are two pieces of information that might be useful:

- Lean has
*subsingleton elimination*which is how certain specific things (like equality) can eliminate from`Prop`

into higher universes. - Universe levels for Π-types use
`imax`

not`max`

, which basically means a Π-type over a`Prop`

is still a`Prop`

, whereas a Π-type over something in universe`Type u`

ends up in`Type (u + 1)`

. - This I think doesn't give rise to Girard's paradox (type theory equivalent of Russell's paradox) because in general (except for subsingleton types) you can't eliminate from
`Prop`

into higher universes.

Note: like I said, I'm not the right person to answer this question, so it's possible I've got something wrong in what I said above.

#### Junyan Xu (Aug 10 2022 at 22:52):

Nice explanations! Some addenda:

The two paragraphs above prior to Section 7.9, TPIL talks about subsingleton elimination (called "singleton elimination" there):

There is an exception to this last rule: we are allowed to eliminate from an inductively defined Prop to an arbitrary Sort when there is only one constructor and each constructor argument is either in Prop or an index. The intuition is that in this case the elimination does not make use of any information that is not already given by the mere fact that the type of argument is inhabited. This special case is known as singleton elimination.

Another prominent example of Prop that allows large elimination is docs#acc, which allows well-founded recursive definitions. `Exists`

on the other hand doesn't admit large elimination and that's why you can't define the first projection. docs#classical.some is sort of a right inverse to Exists.mk, but it's not an eliminator and doesn't satisfy the computation rule.

The universe level of an inductive type is explained in Section 7.8 just above this, and for Pi types also in Section 4.1 (search for imax). This behavior of Pi type for Props is what makes Prop impredicative.

See also Some notes that covers the same topics and also mentions Girard's paradox.

#### Mario Carneiro (Aug 11 2022 at 05:30):

Martin C. Martin said:

Also, I thought the type hierarchy had to be strictly increasing, in the sense that any type that depends on

`Sort u`

must live in a`Sort`

bigger than`u`

, to avoid Russel's paradox? Do the restrictions on inductive types living in`Prop`

avoid this?

This is called predicativity, and `Prop`

is an *impredicative* universe. This is a very strong axiomatic assumption (it pumps the consistency strength from primitive recursive arithmetic all the way up to ZFC + some inaccessible cardinals), but conversely it is necessary for doing "real math" in lean. It is not inconsistent, at least as long as `Prop`

is also proof irrelevant and understood to have no internal structure like you say, just "true" and "false"

Last updated: Dec 20 2023 at 11:08 UTC