The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

I have a question about universes (I keep getting universe
inconsistencies and I find them hard to debug). 

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?

(And, more generally, how do I find out? I can Print Universes, but that
gives me a long list of constraints between universe variables, but
without telling me which variables are associated with what functions).

Thanks,

Edsko