coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Type:Type and turning of universe consistency check

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Cc: Peter LeFanu Lumsdaine <p.l.lumsdaine AT gmail.com>
Subject: Re: [Coq-Club] Type:Type and turning of universe consistency check
Date: Sun, 12 Apr 2015 15:18:07 -0400

Coq 8.5 (beta) has -type-in-type (listed under coqc --help). If you don't want to move to Coq 8.5, the closest you can get in Coq 8.4 is -impredicative-set, which doesn't quite give you what you want. I think Vladimir Voevodsky and Dan Grayson also had a patch for Coq 8.4 that gave you Type:Type (but you have to build Coq from source, then, anyway).

-Jason

On Sun, Apr 12, 2015 at 3:02 PM, Erik Palmgren <palmgren AT math.su.se> wrote:

Hello

I would like to experiment with computational behaviour in a type theory with Type:Type. Is there any possibility to turn off universe consistency check in (recent versions of) Coq? At same time I would like to force Type(1):Type(1) (say).

I seem to remember experiments like this were indeed possible in old Agda by simply making a suitable inductive-recursive definition of such a universe and ignoring warnings of non-well foundedness.

Thanks

Erik Palmgren

RE: [Coq-Club] Term classification in ltac: has_var / is_constr / term complexity measure, Soegtrop, Michael, 04/01/2015
- Re: [Coq-Club] Term classification in ltac: has_var / is_constr / term complexity measure, Jonathan Leivent, 04/01/2015
  - RE: [Coq-Club] Term classification in ltac: has_var / is_constr / term complexity measure, Soegtrop, Michael, 04/02/2015
    - Re: [Coq-Club] Term classification in ltac: has_var / is_constr / term complexity measure, Jonathan Leivent, 04/02/2015
      - Re: [Coq-Club] Term classification in ltac: has_var / is_constr / term complexity measure, Jonathan Leivent, 04/02/2015
        
        Re: [Coq-Club] Term classification in ltac: has_var / is_constr / term complexity measure, Jonathan Leivent, 04/04/2015
      - [Coq-Club] Type:Type and turning of universe consistency check, Erik Palmgren, 04/12/2015
        
        Re: [Coq-Club] Type:Type and turning of universe consistency check, Jason Gross, 04/12/2015
        
        Re: [Coq-Club] Type:Type and turning of universe consistency check, Erik Palmgren, 04/12/2015
        
        Re: [Coq-Club] Type:Type and turning of universe consistency check, Vladimir Voevodsky, 04/13/2015