The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2013/11/18 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."

I think it is not correct.
"cons" is not universally quantified over 'k'.

A more correct vision would be:

cons: forall (A:Type-k) (lst:list A) (x:A), list A

Where k is some "internal Coq integer" which is computed by the system (so it is fixed, and you cannot provide the 'k' value to cons).
In fact, in practice, 'k' is not a Coq Integer, but some system on algebraic _expression_, and you have to check that all systems in the Coq module you define have a solution (so 'k' can be instantiated by an integer).
For your "  we can't have (2) in Coq since "defining Natural numbers requires Type" ", this is wrong in a way, since natural numbers only require Set, not Type. Still, having the ability to express levels with natural numbers would be a burden, as you could not "insert" universes between two given universes. So the only trick I know if you want to do universe manipulations is to do "Definition Universe5 := Type. Definition Universe4 := Type:Universe5. …". And then you can "Inductive list (A: Universe4) : Universe5 := …" This trick fixes the universes once and for all. It can be a good trick to lighten Coq work on universe computations.
 

Thanks!

--
.../Sedrikov\...