The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

On Mon, Sep 05, 2011 at 09:01:13PM -0400, Stefan Monnier wrote:
> > It is a (modest) change of the theory introduced in Coq version 8.2
> > (with reference manual lately updated from version 8.2pl2). The change
> > is motivated by sort polymorphism of inductive types so that it works
> > smoothlier. Typically, sort-polymorphism places the definition of
> > unit:Type at level Prop, and Prop<=Set allows to freely use unit also
> > at level Set or Type(n), as intuitively expected.
> 
> To what extend is it different from "get rid of Set, and then rename
> Type(n+1)=>Type(n) and Type(0)=>Set"?

As far as I understand, getting rid of Set could prevent the option
where Set is impredicative. 
If Set is predicative (the current default), I don't know.

BTW, it seems that without full polymorphism (impredicative Set)
we don't have a decent universal identity function id = \x.x
(i.e., no type can be assigned to id such that (id id) reduces to id).
Is this claim correct?

JF