The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

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

Vladimir.