The Coq mailing list

[Stefan Monnier <monnier AT IRO.UMontreal.CA>]

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

Which brings me to a question I've had for a while now:
When Set was made predicative, why wasn't the relationship between
Type/Prop/Set changed to "Prop : Set : Type₀"?

I can't quite understand what is the current situation, where Prop and
Set seem to be "siblings" (as was the case when set was impredicative)
yet at the same time Set is above Prop.  I'm not sure what are the
benefits of this "flou artistique".


        Stefan