Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Universe Inconsistency?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Universe Inconsistency?


chronological Thread 
  • From: Stefan Karrmann <sk AT mathematik.uni-ulm.de>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] Universe Inconsistency?
  • Date: Thu, 21 Oct 2004 21:30:52 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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




Archive powered by MhonArc 2.6.16.

Top of Page