The Coq mailing list

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

Sorry. I cannot yet get it straight.

From the subtype rules in the reference manual and your response to my question it has to be the case that Prop <= Set.

From the Conv rule I conclude that T:Prop implies T:Set.

This implies that I can feed any proposition into an argument expecting a Set.

Definition idset (A:Set)(x:A):=x.

The term idset (0<=0) (le_n 0) surprisingly passes the type checker.

Is this really the intended behaviour?

Sorry if my question is to stupid. But it puzzles me.

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