The Coq mailing list

[Stefan Karrmann <sk AT mathematik.uni-ulm.de>]

Benjamin Werner (Thu, Jul 21, 2005 at 11:01:36AM +0200):
> 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:

If we use the index in the hierarchy of Typ(i)'s explicitly, we have

   forall i j:nat, i < j -> Type(i):Type(j)

in Coq.


What is the type of 'fun i:nat => Type(i)' or 'Type' ???


Is it 'forall i:nat, Type(i+1)'?
But this is a tangled recursive definition of a value *and* its type.


Or is it something like 'Type omega' where omega is the smallest infinite
ordinal? But then Type must have type 'forall o:ord, Type(ord_succ o)' where:

   Inductive ord:Set :=
   | ord_zero : ord
   | ord_succ : ord -> ord
   | ord_limit : (nat -> ord) -> ord.

   Fixpoint nat_to_ord (n:nat):ord :=
      match n with
      |   0 => ord_zero
      | S m => ord_succ (nat_to_ord m)
      end.

   Coercion nat_to_ord : nat >-> ord.

   Definition omega : ord := ord_limit nat_to_ord.


Note: The specification ord does belong to Set, although the collection of
      ordinals is a proper class in the sense of Von Neumann-Bernays-Gödel
      set theory (NBG)! This looks paradoxical.

Regards,
-- 
Stefan