The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

   Hello,

Le 20 juil. 05, à 16:30, Vladimir Voevodsky a écrit :

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

You are basicaly right.  Set can be considered as the lowest element of 
the Type(i) hierarchy. Originaly however, Set was impredicative, while 
Type (actually the hierarchy of Type(i)'s) is not. When it was decided 
to make Set predicative, there were two reasons for keeping Set:

* One is that it was decided to keep the possibility to run coq with 
the option "impredicative" and keeping the old behavior of Set. For 
that, it was easier to keep the entry Set in the system.

* The other one was for compatibility. Indeed, the tactics which chose 
names for hypotheses they introduce (like inversion) will chose 
different names whether the sort of this hypothesis is Set or Type. 
Therefore, if one maps all entries "Set" to "Type" in the existing 
developments, the naming behavior of these tactics is changed and one 
introduces a lot of stupid, but nether the less difficult to correct, 
mistakes.

It is clear that this second reason is circumstancial and not very 
satisfiying. However, it was decided that keeping an entry Set was the 
easiest compromise even if, as you point out, it introduces some 
confusion.

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

The choice of the keyword Set can certainly be discussed like most 
syntactic choices. As to what corresponds best to a set in a 
type-theoretical setting, this is a vast question whose issues have not 
yet been all setled.

Best wishes,


Benjamin