The Coq mailing list

[Bas Spitters <B.Spitters AT cs.ru.nl>]

On Wednesday 20 July 2005 16:30, Vladimir Voevodsky wrote:
> I am learning Coq and I can not understand why it needs the sort Set.
> As far as I can see Type can be used everywhere where Set is used.
>
> On the other hand, having Set seems to introduce unnecessary
> confusion e.g. setoids are sometimes said to be sets with equality
> and sometimes types with equality.  Similarly, one can introduce
> natural numbers by two inductive definitions which are identical
> except for the fact that one introduces nat as a set and another one
> as a type.
>
> Another confusing point is that the closest analog of a "mathematical
> set"  in Coq is a setoid (a type with an equality) while a member of
> Set is something, from my perspective,  rather weird.
>
> What am I missing here??

Just a few comments.
First there is the historical reason: Set  used to be impredicative, which 
was 
a good reason to separate it from Type.
Now the most important difference between Set and Type is that Prop is a 
subtype of Type, but not of Set. Thus sometimes you might want to quantify 
over Set, however, if you quantified over Type, you would be allowed to fill 
in Prop. This is usually unintended and sometimes dangerous (when adding 
axioms for instance). Recall that Prop is still impredicative.

Regarding the code-duplication: I, and probably many others, have mentioned 
this before. After discussions Hugo Herbelin suggested a nice solution, but, 
as a understand, he did not havetime to implement it yet.

Finally, regarding terminilogy. Again this has historical reasons, maybe 
setoid -> (Bishop) set
Set ->  Type or Type0
would be better, but this will be hard to change.

Bas