The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hello,

I agree the situation is a bit messy, but I suspect the motivation was
to retain the possibility to run Coq with an impredicative Set sort
(using the -impredicative-set flag).

However, the current status of this flag should probably be clarified.
If we can confirm its use has become uncommon (which I believe is the
case), we could deprecate it, then remove it and simplify that part of
the theory.

I'm not sure why we would keep Set in your proposal, though. Does it
play any role?

Maxime.

On 06/07/2018 05:13 PM, Stefan Monnier wrote:
>> 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
>