The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Edsko de Vries wrote:
> prod is defined in the Coq standard library as
>
>   Inductive prod (A : Type) (B : Type) : Type :=  pair : A -> B -> A * B
>  
> Now, the type of prod is really
>
>   Type(i) -> Type(j) -> Type(k)
>
> with some constraints between i, j and k. What are these constraints?
>   

I think the constraints are [i <= k] and [j <= k].  AFAIK, in general, 
the universes of an inductive type's parameters add "<=" constraints 
w.r.t. the inductive type itself.