The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Sorry, the definition was supposed to be of the form:

Inductive U (T:Type) :Type := gen: U |  prod: forall X:U, forall P: elem X -> 
U,  U

with

fixpoint elem (X:U) : Type := 

match X with 

| gen => T

| prod Y P => forall y: elem Y, elem (P y)

end.

.

Then it would be reasonable to expect that if T:Type(0) then U(T):Type(0).

Vladimir.