The Coq mailing list

[Jeffrey Harris <janglernpl AT gmail.com>]

Hello!

I am aware that having the special rule that members of
type Prop can't be used for computation is useful for efficiency and
for extracting programs, but I was curious as to whether there was any
"purely mathematical" (sorry, I know that's not very precise) reason
for having this restriction. The same for Set. More specifically, if
the Calculus of Inductive Constructions were implemented solely with
sorts Type(0), Type(1), etc., what would be the differences between
that implementation and the implementation with Set and Prop? 

Also, do you know of any paper which describes the CIC system with the only sorts being the Type(n)'s?

Thanks,
Jeffrey Harris