The Coq mailing list

[t x <txrev319 AT gmail.com>]

Thoughts:

Although Coq displays the following:

(1) cons: forall (A: Type) (lst: list A) (x: A), list A

we know this is a "lie" since Coq has a universe tower rather than a type of types.

Thus, it seems internally, this must be stored as:

(2) cons: forall (k: Coq-internal-Int) (A: universe k) (lst: list A) 9x: A), list A

Now, we can't have (2) in Coq since "defining Natural numbers requires Type" so we can't have

"k:Nat"

and must instead have

"k: Coq-internal-int"

Question:

Is the above analysis correct? If not, how else does Coq get around the fact that "[Universe k] is always displayed as Type" and "having a Type of Type -> paradox."

Thanks!