The Coq mailing list

[Helmut Brandl <helmut.luis.brandl AT gmail.com>]

Thanks for the answer. Is it correct that "Prop <= Set" is not necessary for the expressive power of CIC?

The answer is probably yes since you plan to remove it.

My silly example is no problem since I didn't expect it to work anyhow. It is always possible to define the identity function having the type "forall (T:Type)(x:T):T".

Regards

Helmut

On Thu, Jun 7, 2018, 10:04 Matthieu Sozeau <mattam AT mattam.org> wrote:

Hi,

What we don’t have is Prop : Set indeed, only Prop <= Set and Set <= Type(i). Actually we even have Prop < Set internally, i.e the two sorts are enforced to be distinct. One reason is that the set-theoretic model allows this, the impredicative universe Prop being interpreted as { ø, { ø } } which is a subset of Set’s interpretation. However this subtyping rule is a bit of a pain as it complicates the model: one has to modify the interpretation of function types and applications to use a so-called trace encoding to kind of dynamically detect if a term is in Prop or Set. If we remove it (which is a plan we have for a future version of the calculus), then one can see Prop as a separate universe from the predicative Type hierarchy and your example wouldn’t work anymore.

Hope this helps a little,
— Matthieu

Le jeu. 7 juin 2018 à 16:34, Helmut Brandl <helmut.brandl AT gmx.net> a écrit :

Hi.

I am confused by a subtyping rule mentioned in chapter 4.4 of the reference manual.

It says that Prop is a subtype of Set. I checked it with the identity function

Definition id {T:Set} (x:T):= x.

And indeed the _expression_ "id I" is well typed.

I always thought that both Set and Prop are subtypes of Type(i) for any i but are not related in the subtyping relation.

What is the reason for this subtyping rule? Can anybody explain?

Thanks

Helmut