This might be a dumb question and I'm blanking on something obvious, but could someone give the justification for why when we quantify over Types but return a prop, the result is still in prop?

```
Check ((forall (x: Type), 1 = 1) : Prop).
```

Is this related to the impredicativity of Prop? I thought that was just about quantifying over Prop still being in Prop, rather than quantifying over Type.

I guess more specifically I'm asking about the justification for the Prod-Prop typing rule: https://coq.inria.fr/refman/language/cic.html#id6

The manual explains that no values of a term of type `Prop`

are extractable, hence this rule, but I was wondering if there was some more justification for this.

No, that is about it. Objects in `Prop`

are non-informational. Quantifying over them does not change that fact. Pretending that they suddenly carry some information due to quantification would just make the system more painful to use.

Is this related to the impredicativity of Prop? I thought that was just about quantifying over Prop still being in Prop, rather than quantifying over Type.

impredicativity of Prop means that we have the Prod-Prop rule

quantifying over Prop is not special

It's probably fair to say the real reason isn't obvious: (1) you build an appropriate proof that Coq's metatheory has certain good properties (say, it's logically sound) (2) you see this rule isn't a problem. And step (1) isn't trivial.

@Gaëtan Gilbert could you clarify what the formal definition of impredicativity is?

a sort `s`

is impredicative when for all product types if the codomain is in `s`

then the product type is also in `s`

Just to clarify: Gaëtan describes the kind of impredicativity accepted by Coq. Impredicativity itself is a more general notion which can be introduced in a few different ways (some of which will introduce known forms of unsoundness).

Last updated: Jan 28 2023 at 06:30 UTC