The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Well, this is doable. One uses Type_i or Type(i) or some other syntax  
like that but treats Type_1, Type_2 etc. as atomic expressions i.e.  
not as combinations of something with an integral index but as a  
collection of completely distinct names.  Could just as well use use  
Type_alpha, Type_beta, Type_gamma etc. In the normal course of events  
one should not need more than a few of them.

Vladimir.



On Jul 23, 2005, at 10:42 AM, Stefan Karrmann wrote:

> 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
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club