The Coq mailing list

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

Hi Adam,

Thanks for your answer. However, based on what my newfound Print command tells
me I'm not sure you're right. The output of

  Inductive prod (A B : Type) : Type :=
    | pair : A -> B -> prod A B.
  
  Set Printing Universes.
  Print prod.

in coq (with -nois) is

  Inductive prod (A : Type (* Top.1 *)) (B : Type (* Top.1 *))
              : Type (* Top.1 *) :=  pair : A -> B -> prod A B

In other words, all the types have the *same* universe variable.
However, when I define prod slightly differently,

  Inductive prod (A : Type) (B : Type) : Type :=
    | pair : A -> B -> prod A B.

we get

  Inductive prod (A : Type (* Top.1 *)) (B : Type (* Top.2 *))
              : Type (* max(Top.1, Top.2) *) :=  pair : A -> B -> prod A B

Which is approximately what you said. Slightly different again:

  Inductive prod : Type -> Type -> Type :=
    | pair : forall (A : Type) (B : Type), prod A B.
  
  Set Printing Universes.
  Print prod.
  Print Universes.

We get

  Inductive prod
                : Type (* Top.1 *) ->
                  Type (* Top.2 *) -> Type (* max((Top.4)+1, (Top.5)+1) *) :=
      pair : forall (A : Type (* Top.4 *)) (B : Type (* Top.5 *)), prod A B
  
  Top.5 <= Top.2
  Top.4 <= Top.1

Which is more permissive again.

Interestingly, for the definition of prod from the standard library, Print
gives

  Inductive prod
                (A : Type (* Coq.Init.Datatypes.22 *))
                (B : Type (* Coq.Init.Datatypes.22 *))
              : Type (* Coq.Init.Datatypes.22 *) :=  pair : A -> B -> A * B

which corresponds to our first definition (the most restrictive version).

I'm not sure why the definition in the standard library is defined the way it
is; it seems more restrictive than it needs to be. But I'm sure somebody can
tell me that there is a very good reason for it :)

Thanks again,

Edsko