The Coq mailing list

[Stefan Karrmann <sk AT mathematik.uni-ulm.de>]

Hello,

if the tower of Type is Type_i : Type_{i+1} for all i in N, why does the
following gives an error?

   Coq < Print type_of.
   type_of = fun (T : Type) (_ : T) => T
        : forall T : Type, T -> Type


   Argument T is implicit
   Argument scopes are [type_scope _]

   Coq < Eval compute in (type_of (type_of (Type))).
   Error: Universe Inconsistency.

Here the written Type is Type_i for some i in N. Then type_of Type_i is
Type_{i+1} and the final result should be Type_{i+2} of type Type_{i+3}.
Where gets the inconsistency in?

PS: The same happens for Set, nat and O:
   Coq < Eval compute in (type_of (type_of (O))).
   Error: Universe Inconsistency.

Regards,
-- 
Stefan Karrmann

"The reasonable man adapts himself to the world; the unreasonable one persists
 in trying to adapt the world to himself.  Therefore all progress depends on 
 the unreasonable man."
-- George Bernard Shaw